native_recip_fixed_iff_cost_zero
plain-language theorem explainer
On positive ratio orbits, the reciprocal fixes q exactly when native cost vanishes: the unit is the unique self-reciprocal zero-cost point. Downstream reciprocal-generator certificates cite this as the unit-is-cost-zero clause. The proof is a short two-direction rational argument: fixed points force q²=1 hence q=1, and zero cost forces q=1 via the cost-zero characterization.
Claim. Let $q$ be a ratio orbit with positive rational value. Then the reciprocal of $q$ has the same rational value as $q$ if and only if the native cost of $q$ (the $J$-cost pulled back along the orbit display) is zero.
background
Ratio orbits are the K4.7 display of a signed integer numerator over a nonzero distinction-natural denominator, with a total map to rationals. Their reciprocal is the K4.12 total operation that sends the zero orbit to itself and otherwise swaps numerator and denominator in the usual way.
Native cost on these orbits is the pullback of the closed-form cost $J_q$ (the rational avatar of the Recognition cost $J(x)=(x+x^{-1})/2-1$). Sibling facts record $J_q(1)=0$, nonnegativity, and the characterization that $J_q(q)=0$ forces the rational value to be $1$ on the nonzero cone.
The local module builds a structural ledger for that native cost: involutivity of reciprocal, cost symmetry under reciprocal, uniqueness of the zero-cost unit, and the absence of a native golden-scale fixed point. This theorem is the unit clause of that ledger.
proof idea
Rewrite the reciprocal-to-rational identity and the identification of orbit cost with $J_q$. Split the biconditional.
Forward: if reciprocal fixes the rational value, field simplification plus linear arithmetic yields $q^2=1$. Positivity then forces $q=1$ by nonlinear arithmetic, and $J_q(1)=0$ closes the goal.
Reverse: if cost is zero, apply the sibling zero-cost characterization (nonzero positive rational with $J_q=0$ implies value $1$), then norm_num checks that reciprocal fixes $1$.
why it matters
Feeds directly into nativeReciprocalGeneratorSplit_holds, which packages the native reciprocal generator split: involutivity, cost symmetry under reciprocal, unit-is-cost-zero (this theorem), and the no-native-golden-scale purchase obstruction.
In Recognition terms this is the elementary fixed-point half of T5-style $J$-uniqueness on the rational cone: $J$ vanishes only at the unit, and the unit is the only positive self-reciprocal orbit. That matches the closed form $J(x)=\cosh(\log x)-1$ and the Recognition Composition Law, where cost-zero is the identity of the multiplicative group.
It is choice-free and stays inside the integer/rational primitive calculus, so later ledger and minimality certificates can quote a fully discharged algebraic fact rather than an analytic uniqueness argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.