liftingProgramCert
plain-language theorem explainer
The declaration constructs a certificate asserting that intensities on the phi-ladder remain positive at every rung, multiply by phi inverse at each successive rung, and decrease strictly. Strength-training researchers cite it to locate classical schemes such as 5x5 and 3x3 as integer steps on the Recognition Science intensity ladder. The construction is a direct record that supplies three pre-proved theorems for the structure fields.
Claim. The lifting-program certificate asserts that the intensity function $I$ on natural-number rungs satisfies $0 < I(k)$ for all $k$, $I(k+1) = I(k) / phi$, and $I(k+1) < I(k)$.
background
The Sport.LiftingProgramDesign module defines intensities on the phi-ladder anchored at 1RM: rung 0 at 100 percent, rung 1 at 100/phi approximately 61.8 percent, rung 2 at 100/phi squared approximately 38.2 percent. The intensityAtRung function is obtained by scaling a reference intensity by phi to the negative integer power of the rung index, as shown by unfolding in the upstream positivity theorem.
proof idea
The definition constructs the LiftingProgramCert record by direct assignment of its three fields to the upstream theorems intensityAtRung_pos, intensityAtRung_succ_ratio, and intensityAtRung_strictly_decreasing.
why it matters
This definition supplies the canonical certificate for the lifting-program layer, extending the structural F8 wrapper to program design on the phi-ladder. It justifies placement of 5x5, 3x3, and 1RM schemes within the documented intensity bands. No downstream uses appear yet, leaving open its role in larger training-optimization results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.