R^n is a constructive metric space, for every n at once

Identifier: F:rn-is-a-metric-space-at-every-dimension
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every natural number n, the setoid (Nat -> CReal, EqOn n) under the Euclidean distance d(u,v) = ||u - v||_n satisfies all twelve fields of the `Metric` record of ADR-1602: the setoid laws, the congruence of the distance under the equivalence, nonnegativity, both directions of the identity of indiscernibles, symmetry, and the triangle inequality. The witness `RN.metric` is a FUNCTION of the dimension, so this is one instance for every finite dimension rather than one instance per dimension. The consequence that matters is not the record but what the record carries: `Metric.dist_self`, `Metric.dist_quadrilateral`, `Metric.CauchyAt`, `Metric.Cauchy`, `Metric.TendsTo` and `Metric.Complete` are all stated for an ARBITRARY metric space, so every one of them now reads on R^n with no further work.

Formal statement

def RN.metric : ((x0 : AxNat) -> Metric)

Dependencies

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

3 direct dependencies 1 direct dependents

Evidence

kernel-RN.metric

Kind: kernel-term
Status: checked

Supports: RN.metric is admitted by the trusted kernel gate as a Definition of type `Nat -> Metric`, which means every one of the record's twelve field obligations type-checked, and Kernel::axiom_footprint reports 0 assumed names.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection -- --require-declaration RN.metric | grep -cE '^found[[:space:]]+rn[[:space:]]+definition[[:space:]]+RN\.metric[[:space:]]+0$'

Evidence notes

Anchored with [[:space:]], never \t (in a scripted GNU grep \t is a literal t). grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. --release is MANDATORY. A `Definition` of record type is the strongest single check available here: the record is not a bag of names but a telescope, so a wrong distance cannot be substituted without one of the eleven law fields failing to typecheck against it.

rn-metric-negative-controls

Kind: witness-replay
Status: checked

Supports: that the record REFUSES plausible wrong choices of distance, so admitting the real one is a finding rather than a formality

Checker command

cargo test --release -p axeyum-lean-kernel --lib rn:: -- --test-threads=2

Evidence notes

Mutation-verified: substituting the REAL distance into the squared-distance control's replacement slot makes exactly one test die (a_squared_distance_is_refused_as_a_metric), so the refusal is caused by the squared distance and not by the probe machinery.

Provenance

{
  "date": "2026-09-04",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_rn_prelude (crates/axeyum-lean-kernel/src/rn.rs)",
  "source": "Lane `rn-carrier`, roadmap W2-4 (convergence point C7), design recorded in ADR-1606. The `Metric` record it instantiates is ADR-1602's."
}