RationalFieldCertificate
plain-language theorem explainer
Bundles the field axioms for the PRC rational quotient with display laws matching ordinary rational arithmetic, positivity, and the lifted J-cost. Anyone assembling the first-pass PRC kernel cites this as the rational-stage certificate. It is a pure Prop structure: no proof body, only named fields filled by a later inhabitant theorem.
Claim. A certificate asserting that the PRC rational quotient $R$ is a field: addition and multiplication are commutative and associative, $0$ and $1$ are identities, negatives and nonzero inverses exist with standard cancellation, and distributivity holds; moreover $0\neq 1$, division and positivity agree with the ordinary embedding $r\mapsto r^{\mathbb{Q}}$, the J-cost on $R$ displays as $J(r)=(r+r^{-1})/2-1$, and that cost is invariant under normalizing the underlying ratio-orbit representative.
background
Primitive Recognition Calculus builds arithmetic from distinction data rather than assuming $\mathbb{Q}$ as a primitive. Ratio orbits are equivalence classes of integer ratios; the PRC rational type is their quotient, with a forgetful map into ordinary rationals that bridges all display statements.
The J-cost on this stage is the functional forced at T5 of the unified forcing chain: $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). It is first defined on ratio orbits, then lifted to the rational quotient by a well-definedness argument using injectivity of the ordinary-rational embedding.
Upstream, additive and multiplicative monoid laws for the underlying logic naturals (associativity, commutativity, units) are proved by induction on the successor construction in ArithmeticFromLogic; the integer/rational layer reuses those patterns. This module packages the full field surface plus J-cost and positivity displays into one Prop for kernel assembly.
proof idea
No proof body: the declaration is a structure of type Prop whose fields are the named axioms and display equalities. An inhabitant is supplied separately by the theorem that builds a RationalFieldCertificate, assigning each field to the corresponding lemma on PRC rationals (commutativity, associativity, left-negation, inverse cancellation gated on nonzero ordinary image, division and positivity display biconditionals, and the two J-cost display theorems). The structure itself only records the interface.
why it matters
This is the rational-stage bundle in the first-pass PRC kernel. Downstream, the kernel first-pass certificate (K7/A2) requires concrete Lean objects for each stage of the analytic specification; the rational field certificate is one of those stages, sitting above trace logic and below later inevitability theorems. The companion inhabitant theorem discharges the structure by wiring in the proved field and display lemmas.
Framework-wise it anchors the T5 J-uniqueness formula on the PRC rational quotient and guarantees that positivity and division agree with ordinary $\mathbb{Q}$, so later mass-ladder and cost arguments can move between the constructive quotient and classical arithmetic. It is a bundling certificate, not the final inevitability claim: the kernel doc marks first-pass certificates as intermediate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.