native_recip_involutive
plain-language theorem explainer
Double reciprocal on a ratio orbit recovers the original rational under the display map to ℚ. Anyone assembling the native reciprocal-generator ledger cites this for the involution half of the split. The argument is a short rewrite through the reciprocal-to-rational transport and the field identity that inversion is involutive on ℚ.
Claim. For every ratio orbit $q$, the rational display of the double total reciprocal equals the rational display of $q$: $\mathrm{toRat}(\mathrm{recip}(\mathrm{recip}(q))) = \mathrm{toRat}(q)$.
background
Ratio orbits are the δ-native carrier for rationals in the Primitive Recognition Calculus: each pairs a signed-orbit numerator with a nonzero distinction-nat denominator. The total reciprocal on this carrier sends a ratio orbit to its inverse and fixes the zero orbit, matching the usual convention on ℚ.
The display toRat is a transport wrapper into ordinary rationals, $(q.num.toInt)/(q.den.toNat)$. Upstream, recip_toRat records that this display intertwines native reciprocal with field inversion: $(\mathrm{recip}, a).\mathrm{toRat} = (a.\mathrm{toRat})^{-1}$.
Part 8 of this module isolates which pieces of the reciprocal-generator claim are truly δ-native versus which require completing to ℝ. Involution is one of the three native facts; the self-similar scale equation is the purchase.
proof idea
One-line wrapper. Rewrite twice with recip_toRat to push both native reciprocals through the display, obtaining $((q.\mathrm{toRat})^{-1})^{-1} = q.\mathrm{toRat}$, then close by the field lemma inv_inv on ℚ.
why it matters
Supplies the involutive field of nativeReciprocalGeneratorSplit_holds, which packages four facts into NativeReciprocalGeneratorSplit: involution, cost reciprocity symmetry, unit as unique zero-cost orbit, and absence of a native golden scale. The first three live on the δ-native carrier; only the fourth buys completion to ℝ.
In the Recognition framework the reciprocal map $\iota(x)=x^{-1}$ is the dual-recognition symmetry of UniversalForcing.ReciprocalGenerator. Proving involution natively on ratio orbits, without ℝ, keeps the structural ledger honest about what the completion actually purchases. The public spine tags the reciprocal-generator claim at traceClosure because the certificate lives on ℝ; this lemma is the receipt that involution did not need that purchase.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.