PhiPow_sub
plain-language theorem explainer
PhiPow_sub establishes that the φ-power function obeys the subtraction rule PhiPow(x - y) = PhiPow(x) / PhiPow(y) for all real x and y. Researchers manipulating scale hierarchies and negative exponents in Recognition Science cite it when reducing differences on the φ-ladder. The proof unfolds the exponential definition then applies the ring lemma followed by a calc chain that invokes exp_add, exp_neg, and div_eq_mul_inv.
Claim. For all real numbers $x$ and $y$, let $PhiPow(z) := exp(log(φ) · z)$ where $φ$ is the golden-ratio constant. Then $PhiPow(x - y) = PhiPow(x) / PhiPow(y)$.
background
The module RecogSpec.Scales develops binary scales and φ-exponential wrappers. PhiPow is the noncomputable wrapper sending a real exponent z to exp(log(φ) · z), with φ drawn from the Constants structure. That structure bundles the abstract CPM constants (Knet, Cproj, Ceng, Cdisp) together with the nonnegativity hypothesis on Knet.
proof idea
The proof unfolds PhiPow, applies ring to obtain log(φ) · (x - y) = log(φ) · x + log(φ) · (-y), then runs a calc block. The block rewrites the left-hand exponential via exp_add, converts the negative factor with exp_neg, and finishes with div_eq_mul_inv.
why it matters
The lemma directly supports the sibling PhiPow_neg, which obtains the negation rule by specializing to x = 0. It supplies the additive subtraction property required for manipulations on the φ-ladder, feeding the Recognition Composition Law and the eight-tick octave steps in the T5–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.