PhiPow_one
plain-language theorem explainer
PhiPow_one establishes that the exponential wrapper PhiPow recovers the base constant phi exactly at exponent 1. Researchers building inductive arguments on the phi-ladder or binary scales in Recognition Science would cite this base case. The proof unfolds the definition, asserts positivity of phi, and reduces via the exp-log identity together with a multiplication lemma.
Claim. $Phi(1) = phi$, where $Phi(x) := exp(log(phi) * x)$ and $phi$ denotes the golden-ratio constant supplied by the Constants structure.
background
The module RecogSpec.Scales supplies binary scales and phi-exponential wrappers. PhiPow is the noncomputable wrapper $Phi(x) := Real.exp(Real.log(Constants.phi) * x)$. The Constants structure bundles the CPM constants and supplies the positivity fact phi_pos. The upstream one_mul lemma from ArithmeticFromLogic supplies a multiplication identity that participates in the final simplification step.
proof idea
The proof first unfolds the definition of PhiPow. It then introduces the hypothesis 0 < Constants.phi via Constants.phi_pos. The final simp call with one_mul and Real.exp_log hφ reduces the expression directly to phi.
why it matters
This supplies the unit-exponent base case for the PhiPow wrapper inside the scales module, supporting later constructions on the phi-ladder. It aligns with the T6 self-similar fixed-point requirement for phi and the phi-exponential mass formula. No downstream uses are recorded, so the lemma functions as local scaffolding rather than a high-traffic interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.