pith. machine review for the scientific record. sign in
theorem proved term proof high

phi_unique

show as:
view Lean formalization →

The declaration shows that the golden ratio φ is the unique positive real root of the equation x² = x + 1. Workers deriving constants from self-similar closure in recognition models cite this to eliminate alternative fixed points. The proof is a one-line wrapper that invokes the self-similarity forcing result.

claimThe unique positive real number $x$ satisfying $x^2 = x + 1$ equals the golden ratio $φ$.

background

The RRF foundation module treats the meta-principle as a theorem rather than an axiom: nothing cannot recognize itself, which forces a ledger structure whose self-similar closure yields φ. RRF itself is the local non-sealed recognition field interface, an abbreviation for maps from (Fin 4 → ℝ) to ℝ. The upstream lemma self_similarity_forces_phi states that self-similar ledger closure forces φ as the only positive solution to x² = x + 1 and supplies the quadratic-formula argument.

proof idea

The proof is a one-line wrapper that applies the theorem self_similarity_forces_phi, which reduces the quadratic x² - x - 1 = 0, invokes positivity to discard the negative root, and identifies the surviving root with φ.

why it matters in Recognition Science

This uniqueness result is invoked by the master theorem concrete_implies_no_alternatives and by the noFreeParameters theorem in InevitabilityEquivalence; together they close the chain from the meta-principle through ledger closure to unique constants. It realizes the T6 forcing step in which φ is fixed as the self-similar point, removing free parameters from the derivation of c, ħ, G and α.

scope and limits

formal statement (Lean)

 193theorem phi_unique : ∀ x : ℝ, 0 < x → x ^ 2 = x + 1 → x = phi :=

proof body

Term-mode proof.

 194  self_similarity_forces_phi
 195
 196end RRF.Foundation
 197end IndisputableMonolith

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.