information_balance_gives_phi
plain-language theorem explainer
The declaration establishes that the golden ratio φ satisfies φ² = φ + 1 as the equilibrium ratio of mass-event to light-event counts under J-cost minimization in the information ledger. Astrophysicists working on recognition-bounded observability and mass-to-light ratios would cite it to anchor M/L derivations. The proof is a direct term-mode instantiation of φ that splits the conjunction and invokes the algebraic identity phi_squared.
Claim. There exists a real number ratio equal to the golden ratio φ such that ratio² = ratio + 1, where φ arises as the unique fixed point of the J-cost recursion balancing mass information I_mass = n_mass × J_bit and light information I_light = n_light × J_bit under total conservation.
background
The module derives observable mass-to-light ratios from recognition constraints: photon flux must exceed F_threshold ~ E_coh/τ_0 and mass assembly is limited by coherence volume V ~ l_rec³. Total J-cost J_total = J_mass(M) + J_light(L) is minimized subject to these bounds, yielding M/L ratios in {φ^n : n ∈ [0, 3]} with typical value ≈ φ. J_bit is the per-event information unit defined as Real.log φ. The local setting is Strategy 3 of Recognition-Bounded Observability, which aligns with geometric constraints from l_rec and τ_0.
proof idea
The proof is a term-mode construction. It instantiates φ as the witness for the existential quantifier, applies constructor to split the conjunction into two goals, uses rfl for the first equality, unfolds the definition of φ, and applies the phi_squared lemma from PhiSupport to discharge the quadratic relation.
why it matters
This result closes the information-balance argument that produces the φ equilibrium ratio for observable stellar systems, supporting the module's main claim that M/L ∈ {φ^n : n ∈ [0, 3]}. It connects directly to the self-similar fixed-point property of φ (T6 in the forcing chain) and the Recognition Composition Law. No downstream uses are recorded, but the declaration supplies the algebraic anchor for equilibrium ratios in the astrophysics derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.