real_null_setoid_conditional_certificate
plain-language theorem explainer
Build Order step 9 is closed conditionally: once the local J-cost triangle modulus holds, null-distance is a setoid and the real null quotient (with rational embedding) exists. Foundation auditors cite it to pin the remaining obligation before quotient construction. The proof assembles already-proved implication lemmas and supplies the constant-Cauchy rational embedding under transitivity.
Claim. There is a conditional certificate for the real null-distance setoid: the J-cost triangle-modulus target implies null-distance transitivity; transitivity implies the null-distance setoid laws; the triangle modulus alone implies the setoid; and under transitivity the null-distance quotient carrier is inhabited and every rational embeds as a constant Cauchy class. The certificate also records the strength tag for this step.
background
In the Primitive Recognition Calculus, reals are built from Cauchy ledgers of rational intervals rather than classical completeness axioms. Null distance is the relation that two Cauchy sequences are identified when their J-cost separation vanishes; the intended carrier is the quotient by that relation.
The local remaining analytic obligation is the J-cost triangle modulus (a quantitative triangle inequality for the recognition cost $J$). Upstream lemmas already show: triangle modulus yields null-distance transitivity; transitivity yields a setoid; and triangle modulus yields the setoid directly. Conditional on transitivity, ofRat embeds a rational as the class of the constant Cauchy sequence.
The module packages these arrows into a single Prop-structure certificate so later kernel audits can treat step 9 as a named conditional closure rather than scattered lemmas.
proof idea
Tactic-mode structure inhabitant. The triangle-modulus field is rfl (target equals itself). Transitivity-from-triangle, setoid-from-transitive, and setoid-from-triangle are filled by the three named implication theorems already proved in this module. Quotient-from-transitive and rat-embedding-from-transitive each take a transitivity hypothesis and return a witness built by the conditional rational embedding (constant Cauchy sequence at $0$, or at a general rational). Strength tag is again rfl. No new analysis is done here; the certificate only wires the chain.
why it matters
This is Build Order step 9 conditional closure in the PRC foundation stack. Doc-comment: once the local J-cost triangle modulus is proved, no quotient mechanics remain. Downstream it feeds the first-pass kernel certificate (kernel_first_pass_certificate), which assembles strength tags, trace syntax, and judgment surface for the kernel audit.
In Recognition Science terms, the null-distance quotient is the carrier on which later cost geometry and forcing-chain material sit; identifying sequences at vanishing $J$-separation is the discrete precursor to continuum structure. The certificate does not yet discharge the triangle modulus itself; it isolates that single remaining target so the rest of the setoid/quotient story is already formal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.