phiScale_add
plain-language theorem explainer
φ-scaling composes by adding the integer exponents, so that scaling a real by φ^m after scaling by φ^n recovers scaling by φ^{m+n}. Workers on the Recognition Science φ-ladder hypothesis cite the result when chaining scale factors for masses or timescales. The short term-mode proof unfolds the definition of phiScale and reduces the exponents via the additivity law for positive-base powers.
Claim. For integers $m,n$ and real $x$, the scaling map satisfies $x·φ^m·φ^n = x·φ^{m+n}$, where $φ$ denotes the golden ratio.
background
The φ-ladder hypothesis states that privileged physical scales obey $X = X_0 · φ^n$ for integer $n$. The auxiliary definition phiScale implements this map by the rule phiScale n x := x * φ^n. The present theorem supplies the composition law that turns phiScale into a group action of the integers under addition.
proof idea
The term proof first rewrites both sides by the definition of phiScale, producing the product x * φ^n * φ^m on the left. It then applies the library lemma zpow_add₀ (using positivity of φ) to replace the product of powers by a single power with summed exponent, followed by a commutativity step to finish the equality.
why it matters
The result is invoked directly by the sibling theorem phiScale_neg to establish the inverse property, thereby completing the group-action structure demanded by the φ-ladder hypothesis. That hypothesis is explicitly flagged in the module as an empirical claim rather than a derived truth, generating testable obligations for mass ladders and time scales within the RRF framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.