phiScale_zero
plain-language theorem explainer
The theorem states that scaling any real number x by phi to the power zero returns x unchanged. Researchers working on the phi-ladder hypothesis in Recognition Science would cite this as the identity element of the scaling operation. The proof is a one-line wrapper that applies the simp tactic to the definition of phiScale.
Claim. For every real number $x$, $x · ϕ^0 = x$.
background
The module states the φ-ladder hypothesis as an explicit assumption: privileged physical scales satisfy X = X₀ · ϕⁿ for integer n. This generates empirical predictions for particle masses, timescales, and amplitudes. The upstream definition states that phiScale(n, x) := x * phi^n and notes that φ-scaling is a group action on the reals.
proof idea
The proof is a one-line wrapper. It applies the simp tactic to the definition of phiScale, which unfolds phiScale 0 x directly to x * phi^0 and reduces to x.
why it matters
This supplies the identity case for the φ-scaling group action and is invoked in the proof of phiScale_neg to obtain the inverse property. It supports the integer rung structure required by the φ-ladder hypothesis in the RRF module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.