phi_is_cost_fixed_point
plain-language theorem explainer
The lemma records that the golden ratio φ satisfies φ = 1 + 1/φ inside the Recognition Science constants bundle. Modelers of self-similar cost structures or phi-ladder fixed points would cite it when invoking the algebraic root. The proof is a one-line wrapper that applies the upstream algebraic identity from PhiSupport.
Claim. The golden ratio satisfies the equation $φ = 1 + 1/φ$.
background
In Recognition Science the constant φ is introduced as the positive self-similar fixed point of the map x ↦ 1 + 1/x. The Constants structure packages φ together with the other CPM parameters Knet, Cproj, Ceng and Cdisp. Cost is defined as the abbreviation Quantity CostUnit, locating the fixed-point statement inside cost measurements on the phi-ladder.
proof idea
The proof is a one-line wrapper that applies the theorem phi_fixed_point from IndisputableMonolith.PhiSupport.Lemmas via the simpa tactic.
why it matters
The result supplies the algebraic anchor for φ required by the self-similar fixed-point step (T6) in the forcing chain and by the Recognition Composition Law. It supports downstream constructions that raise φ to integer powers for mass formulas and Berry thresholds. No immediate parent theorems are recorded in the used-by list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.