PhiPow_add
plain-language theorem explainer
PhiPow_add records that the φ-power function satisfies the exponential addition law φ^{x+y} = φ^x φ^y over the reals. Workers on the phi-ladder in Recognition Science cite this when chaining scale factors. The short tactic proof unfolds the definition to Real.exp and reduces the exponent addition via ring and the exp_add lemma.
Claim. Let φ denote the golden ratio. Define the φ-power wrapper by φ^x := exp((log φ) ⋅ x). Then φ^{x+y} = φ^x ⋅ φ^y for all real x, y.
background
The module RecogSpec.Scales supplies binary scales and φ-exponential wrappers. PhiPow is the noncomputable wrapper PhiPow(x) := Real.exp(Real.log(Constants.phi) ⋅ x). The upstream Constants structure from LawOfExistence bundles the CPM constants, with phi appearing as the self-similar fixed point.
proof idea
Unfold PhiPow to expose the exponential. Apply ring to obtain linearity of the log multiplier on the sum. Finish with simp using Real.exp_add.
why it matters
The lemma supplies the homomorphism property required for composing φ-powers on the phi-ladder. It directly supports the T6 fixed-point and T7 octave constructions in the forcing chain. No downstream uses appear yet, leaving open its role in explicit mass or alpha-band calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.