phi_power_compose
plain-language theorem explainer
The theorem asserts that integer powers of the golden ratio φ multiply by adding their exponents. Researchers building the phi-ladder and cascade bounds in the StillnessGenerative module cite it to compose rung costs. The proof is a one-line term that invokes the Mathlib zpow_add₀ lemma on the positivity of φ and symmetrizes the result.
Claim. For all integers $a$ and $b$, $φ^a · φ^b = φ^{a+b}$, where $φ$ is the positive golden-ratio fixed point from the T6 self-similar closure.
background
The StillnessGenerative module derives non-trivial structure from the unique zero-defect ground state x=1 by applying the T4-T7 forcing chain. Non-uniformity on the closed geometric scale sequence forces every non-trivial entry to be a power of φ, with positive and negative rungs related by J-cost symmetry. The phi_ladder is constructed directly from these powers, and the Recognition Composition Law governs their J-costs.
proof idea
The proof is a one-line term wrapper that applies zpow_add₀ to PhiForcing.phi_pos.ne' and then takes the symmetric form to obtain the stated multiplication order.
why it matters
It supplies the algebraic composition rule required by ladder_cascade_bound, which unfolds phi_ladder and rewrites the summed exponent to bound the J-cost of the composite rung via the Recognition Composition Law. The result instantiates the Fibonacci cascade step in the module's T0-T8 derivation chain that populates the full ladder from the ground-state instability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.