intensityAtRung_succ_ratio
plain-language theorem explainer
The theorem states that intensity on the phi-ladder at rung k+1 equals intensity at rung k multiplied by phi inverse. Strength-training modelers cite it to derive the exact ratio between consecutive rungs in canonical programs such as 5x5 or 3x3. The proof is a short tactic sequence that unfolds the definition, invokes phi nonzero to justify the exponent rule, and reduces the rest by ring and zpow_add.
Claim. Let $I(k)$ be the intensity at natural-number rung $k$ on the phi-ladder, given by $I(k) = I_0 phi^{-k}$ with reference intensity $I_0$. Then $I(k+1) = I(k) phi^{-1}$ holds for every $k$.
background
The module develops lifting-program design as integer steps on the phi-ladder of intensity. The central definition is intensityAtRung k := referenceIntensity * phi ^ (-(k : Z)), where rung 0 anchors at 1RM and each higher rung scales by successive powers of phi inverse. MODULE_DOC records the predicted ladder: rung 1 at 100/phi, rung 2 at 100/phi squared, etc., placing classical 5x5 and 3x3 schemes near rungs 1-2. Upstream lemmas supply phi_ne_zero from Constants, NumberTheory.PhiLadderLattice, and PhiSupport.Lemmas, each stating phi > 0 and hence nonzero.
proof idea
The tactic proof unfolds intensityAtRung, obtains phi_ne_zero from Constants, then proves the exponent identity phi^(-(k+1)) = phi^(-k) * phi^{-1} by rewriting the exponent as -(k) + (-1) and applying zpow_add_0. A cast lemma equates (k+1 : Z) with (k : Z) + 1. The final ring step closes the equality.
why it matters
This ratio is the one-step relation required by the liftingProgramCert structure, which bundles intensity_pos, one_step_ratio, and strictly_decreasing into a single certificate. It directly supports the downstream theorem intensityAtRung_strictly_decreasing via rewrite. In the Recognition framework the result instantiates the self-similar scaling forced by T6 (phi as fixed point) and the eight-tick octave structure, confirming that documented strength schemes lie within half-rung of the canonical anchors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.