realNullSetoidClaim
plain-language theorem explainer
Audit claim for Build Order step 9 (K1/R9): the PRC real null-distance setoid is obtained from the J-cost distance triangle modulus. Foundation auditors cite it as the named strength obligation for the null-distance quotient. It is a StrengthClaim record (label, traceClosure tag, English statement), not a proved theorem.
Claim. Build Order step 9 records the claim that the primitive recognition calculus real null-distance setoid follows from the $J$-cost distance triangle modulus, classified under trace-closure strength. The open analytic obligation is that triangle-modulus property; no new logical primitive is required.
background
In the Primitive Recognition Calculus, distances on positive reals are built from the recognition cost $J$. The classical RS cost is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced uniquely at T5 of the forcing chain. Null distance means pairs at $J$-distance zero; the intended carrier is the quotient by that relation.
A setoid packages a type with an equivalence relation so the quotient exists as a type. Upstream, the same pattern appears in logic-native integers (Grothendieck completion of pairs of logic naturals). Here the relation is null $J$-distance on a real Cauchy-style carrier from the RealCauchy import.
The module's local setting is Build Order step 9: reduce construction of the real null-distance setoid and quotient to a single analytic target, the $J$-cost distance triangle modulus, rather than inventing a new foundation axiom.
proof idea
No mathematical proof. The declaration is a structure value of type StrengthClaim: it sets the build-order label BuildOrder9_real_null_distance_setoid, tags the obligation as traceClosure, and stores the English statement that the PRC real null-distance setoid follows from the J-cost distance triangle modulus. Downstream certificate code reads this record as the named remaining obligation.
why it matters
Feeds PRCRealNullSetoidConditionalCertificate, which "records the precise remaining theorem and proves that this theorem is sufficient to construct the null-distance setoid and quotient carrier." That certificate wires triangle-modulus target to transitivity of null distance, then to the setoid instance and quotient.
In the RS ledger this is K1/R9: the final null-distance quotient still lives under trace closure; the open obligation is analytic (triangle inequality / modulus for $J$-cost distance), not a new primitive. It sits under the T5 J-uniqueness landmark and the Recognition Composition Law that governs $J$, clearing the path from cost geometry to a real quotient carrier without enlarging the axiom base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.