The Euclidean plane is the n = 2 case of R^n, not a parallel construction

Identifier: F:rn-cpoint-agreement
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

The map RN.ofCPoint sending a plane point P to the vector (x P, y P, y P, ...) satisfies: <ofCPoint P, ofCPoint Q>_2 ~ CPoint.dot P Q; <ofCPoint P - ofCPoint Q, ofCPoint P - ofCPoint Q>_2 ~ CPoint.distSq P Q; RN.dist 2 (ofCPoint P) (ofCPoint Q) ~ Metric.CPoint.dist P Q; and it carries the two setoid equalities into each other IN BOTH DIRECTIONS -- CPoint.Equiv P Q iff EqOn 2 (ofCPoint P) (ofCPoint Q). So the plane's inner product, its squared distance and its metric distance are the n = 2 instances of the general definitions, established rather than assumed.

Formal statement

theorem RN.ofCPoint_dist : ((x0 : CPoint) -> ((x1 : CPoint) -> CReal.Equiv (RN.dist (AxNat.succ (AxNat.succ AxNat.zero)) (RN.ofCPoint x0) (RN.ofCPoint x1)) (Metric.CPoint.dist x0 x1)))

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

kernel-RN.ofCPoint_dist

Kind: kernel-term
Status: checked

Supports: RN.ofCPoint_dist is admitted by the trusted kernel gate with the type recorded in formal.statement, and Kernel::axiom_footprint reports 0 assumed names. The three siblings RN.ofCPoint_dot, RN.ofCPoint_distSq, RN.ofCPoint_congr and RN.cpointEquiv_of_eqOn are admitted in the same build with the same empty footprint.

Checker command

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

Evidence notes

Anchored with [[:space:]], never \t. grep -c rather than grep -q. --release is MANDATORY.

rn-ofcpoint-coordinate-placement

Kind: witness-replay
Status: checked

Supports: that RN.ofCPoint puts the coordinates where the agreement lemmas assume, rather than agreeing by some coincidence of the two definitions

Checker command

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

Evidence notes

The probe quantifies over the point rather than instantiating it, deliberately: a probe at a concrete CPoint.mk would reduce through the constructor and could pass for reasons that have nothing to do with the definition's shape.

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."
}