NativeReciprocalGeneratorSplit
plain-language theorem explainer
Packages the φ-split as four reciprocal-generator facts on ratio orbits: reciprocal is involutive on the rational display, J-cost is reciprocal-symmetric, positive fixed points of reciprocal are exactly the cost-zero units, and no positive orbit solves the golden-scale equation. The structural ledger cites it via the theorem that discharges all four fields. Definitional Prop bundle; no proof body.
Claim. A proposition asserting four facts on ratio orbits $q$: (i) reciprocal is an involution on the rational display, $\mathrm{toRat}(\mathrm{recip}(\mathrm{recip}\, q))=\mathrm{toRat}(q)$; (ii) the rational $J$-cost is reciprocal-symmetric, $\mathrm{toRat}(J(\mathrm{recip}\, q))=\mathrm{toRat}(J(q))$; (iii) if $\mathrm{toRat}(q)>0$, then $\mathrm{toRat}(\mathrm{recip}\, q)=\mathrm{toRat}(q)$ if and only if $\mathrm{toRat}(J(q))=0$; (iv) there is no positive ratio orbit with $1+q^{-1}=q$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer-numerator / nonzero-orbit-denominator display of a rational (K4.7). Its verifier map toRat sends the orbit to $\mathbb{Q}$ by ordinary division; the internal equality test is cross-multiplication. Reciprocal on ratio orbits is total and sends zero to zero, matching $\mathbb{Q}$ (K4.12).
The PRC rational $J$-cost on a ratio orbit is the orbit-level object $J(q)=((q+q^{-1})/2)-1$, built from orbit add, mul, recip, and the half unit. It is not yet the real-analytic uniqueness theorem; that bridge sits downstream. The universal-forcing reciprocal generator is the dual-recognition involution $\iota(x)=x^{-1}$ on the positive reals; the present structure records which of its cost consequences are already native at the ratio-orbit layer.
The module is the structural ledger for native cost minimality certificates. The doc-comment names the content: everything the reciprocal generator says about the cost is $\delta$-native; only the fixed point is bought.
proof idea
No proof body: this is a structure whose type is Prop, i.e. a named bundle of four fields. Each field is a pure statement about ratio orbits, reciprocal, toRat, and the orbit-level $J$-cost. Discharge is deferred to the sibling theorem nativeReciprocalGeneratorSplit_holds, which fills the fields by native_recip_involutive, native_cost_recip_symmetric, native_recip_fixed_iff_cost_zero, and no_native_golden_scale.
why it matters
This is the ledger's φ-split interface. It separates what the reciprocal generator already forces at the native ratio-orbit layer (involution, cost symmetry, unit = cost zero) from the golden fixed-point equation, which is explicitly not native and must be purchased. Downstream, nativeReciprocalGeneratorSplit_holds is the theorem that witnesses the structure, wiring those four native lemmas into one certificate.
In the Recognition forcing chain this sits under T5 ($J$-uniqueness, $J(x)=(x+x^{-1})/2-1$) and T6 ($\varphi$ as the self-similar fixed point). The fourth field is precisely the denial that $\varphi$ (or any positive rational solving $q=1+q^{-1}$) lives inside the native ratio-orbit calculus; the fixed point is bought, not derived from $\delta$-native cost alone. That split keeps the structural ledger honest about what is forced versus what is assumed when the golden scale enters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.