Foundation Universal Forcing Reciprocal Generator Jcost Recip Symmetric

The reciprocal symmetry of cost

In mathematics, an involution is a function that is its own inverse: applying it twice brings you back to where you started. The reciprocal map on positive numbers, which sends x to 1/x, is the classic example. Its fixed point, the number that maps to itself, is 1, since 1/1 = 1. This map is so elementary that it appears throughout geometry, algebra, and number theory, often as a symmetry that reveals hidden structure.

In the Recognition Science framework, the cost function J(x) measures the price of recognizing a quantity x, with J(1) = 0 as the no-cost baseline. The declaration jcost_recip_symmetric proves a specific symmetry: for any positive x, J(1/x) = J(x). In plain language, recognizing a quantity and recognizing its reciprocal cost exactly the same. This is not a coincidence of the framework's design; it is a theorem, machine-checked in the framework's library, that follows from the defining properties of the cost function itself.

The power of this symmetry appears when it is combined with a second, related map. Consider the function g(x) = 1 + 1/x, which shifts the reciprocal by one. Its fixed points satisfy x = 1 + 1/x, the defining equation of the golden ratio φ ≈ 1.618. The framework proves that among numbers greater than 1, φ is the unique fixed point of this shifted map. Thus the same reciprocal involution that fixes the unit 1 also generates the golden ratio through its affine shift. The unit and the scale are two fixed points of one involution family.

This result is the sharpest form of a bridge the framework draws between cost and scale. The cost's symmetry axis, the point where cost is zero, coincides with the involution's fixed point at 1. The golden ratio, the framework's fundamental scale, is the unique fixed point of the shifted map. The declaration jcost_recip_symmetric is the cost-side half of this bridge, establishing the symmetry that makes the unit special. Its companion theorems, recip_fixed_iff_cost_zero and recipShift_fixed_iff, complete the picture by tying the fixed points to the cost's zero and to φ.

What this declaration does not claim is equally important. It does not state that the cost function is uniquely determined by this symmetry; the full uniqueness of J requires additional axioms beyond symmetry alone. It does not assert that the golden ratio is derived from the cost function, only that both share the same underlying reciprocal structure. And it says nothing about how this abstract symmetry connects to physical measurements; that bridge remains a separate, open question in the framework.

/-- `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

/-- `ι` is an involution on the positive reals. -/
theorem recip_involutive {x : ℝ} (_hx : 0 < x) : recip (recip x) = x := by
  simp [recip]

/-- `ι` has a unique fixed point among positive reals, namely the unit `1`. -/
theorem recip_fixed_iff {x : ℝ} (hx : 0 < x) : recip x = x ↔ x = 1 := by
  unfold recip
  have hxne : x ≠ 0 := ne_of_gt hx
  constructor
  · intro h
    have hsq : x * x = 1 := by
      have hmul : x⁻¹ * x = x * x := by rw [h]
      rw [inv_mul_cancel₀ hxne] at hmul
      exact hmul.symm
    nlinarith [hsq, hx]
  · intro h; subst h; simp

/-- `φ` 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

/-- **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]

What this page does not claim

The declaration does not prove that the cost function J is uniquely determined by reciprocal symmetry alone. The declaration does not claim that the golden ratio is derived from the cost function, only that both share the same reciprocal structure. The declaration does not make any statement about how this symmetry relates to physical measurements or experimental data.

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: