rational_field_certificate
plain-language theorem explainer
The recognition-calculus rationals satisfy the full field axioms, packaged as a single certificate structure. Anyone needing a field of fractions under the primitive recognition calculus cites this. The proof is a structure inhabitant that wires already-proved additive and multiplicative lemmas, inverse cancellation, and the J-cost/positivity display equalities.
Claim. The recognition-calculus rationals form a field: for all $a,b,c$, addition and multiplication are commutative and associative, $0$ and $1$ are units, $-a+a=0$, distributivity holds, $0\neq 1$, nonzero elements have two-sided multiplicative inverses, and the division, positivity, and $J$-cost displays agree with the underlying rational embedding and ratio-orbit representatives.
background
Primitive Recognition Calculus builds arithmetic from logic rather than assuming $\mathbb{Q}$ as a primitive. Naturals arise first (ArithmeticFromLogic), then integers, then a quotient of ratio-orbit representatives yields the type of recognition rationals. The present module equips that quotient with field operations and a positivity predicate, and lifts the recognition $J$-cost from ratio orbits onto the quotient.
Upstream, the additive and multiplicative monoid laws on logic-naturals (associativity, commutativity, units) are already proved by induction on the successor structure. Those facts are transported through the integer and rational constructions to give the primed lemmas used here (associativity, left negation, distributivity, reciprocal cancellation).
The certificate structure is a Prop-valued bundle: every field axiom appears as a named field, together with display lemmas that say division, positivity, and $J$-cost on the quotient match the corresponding maps on ordinary rationals and on normalized ratio-orbit representatives.
proof idea
Pure structure construction. Each field of the certificate is filled by an existing lemma on the recognition rationals: commutativity and the primed associativity/unit/negation/distributivity facts for $+$ and $\cdot$, the $0\neq 1$ and $\mathrm{inv},0=0$ facts, and two short intro/exact blocks that apply reciprocal cancellation on both sides under a nonzero hypothesis. The last four fields are the display equalities for division, positivity (on the quotient and on ratio orbits), and the two $J$-cost lift lemmas (value on the quotient and invariance under normalized representatives). No new algebra is proved in this declaration.
why it matters
This is the field-axioms checkpoint for the primitive recognition calculus. Downstream it is consumed by the first-pass kernel certificate (K7/A2), which assembles strength tags, trace syntax, a judgment surface, and trace logic into a single inhabited kernel bundle. Without a verified rational field, later recognition constructions that need ratios, positivity, or the $J$-cost on $\mathbb{Q}$ have no certified carrier.
In the broader Recognition Science stack the $J$-cost is the unique solution of the Recognition Composition Law (forcing chain T5), and the rational field is the minimal arithmetic stage on which that cost can act before the self-similar fixed point $\varphi$ and the eight-tick octave appear. The certificate therefore sits under the foundation layer that eventually supports the forcing chain, not as a physics claim itself but as the arithmetic substrate those claims require.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.