Foundation Universal Forcing Reciprocal Generator Recip Shift Fixed Iff

The reciprocal-shift fixed point

The golden ratio, usually written φ, is the number that satisfies the equation x = 1 + 1/x. Multiplying both sides by x gives x² = x + 1, and the positive solution is φ = (1 + √5)/2, approximately 1.618. The equation itself describes a self-similarity: a rectangle with sides in the ratio φ to 1 can be divided into a square and a smaller rectangle with the same proportions. This property appears throughout classical geometry, from the pentagon to the Fibonacci sequence, where the ratio of successive terms approaches φ.

The declaration recipShift_fixed_iff states a uniqueness result about this equation. It considers the map g(x) = 1 + 1/x, which is called the reciprocal-shift because it takes a number, takes its reciprocal, and adds 1. The theorem proves that among all real numbers greater than 1, the equation g(x) = x has exactly one solution, and that solution is φ. In other words, the golden ratio is not just one possible self-similar scaling; within this framework, it is the only one above 1.

This result is part of a broader structure in Recognition Science, a framework that models physical structure from a discrete record of events called a ledger. Within this framework, the reciprocal involution ι(x) = 1/x plays a central role: it is the symmetry that exchanges a quantity with its reciprocal. The framework proves that the recognition cost function J, which measures the cost of a recognition event, is symmetric under this involution, so J(1/x) = J(x). The fixed point of the involution itself, the number satisfying x = 1/x, is the unit 1, which is also the unique point where the cost J is zero.

The reciprocal-shift map g(x) = 1 + 1/x is a close cousin of this involution. Its fixed-point equation is exactly the self-similarity constraint x = 1 + 1/x. The theorem recipShift_fixed_iff proves that this equation has a unique solution above 1, namely φ. This is the sharpest form of the bridge between the cost and the scale: the same involution family pins down both the unit (as the fixed point of ι) and the golden ratio (as the fixed point of 1 + ι). The framework's machine-checked library of formal theorems records this result as a proved statement, not a conjecture.

The practical consequence is that the golden ratio is not an arbitrary constant in this framework. It is forced by the structure of the reciprocal involution and the requirement of a unique self-similar scaling above unity. The theorem does not claim that the golden ratio is the only fixed point of the reciprocal-shift map overall; it restricts attention to numbers greater than 1. It also does not claim that the reciprocal-shift map is the only way to derive φ, nor that the framework's cost function J is the only possible cost function. Those are separate results with their own conditions.

/-- `φ` is the **unique** fixed point of the `ι`-shift among reals `> 1`. -/
theorem recipShift_fixed_iff {x : ℝ} (hx : 1 < x) :
    recipShift x = x ↔ x = Constants.phi := by
  unfold recipShift recip
  have hx0 : (0 : ℝ) < x := lt_trans one_pos hx
  have hxne : x ≠ 0 := ne_of_gt hx0
  constructor
  · intro h
    have hexp : (1 + x⁻¹) * x = x + 1 := by
      rw [add_mul, one_mul, inv_mul_cancel₀ hxne]
    have hmul : (1 + x⁻¹) * x = x * x := by rw [h]
    rw [hexp] at hmul
    have hsq : x ^ 2 = x + 1 := by rw [pow_two]; linarith [hmul]
    exact (PhiSupport.phi_unique_pos_root x).mp ⟨hsq, hx0⟩
  · intro h; subst h
    have h := PhiSupport.phi_fixed_point
    rw [one_div] at h
    exact h.symm

/-- `J` is invariant under the reciprocal involution: `J(ι x) = J(x)`. This is
`Cost.Jcost_symm`, here phrased as a property of `recip`. -/
theorem jcost_recip_symmetric {x : ℝ} (hx : 0 < x) :
    Cost.Jcost (recip x) = Cost.Jcost x := by
  unfold recip
  exact (Cost.Jcost_symm hx).symm

/-- **The involution's fixed point is the cost's zero.** For positive `x`,
`ι x = x ↔ J x = 0` — both hold iff `x = 1`. So `ι`'s own fixed point is not
arbitrary: it is the unit, the unique point of zero recognition cost. This is
the sharp form of the cost side — not merely that `J` is `ι`-symmetric, but that
the symmetry axis of `ι` coincides with the null set of `J`. -/
theorem recip_fixed_iff_cost_zero {x : ℝ} (hx : 0 < x) :
    recip x = x ↔ Cost.Jcost x = 0 := by
  rw [recip_fixed_iff hx, Cost.Jcost_eq_zero_iff x hx]

/-- **One involution, two constants.** The reciprocal involution `ι` pins both
fundamental quantities of the framework through its fixed points:

* the fixed point of `ι` itself is the unit `1`, which is exactly the zero of
  the recognition cost `J` (the no-cost point);
* the fixed point of the affine shift `1 + ι` is the golden ratio `φ`, the
  scale.

This is the sharpest form of the bridge. The unit and the scale — the two
constants the whole framework is built from — are the two fixed points of one
involution family: `ι` fixes the unit (= `J`'s null point), and `1 + ι` fixes
`φ`. -/
theorem recip_pins_unit_and_scale :
    (∀ x : ℝ, 0 < x → (recip x = x ↔ Cost.Jcost x = 0))
    ∧ (∀ x : ℝ, 1 < x → (recipShift x = x ↔ x = Constants.phi)) :=
  ⟨fun _ hx => recip_fixed_iff_cost_zero hx,
   fun _ hx => recipShift_fixed_iff hx⟩

What this page does not claim

The theorem does not claim that φ is the only fixed point of the reciprocal-shift map overall, only among numbers greater than 1. The theorem does not claim that the reciprocal-shift map is the only way to derive the golden ratio. The theorem does not claim that the cost function J is the only possible cost function satisfying the framework's axioms.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/UniversalForcing/ReciprocalGenerator.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: