IndisputableMonolith.PhiSupport.Lemmas
PhiSupport.Lemmas supplies the closed-form definition of the golden ratio φ together with basic algebraic properties including positivity, non-zero status, the relation φ² = φ + 1, and the fixed-point property. Astrophysicists cite these lemmas when anchoring φ-tier calculations inside mass-to-light derivations. The module consists of direct definitions and short verifications drawn from Mathlib golden-ratio theory plus the RS constants import.
claimThe golden ratio is given by the closed form $φ = (1 + √5)/2$, satisfying $φ > 1$, $φ ≠ 0$, $φ² = φ + 1$, and the fixed-point equation that follows from the self-similar solution of the Recognition Composition Law.
background
The module imports IndisputableMonolith.Constants, whose sole documented object is the fundamental RS time quantum τ₀ = 1 tick. It introduces the sibling objects phi_def (closed form), one_lt_phi, phi_ne_zero, phi_squared, phi_fixed_point, and exclusivity_model_independent. These sit inside the PhiSupport domain and supply the algebraic substrate for the φ-ladder that appears in mass formulas and recognition-cost weighting.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The lemmas feed the three independent M/L derivations in Astrophysics.MassToLight (recognition-cost weighting), NucleosynthesisTiers (φ-tier nuclear densities), ObservabilityLimits (recognition-length bounds), and StellarAssembly (collapse cost differential). They close the basic φ-support required before any φ-ladder rung or mass formula can be stated.
scope and limits
- Does not derive numerical values for α or G.
- Does not contain the T0–T8 forcing chain.
- Does not perform any astrophysical integration or simulation.
- Does not address model-dependent exclusivity beyond the listed lemma.