repMaxRatio
plain-language theorem explainer
The theorem states that rep-max values on consecutive rungs of the phi-ladder stand in the ratio phi. Strength-training modelers deriving universal hypertrophy exponents from Recognition Science would cite this when linking 1RM to 5RM ratios. The proof is a one-line algebraic reduction that unfolds the power definition of rep-max and normalizes the ratio via successor exponent and ring simplification.
Claim. For every natural number $k$, the ratio of rep-max at rung $k+1$ to rep-max at rung $k$ equals the golden ratio $phi$, where rep-max at rung $k$ is $phi^k$.
background
In the Sports.PeakPerformanceFromPhiLadder module the rep-max function is defined as $phi^k$ for natural rung index $k$. This sits inside the Recognition Science derivation of strength training, where consecutive rep-max rungs differ by $phi^{1/n}$ for rep count $n$, and the universal hypertrophy exponent is $beta = 1/(2 phi)$. The module imports Constants and uses the phi value forced as the self-similar fixed point in the T0-T8 chain. Upstream results supply multiple rung maps (lepton, quark, ore-class, anchor) that are not invoked here; the immediate predecessor is the rep-max definition itself.
proof idea
The term proof unfolds rep-max to obtain $phi^{k+1}/phi^k$, invokes positivity of $phi^k$ to justify division, rewrites the successor power, applies the division-equivalence lemma, and finishes with ring normalization.
why it matters
This supplies the phi-ratio field inside the peakPerformanceCert record that assembles the full certificate for the sports module. It directly instantiates the phi fixed-point (T6) and eight-tick octave structure for the hypertrophy dose-response, where the same exponent $1/(2 phi)$ appears in aging models. The result closes the algebraic link between the phi-ladder and empirical 1RM/5RM ratios reported in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.