recip
plain-language theorem explainer
The reciprocal map ι(x)=x⁻¹ on the reals is the dual-recognition symmetry that generates both the J-cost and the golden-ratio scale. Anyone citing the Universal Forcing chain, cost factorization, or character rigidity uses this as the shared generator. It is a one-line definition aliasing real inversion; downstream lemmas prove it is an involution and that J and φ are built from it.
Claim. Define the reciprocal involution $\iota:\mathbb{R}\to\mathbb{R}$ by $\iota(x)=x^{-1}$. On the positive reals this is the dual-recognition symmetry exchanging a quantity with its reciprocal.
background
The module isolates a single structural object beneath the cost-form theorem and the φ-forcing theorem. Those two results, when merely conjoined, talk about unrelated objects (the J-cost and a minimal hierarchy). Here both are derived from one function: the reciprocal involution ι(x)=x⁻¹ on the positive reals.
On the cost side, J is exactly the ι-symmetric cost (J∘ι=J). On the scale side, φ is the unique fixed point greater than 1 of the ι-shift g(x)=1+ι(x). The Recognition Composition Law and the T5–T6 forcing steps sit downstream of this shared generator.
Upstream, a discrete reciprocal already exists on ratio orbits (sending zero to zero, as in ℚ), together with a PRC-native positivity predicate. The present definition lifts that idea to the continuum reals as plain multiplicative inverse.
proof idea
One-line definition: recip x is definitionally x⁻¹. No tactics, no lemmas. Sibling theorems in the same module then establish that this map is an involution on the positive reals, that its fixed-point locus is {±1}, that J is symmetric under it, and that φ is the unique fixed point >1 of the shift x↦1+ι(x).
why it matters
This is the common generator that turns the OneLaw assembly into a genuine deduction rather than a glued pair of independent facts. Downstream, cost factorization uses it heavily: BaseSansTwo requires a reciprocal axiom on ratio-orbit maps; rationalTrace, realCharacterCandidate, and traceDisplay all prove reciprocity identities for native cost characters; CharacterRigidityForcing closes calibration under reciprocals.
In the forcing chain it sits logically upstream of T5 (J-uniqueness via the RCL and ι-symmetry) and T6 (φ as the self-similar fixed point of the ι-shift). The module certificate ReciprocalGeneratorCert packages both sides so later continuum and mass-ladder work can cite one object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.