PhiPow
plain-language theorem explainer
PhiPow defines the real function phi^x as exp(log phi * x). Researchers deriving phi-ladder scalings or growth rates in Recognition Science cite this wrapper to obtain additivity and monotonicity. The definition is a direct one-line translation of the exponential using Mathlib's Real.exp and Real.log.
Claim. Define the map $xmapsto exp(log phi * x)$ for real $x$, where phi denotes the golden-ratio constant supplied by the CPM Constants bundle.
background
The module RecogSpec.Scales supplies binary scales together with phi-exponential wrappers. PhiPow realizes the self-similar scaling by the golden ratio that appears in the phi-ladder mass formula. It imports the Constants structure, an abstract bundle that packages the CPM constants Knet, Cproj, Ceng, Cdisp together with the non-negativity axiom on Knet.
proof idea
One-line definition that directly invokes Real.exp (Real.log (Constants.phi) * x). All algebraic properties are proved in downstream lemmas such as PhiPow_add and PhiPow_zero by unfolding the definition and applying ring and exp_add.
why it matters
PhiPow supplies the concrete exponential that feeds the phi-ladder used in mass formulas and the eight-tick octave. It is the base for PhiPow_add, PhiPow_zero, PhiPow_one and the tc_growth_holds lemma in the URC adapters. The definition therefore closes the gap between the abstract Constants bundle and the concrete scaling laws required by T6 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.