phiRung_add
plain-language theorem explainer
The lemma establishes that the φ-ladder scaling satisfies the additive exponent rule: phiRung(m + n) equals the product phiRung m times phiRung n for any integers m and n. Workers composing masses or energies from multiple rungs on the Recognition Science ladder would cite this identity when adding contributions. The proof is a one-line term wrapper that unfolds the definition and invokes the standard zpow addition identity for nonzero bases.
Claim. For integers $m, n$, let $r(k) = φ^k$ denote the scaling factor at rung $k$ on the φ-ladder. Then $r(m + n) = r(m) · r(n)$.
background
The RS-native units module organizes all derived quantities on the φ-ladder, where each integer rung multiplies the base scale by φ. The definition phiRung(n) := φ^n supplies the explicit scaling for masses, energies, lengths, and times. The module sets c = 1 in voxel/tick units and fixes all dimensionless ratios by powers of φ alone.
proof idea
The term proof first simplifies the definition of phiRung to the power expression, then applies the lemma zpow_add₀ (which requires the base nonzero) to obtain the product identity directly.
why it matters
The result underwrites consistent rung arithmetic throughout the constants module and its siblings (Mass, Energy, Length). It aligns with the self-similar fixed-point scaling forced at T6 of the unified forcing chain and supports the mass formula that places quantities at integer rungs offset by gap(Z). No open scaffolding is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.