Meta Ledger Uniqueness Cost Fixed Point Is Phi

The fixed point

The golden ratio φ = (1 + √5)/2 is the unique positive solution to the equation x² = x + 1. That equation has a long classical life: it defines the proportion that divides a segment so the whole is to the longer part as the longer is to the shorter, and it appears in pentagon geometry and in the Fibonacci sequence as the limit of successive ratios. The number is irrational, and its continued fraction is the simplest possible, all ones.

The equation x² = x + 1 is also a fixed-point condition, and that is where the machine-checked result enters. In Recognition Science, a ledger (a discrete record of events) assigns a cost (a forced penalty for each recognition event) to comparisons between quantities. The framework's central cost function J(x) = (x + 1/x)/2 - 1 has a symmetry: J(x) = J(1/x), so a value and its reciprocal pay the same cost. The fixed point of that symmetry, where x = 1/x, would be 1, but the relevant fixed point for the ledger's scaling turns out to be the positive solution of x² = x + 1, which is φ.

The declaration cost_fixed_point_is_phi in the framework's machine-checked library of formal theorems proves exactly this: for any positive real x, if x² = x + 1, then x = φ. It is a direct restatement of the classical uniqueness theorem for that quadratic, and it is proved with no additional axioms beyond the standard logical ones. The proof is short: the quadratic has at most two roots, and φ is the positive one.

What the declaration does not claim is broader. It does not say that the cost function J is the only possible cost function, nor that the ledger's structure is unique. Those are separate claims, and in the framework they rest on other theorems, not on this one. The fixed-point result pins down one number, φ, as the unique positive solution to a specific equation. It does not by itself force the golden ratio into physics, nor does it prove that any real system must use this cost. It is a lemma, not a law of nature.

In Recognition Science, this lemma is one component of a larger uniqueness argument: the framework aims to show that its ledger, with ratio φ, dimension 3, and cycle length 8, is the unique discrete conservative structure. That full claim is assembled from separate proofs for each component. The fixed-point theorem is the φ part. The reader who wants to know why the golden ratio appears in the framework's account should look at this lemma as the precise, narrow answer: it is the unique positive number satisfying x² = x + 1, and the cost symmetry picks out that equation.

/-- φ is the unique positive solution to x² = x + 1. -/
theorem phi_unique_fixed_point :
    ∀ x : ℝ, x > 0 → x^2 = x + 1 → x = phi := by
  intro x hx hEq
  -- x² = x + 1 ⟹ x² - x - 1 = 0
  have h1 : x^2 - x - 1 = 0 := by linarith

  -- Factorization: x^2 - x - 1 = (x - phi) * (x - psi)
  let psi := (1 - Real.sqrt 5) / 2
  have h_factor : x^2 - x - 1 = (x - phi) * (x - psi) := by
    unfold phi psi
    ring_nf
    rw [Real.sq_sqrt (by norm_num)]
    ring

  rw [h_factor] at h1
  cases mul_eq_zero.mp h1 with
  | inl h => exact sub_eq_zero.mp h
  | inr h =>
    have h_psi_neg : psi < 0 := by
      unfold psi
      have hsqrt : Real.sqrt 5 > 1 := by
        rw [← Real.sqrt_one]
        exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
      linarith
    have h_x_psi : x = psi := sub_eq_zero.mp h
    rw [h_x_psi] at hx
    linarith -- Contradiction: x > 0 but psi < 0

/-- The cost function fixed point is uniquely φ. -/
theorem cost_fixed_point_is_phi :
    ∀ x : ℝ, x > 0 →
    (x^2 = x + 1) → x = phi := by
  exact phi_unique_fixed_point

What this page does not claim

The declaration does not prove that the cost function J is the only possible cost function. The declaration does not by itself force the golden ratio into physical law. The declaration does not establish the uniqueness of the full ledger structure, which depends on separate proofs for dimension and cycle length.

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/Meta/LedgerUniqueness.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: