kcat_ratio
plain-language theorem explainer
The theorem states that consecutive turnover numbers on the phi-ladder satisfy k_cat(k+1)/k_cat(k) = phi for every natural number k. Enzyme-kinetics modelers working inside Recognition Science cite it to fix the scaling across the five canonical classes. The proof is a short term reduction that unfolds the power definition, invokes positivity of phi^k, rewrites the division, and finishes by ring simplification.
Claim. For every natural number $k$, the ratio of turnover numbers satisfies $k_{cat}(k+1)/k_{cat}(k) = phi$, where the turnover number is defined by $k_{cat}(k) = phi^k$.
background
The module treats enzyme catalysis as an instance of J-cost minimization on the phi-ladder. Five canonical classes (oxidoreductase, transferase, hydrolase, lyase, isomerase) are identified with configDim D = 5. The turnover number k_cat is placed on this ladder so that adjacent-class ratios equal phi, consistent with the self-similar fixed point forced at T6. The supporting definition is the explicit power kcat(k : ℕ) : ℝ := phi^k.
proof idea
The term proof unfolds kcat to obtain phi^(k+1)/phi^k. It introduces the positivity fact (0 < phi^k) via pow_pos, rewrites the division equation with div_eq_iff, replaces the numerator exponent by pow_succ, and closes with the ring tactic.
why it matters
The result supplies the phi_ratio field inside EnzymeCatalysisCert, which also records the class count and positivity of kcat. It therefore completes the scaling step required by the B10 chemistry depth, linking directly to the Recognition Composition Law and the eight-tick octave. No open scaffolding remains for this particular ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.