PhiPow
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.
claimDefine 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 in Recognition Science
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.
scope and limits
- Does not prove any functional equation; those are separate lemmas.
- Does not fix a numerical value for phi beyond the Constants bundle.
- Does not extend the domain beyond the reals.
- Does not address convergence or analytic continuation.
formal statement (Lean)
47noncomputable def PhiPow (x : ℝ) : ℝ := Real.exp (Real.log (Constants.phi) * x)
proof body
Definition body.
48