ReciprocalGeneratorCert
plain-language theorem explainer
Certificate packing five properties that make the reciprocal map ι(x)=x⁻¹ the shared generator of the recognition cost J and the golden ratio φ. Cited by anyone treating cost symmetry and φ-forcing as one structural fact rather than two glued theorems. Fields record involutivity, J∘ι=J, cost-zero units as fixed points of ι, uniqueness of φ as the >1 fixed point of the ι-shift g=1+ι, and the witness g(φ)=φ. Pure structure definition; the holding instance is assembled elsewhere from sibling lemmas.
Claim. A certificate of five properties of the reciprocal map $\iota(x)=x^{-1}$ on $\mathbb{R}_{>0}$: (1) $\iota$ is an involution; (2) $J(\iota(x))=J(x)$ for all $x>0$, where $J(x)=(x+x^{-1})/2-1$; (3) $\iota(x)=x$ if and only if $J(x)=0$; (4) for $x>1$, the reciprocal-shift $g(x)=1+\iota(x)$ satisfies $g(x)=x$ if and only if $x=\varphi$; (5) $g(\varphi)=\varphi$.
background
The module isolates a single structural object beneath two capstone facts that OneLaw only conjoins: the shape of the recognition cost J and the forcing of the scale ratio φ. That object is the reciprocal involution ι(x)=x⁻¹ on the positive reals, the dual-recognition symmetry exchanging a quantity with its reciprocal.
On the cost side, J is defined by J(x)=(x+x⁻¹)/2−1 (the T5 unique cost form) and is exactly the ι-symmetric cost: J∘ι=J. Fixed points of ι are precisely the cost-zero units. On the scale side, the reciprocal-shift g(x)=1+ι(x) has fixed-point equation x=1+1/x; φ is its unique fixed point greater than 1 (the T6 self-similar scale).
Upstream siblings supply the raw facts: involutivity of ι, J-symmetry under ι, the cost-zero characterization of fixed points, uniqueness of the g-fixed point above 1, and the direct check that φ solves g(x)=x.
proof idea
No proof body: this is a structure definition whose five fields are propositions about ι and g. The holding instance reciprocalGeneratorCert_holds fills each field by a one-line application of a sibling lemma: involutivity from recip_involutive, cost symmetry from jcost_recip_symmetric, unit/cost-zero equivalence from recip_fixed_iff_cost_zero, scale uniqueness from recipShift_fixed_iff, and the φ witness from phi_is_recipShift_fixed.
why it matters
This certificate is the genuine unification the module advertises: both halves of the cost-and-scale story quantify over the same reciprocal map, so the conjunction is a deduction about a shared generator rather than an assembly of unrelated objects. Downstream, PhiFromIota on the public spine is exactly the proposition that this certificate holds (tier THEOREM, algebra of ι / 1+ι). The holding instance reciprocalGeneratorCert_holds is the concrete witness consumed there.
In the forcing chain this sits under T5 (J-uniqueness via the symmetric cost form) and T6 (φ as the self-similar fixed point of x=1+1/x). It does not itself re-prove uniqueness of J among all candidate costs; it packages the reciprocal generator that makes the two forcings talk about one object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.