PhiPow_neg
plain-language theorem explainer
The lemma establishes the inversion rule for the φ-power wrapper: its value at -y equals the reciprocal of its value at y. Researchers extending the φ-ladder to negative rungs in Recognition Science scales would cite this identity. The proof is a one-line wrapper that instantiates the subtraction lemma at zero and simplifies with the zero case.
Claim. For any real number $y$, the φ-power function satisfies $f(-y) = 1/f(y)$, where $f(x) = e^{x log φ}$ and $φ$ is the golden ratio.
background
The module develops binary scales and φ-exponential wrappers. The φ-power wrapper is defined by $f(x) := exp(log(φ) · x)$, with φ drawn from Constants. It obeys the subtraction identity $f(x - y) = f(x)/f(y)$ and the normalization $f(0) = 1$.
proof idea
The proof instantiates the subtraction lemma at (0, y) to obtain f(0 - y) = f(0)/f(y). It then applies simplification with the zero case and the identity 0 - y = -y to reach the reciprocal form.
why it matters
This supplies the basic inversion property for the φ-power wrapper inside the scales module. It closes an algebraic prerequisite for handling negative exponents on the φ-ladder. No downstream theorems are recorded yet, but the result aligns with the φ-exponential constructions that support the Recognition Science mass formula and rung arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.