repMax_strictMono
plain-language theorem explainer
The rep-max function on the phi-ladder is strictly increasing for natural-number rungs. Sports scientists modeling strength training with Recognition Science would cite this to confirm higher rungs produce strictly higher maximum loads. The proof is a short term-mode algebraic reduction that unfolds the power definition, invokes positivity of phi^k, and closes with linear arithmetic on the known inequality 1 < phi.
Claim. For every natural number $k$, the rep-max function $r$ on the phi-ladder satisfies $r(k) < r(k+1)$, where $r(k) = phi^k$ and $phi > 1$ is the golden ratio.
background
The module derives peak performance in sports from the phi-ladder, modeling 1RM and multi-rep maxima via powers of the golden ratio with empirical ratios 1RM/5RM falling in (phi^0.3, phi^0.4). The rep-max function encodes rung-dependent load scaling. Upstream, the lemma one_lt_phi establishes 1 < phi, quoted as 'φ > 1: The golden ratio is strictly greater than 1.' This rests on the self-similar fixed-point property of phi in the foundation.
proof idea
The term proof unfolds repMax to its power expression, applies pow_pos to obtain positivity of phi^k, rewrites the successor case via pow_succ, and closes with linarith instantiated by mul_lt_mul_of_pos_left applied to one_lt_phi.
why it matters
This supplies the strict-mono component of peakPerformanceCert, which bundles phi ratio, monotonicity, and positive hypertrophy exponent beta = 1/(2 phi). It applies the phi-ladder (T6 self-similar fixed point) to strength-training dose-response, aligning with the universal aging exponent and the alpha band. No open scaffolding remains in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.