PRCRealNullSetoidConditionalCertificate
plain-language theorem explainer
Conditional certificate for Build Order step 9 of the Primitive Recognition Calculus. It records that a local triangle modulus for the J-cost rational distance is enough to obtain null-distance transitivity, the null-distance setoid, the real quotient carrier, and a rational embedding. Anyone assembling the PRC real line from orbit quotients would cite this packaging. The structure is pure interface: implication arrows plus a strength tag, with no proof body of its own.
Claim. A Prop-valued certificate asserting: the $J$-cost rational distance has a local triangle modulus (for every positive $\varepsilon$ there is $\delta>0$ so that two legs below $\delta$ force the third below $\varepsilon$); that modulus implies null-distance transitivity; transitivity yields a setoid on the rationals; the modulus alone yields that setoid; under transitivity the null-distance quotient type is inhabited; rationals embed into that quotient; and the obligation is tagged as a trace-closure strength claim.
background
Primitive Recognition Calculus builds number carriers from traces and distinction acts, then quotients. Rationals appear as ratio-orbit classes (cross-multiplication setoid). From those, a $J$-cost-derived distance on rationals is used to form a null-distance relation: pairs at vanishing cost distance are identified.
The remaining analytic blocker is a local triangle modulus for that distance: for each positive tolerance $\varepsilon$ there exists a smaller positive $\delta$ such that two consecutive legs below $\delta$ force the composed leg below $\varepsilon$. Upstream cost notions (observer $J$-cost, multiplicative-recognizer derived cost, rung-coarsen weighted sums) supply the same $J$-shape that this distance inherits.
Once that modulus is available, null-distance becomes transitive, hence a setoid; the intended real carrier is the corresponding quotient, with rationals embedding as classes. This module packages exactly that residual obligation chain.
proof idea
No proof body: this is a structure of type Prop whose fields are the residual targets and the implication arrows among them. The triangle-modulus field is a reflexive equality placeholder marking the open analytic goal. The remaining fields are typed implications (modulus implies transitivity; transitivity implies setoid; modulus implies setoid; transitivity implies a nonempty null-distance quotient; transitivity implies a nonempty rational embedding into that quotient) plus a strength-tag equality fixing the claim as trace-closure. Instantiation is deferred to the sibling theorem that fills each field by rfl or by the named reduction lemmas.
why it matters
Build Order step 9 conditional closure: once the local $J$-cost triangle modulus is proved, no further quotient mechanics remain. Downstream, the concrete inhabitant real_null_setoid_conditional_certificate discharges every field of this structure (via the triangle-to-transitive and transitive-to-setoid reductions), and the kernel first-pass certificate consumes the same packaging as part of the staged PRC theorem chain. In framework terms this is the last analytic gate before the PRC real line exists as a null-distance quotient of rationals, sitting under the forcing chain's cost uniqueness (T5 $J$-shape) without yet invoking eight-tick or $D=3$ geometry. The open question it isolates is precisely the triangle modulus itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.