intensityAtRung_pos
plain-language theorem explainer
The result establishes that intensity at every natural-number rung k on the phi-ladder is strictly positive. Strength-training researchers cite it when confirming that all canonical schemes from 1RM to deload zones remain above zero. The argument is a term-mode reduction that unfolds the definition and applies positivity of phi to the negative integer power via zpow_pos before closing with linarith.
Claim. For every natural number $k$, the intensity at rung $k$ on the phi-ladder satisfies $0 < I(k)$, where $I(k) = 1 · ϕ^{-k}$ and $ϕ$ is the golden-ratio fixed point.
background
The Lifting Program Design module extends the Recognition Science framework to strength-training schemes by anchoring them to the phi-ladder of intensities. Intensity at rung $k$ is defined as reference intensity (normalized to 1) times $ϕ$ raised to the negative integer $k$, placing rung 0 at 100% 1RM, rung 1 near 61.8%, rung 2 near 38.2%, and rung 3 near 23.6%. The module states that every documented peak-strength scheme sits within half a rung of these anchors.
proof idea
The proof unfolds intensityAtRung and referenceIntensity to expose the product with $ϕ^{-k}$. It applies zpow_pos using the positivity hypothesis from the Constants structure, then closes the inequality with linarith.
why it matters
This supplies the intensity_pos field inside the liftingProgramCert definition and is invoked directly by intensityAtRung_strictly_decreasing. It anchors the sport layer to the phi-ladder (T6 self-similar fixed point) and supports the canonical band claim without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.