recipShift
plain-language theorem explainer
The reciprocal-shift map g(x) = 1 + 1/x on the reals packages the self-similarity constraint x = 1 + 1/x. Anyone forcing φ as the unique scale > 1 cites this map. It is a one-line definition: add one to the reciprocal involution ι(x) = x⁻¹.
Claim. Define the reciprocal-shift $g:\mathbb{R}\to\mathbb{R}$ by $g(x)=1+x^{-1}$. Fixed points of $g$ solve the self-similarity equation $x=1+1/x$.
background
This module treats the reciprocal involution ι(x)=x⁻¹ on the positive reals as the single generator beneath both the recognition cost J and the golden-ratio scale φ. The module doc states the program: J is exactly the ι-symmetric cost (J∘ι=J), and φ is the unique fixed point >1 of the ι-shift g(x)=1+ι(x).
The local reciprocal is recip x := x⁻¹. The present definition is the affine shift of that involution: g(x)=1+ι(x). Its fixed-point equation is the classical self-similarity constraint x=1+1/x that forces the golden ratio in the T6 step of the forcing chain.
Upstream, recip is the dual-recognition symmetry the framework is built on; involutivity and J-symmetry of ι are proved as sibling facts before uniqueness of the g-fixed point is stated.
proof idea
Pure definitional abbreviation: unfold to 1 + recip x, i.e. 1 + x⁻¹. No lemmas, no tactics. Downstream proofs unfold this name and rewrite with the known φ fixed-point identity φ = 1 + 1/φ.
why it matters
This map is the scale half of the reciprocal-generator story. Downstream, phi_is_recipShift_fixed shows φ solves g(φ)=φ; recipShift_fixed_iff shows uniqueness among reals >1; both feed recip_generates_cost_and_scale and recip_pins_unit_and_scale, which package the claim that one involution pins the unit (fixed point of ι, zero of J) and the scale (fixed point of 1+ι).
The certificate structure ReciprocalGeneratorCert records scale_unique and phi_solves in terms of this map. In the framework landmarks this is the concrete carrier of T6: φ forced as the self-similar fixed point of x ↦ 1+1/x, logically upstream of the glued OneLaw assembly of cost-form and hierarchy scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.