exclusivity_model_independent
plain-language theorem explainer
The golden ratio is the unique positive real number satisfying the equation x squared equals x plus one. Researchers deriving self-similar fixed points in Recognition Science cite this to confirm model-independent exclusivity of phi. The proof applies the positive-root uniqueness lemma directly to the equation and positivity hypotheses.
Claim. Let $phi$ denote the golden ratio. For every real number $x > 0$, if $x^2 = x + 1$, then $x = phi$.
background
The PhiSupport.Lemmas module supplies elementary golden-ratio facts for certificate constructions. These include the relation $phi^2 = phi + 1$ from Mathlib, the fixed-point identity $phi = 1 + 1/phi$, and uniqueness of the positive root of $x^2 = x + 1$. The local setting restricts to real algebra with no model-specific assumptions. The upstream Constants structure from LawOfExistence bundles CPM constants including the phi field referenced in the statement.
proof idea
The proof introduces x with the positivity and equation hypotheses. It invokes the lemma phi_unique_pos_root x and matches the supplied conditions via mp to obtain the conclusion that x equals Constants.phi.
why it matters
This theorem supplies the model-independent exclusivity of phi as the unique positive solution to the self-similarity constraint, per the Phase 3 derivation note. It anchors the T6 step forcing phi as the self-similar fixed point in the unified forcing chain. No downstream uses appear yet, leaving open its role in later mass-ladder or constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.