phi
plain-language theorem explainer
The definition supplies the golden ratio φ = (1 + √5)/2 as a real number. Researchers deriving constants from the Meta-Principle in Recognition Science cite it as the self-similar fixed point. The implementation is a direct noncomputable assignment of the closed-form expression.
Claim. Define the golden ratio by the equation $φ = (1 + √5)/2$.
background
The module establishes the Meta-Principle that nothing cannot recognize itself, so recognition requires a recognizer and empty recognition is impossible. This forces a double-entry ledger structure whose self-similar closure yields the golden ratio. The definition supplies the explicit real value used downstream to obtain constants such as c, ℏ, G, and α.
proof idea
The declaration is a direct noncomputable definition that assigns the algebraic expression (1 + Real.sqrt 5) / 2.
why it matters
This definition supplies the golden ratio required for self-similar closure after the ledger step in the Meta-Principle chain. It aligns with the forcing chain landmark where φ is the self-similar fixed point. No downstream uses are recorded in the current module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.