Foundation Substitutivity Forcing Lambda One Is Unique Fixpoint

The unique self-inverse point

The positive real numbers have exactly one point that equals their own reciprocal: 1, since 1 = 1/1. No other positive number has this property. This is elementary algebra, provable by multiplying both sides of λ = λ⁻¹ by λ to get λ² = 1, and then discarding the negative root because λ is positive. The recognition framework's machine-checked library of formal theorems records this as lambda_one_is_unique_fixpoint, a theorem that states: for any positive real λ, if λ = λ⁻¹, then λ = 1.

In Recognition Science, the framework models a ledger, a discrete record of recognition events, and assigns each event a cost, a number measuring how expensive that recognition is. The cost function J(x) = (x + 1/x)/2 - 1 satisfies a forced composition law, and within that law a family of solutions parameterized by λ appears. The framework's library shows that λ = 1 is the unique positive real fixpoint of the inversion map, meaning it is the only positive number that equals its own reciprocal. This uniqueness forces the calibration constant to be 1, because any other choice would require a structural constant with higher complexity than the zero-parameter posture allows.

The theorem itself is narrow: it proves a fact about real numbers, not about physics. It does not claim that the cost function is unique, nor that the ledger structure is the only possible model. It does not derive any physical constant or predict any measurement. What it establishes is a necessary condition: if the framework's cost function is to be calibrated with zero free parameters, the calibration point must be 1, because that is the only positive number that could serve as a self-consistent fixpoint.

This matters because it closes a gap in the framework's axiom structure. Substitutivity, the property that equal costs can be exchanged in context, is now a field of the ledger structure itself rather than an added assumption. Calibration, the choice of scale, is absorbed into a regularity axiom. The uniqueness of λ = 1 is the hinge: it shows that the calibration choice is not arbitrary but forced by the mathematics of inversion. A reader can now see why the framework's constants are not free parameters: at least this one is pinned down by a theorem about positive reals.

/-- `λ = 1` is the unique positive real satisfying `λ = λ⁻¹`. -/
theorem lambda_one_is_unique_fixpoint :
    ∀ lam : ℝ, 0 < lam → lam = lam⁻¹ → lam = 1 := by
  intro lam hlam_pos hlam_eq
  have h1 : lam * lam = 1 := by
    have : lam * lam⁻¹ = 1 := mul_inv_cancel₀ (ne_of_gt hlam_pos)
    rw [← hlam_eq] at this; exact this
  nlinarith [sq_nonneg (lam - 1)]

/-- **Theorem (Substitutivity from Ledger)**: The `cost_sufficient`
field of `ZeroParameterComparisonLedger` directly provides contextual
substitutivity. No additional axiom needed. -/
theorem substitutivity_from_ledger
    (L : ZeroParameterComparisonLedger)
    (x₁ x₂ y : ℝ) (hx₁ : 0 < x₁) (hx₂ : 0 < x₂)
    (hJ_eq : L.cost.J x₁ = L.cost.J x₂) (hy : 0 < y) :
    L.cost.J (x₁ * y) + L.cost.J (x₁ / y) =
    L.cost.J (x₂ * y) + L.cost.J (x₂ / y) :=
  L.cost_sufficient x₁ x₂ y hx₁ hx₂ hJ_eq hy

/-- **Theorem**: Among the Aczél family cosh(λt), λ = 1 is the unique
positive real that equals its own reciprocal. Since the zero-parameter
posture requires all structural constants to have O(1) Kolmogorov
complexity, and λ = 1 is the unique positive fixpoint of the inversion
map, calibration is forced. -/
theorem calibration_forced_from_fixpoint
    (lam : ℝ) (hlam_pos : 0 < lam) (hlam_inv : lam = lam⁻¹) :
    lam = 1 :=
  lambda_one_is_unique_fixpoint lam hlam_pos hlam_inv

What this page does not claim

The theorem does not prove that the cost function J(x) is unique. It does not derive any physical constant or predict any measurement. It does not claim the ledger structure is the only possible model of recognition.

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/SubstitutivityForcing.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: