Completeness transfers to the product of two metric spaces

Identifier: F:metric-product-completeness-transfer
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For any two metric spaces M and N, if M and N are each `Metric.Complete` then their product `Metric.prod M N` (carried by `Sigma.{0,0} M.carrier (fun _ => N.carrier)`, distance the max metric `dist (x,y) := CReal.max (M.dist (fst x)(fst y)) (N.dist (snd x)(snd y))`) is `Metric.Complete` too. The Cauchy-ness of each projected component sequence needs no combination of moduli -- the product's own Cauchy witness already bounds both components at the same rate, via `le_max_left`/`le_max_right`. Recombining the two limits' own (independently witnessed) TendsToAt moduli into one witness for the pair DOES need a combination step: `Rat.natDivSucc` is monotone increasing in its numerator, so the SUM of the two moduli dominates both, standing in for "the max of the two moduli" (no `Nat.max` primitive is threaded through `Rat.natDivSucc`'s own lemmas; the sum has the same domination property a max would, which is the only property this proof needs).

Formal statement

theorem Metric.prod_complete : (x0 : Metric) -> (x1 : Metric) -> (x2 : Metric.Complete x0) -> (x3 : Metric.Complete x1) -> Metric.Complete (Metric.prod x0 x1)

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

kernel-Metric.prod_complete

Kind: kernel-term
Status: checked

Supports: Metric.prod_complete is admitted by the trusted kernel gate with the type recorded in formal.statement, and Kernel::axiom_footprint reports 0 assumed names.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example metric_prod_theorem_inventory -- prod_complete

Evidence notes

--release is mandatory: the Metric/CPoint/CReal preludes this sits on top of overflow the default debug thread stack, and the debug kernel is measured up to 32x slower on proof terms of this size. A filter matching zero theorems exits non-zero (an absent theorem is a failure, not an empty report), the same discipline nat_theorem_inventory/kernel_declaration_projection use.

suite-every_metric_prod_declaration_is_axiom_free

Kind: exhaustive-enumeration
Status: checked

Supports: All twelve names this lane's file declares, including Metric.prod_complete, have an empty Kernel::axiom_footprint. The test derives its name list from MetricProdNames::all(), not from a literal, so a new declaration cannot escape it.

Checker command

cargo test --release -p axeyum-lean-kernel --lib -- metric_prod::metric_prod_tests::every_metric_prod_declaration_is_axiom_free --test-threads=4 2>&1 | grep -cE '^test result: ok\. 1 passed'

Evidence notes

`cargo test -- <filter>` runs ZERO tests and exits 0 when the filter matches nothing, so the exact `1 passed` count is load-bearing, not the exit status alone. --release avoids the debug-build stack overflow this prelude's upstream (CReal/CPoint/Metric) is already documented as needing.

Provenance

{
  "date": "2026-09-05",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_metric_prod_prelude (crates/axeyum-lean-kernel/src/metric_prod.rs)",
  "source": "Lane `metric-products`, roadmap W2-10 (the product-of-two-metric-spaces half `metric/subspace.rs` left open). ADR-1639. formal.statement is Kernel::render_lean of the declaration's type, taken verbatim from this lane's own metric_prod_theorem_inventory example (kernel_declaration_projection does not build this prelude, so it could not supply it)."
}