FlameSpeedCert
plain-language theorem explainer
The FlameSpeedCert structure bundles four properties of the flame speed function on the phi-ladder: positivity at every rung, exact multiplication by phi on each integer step, strict increase, and adjacent ratio equality to phi. Combustion modelers comparing laminar speeds across fuels would cite it for the parameter-free structural prediction. The definition is a direct bundling of lemmas that follow algebraically from the exponential form of flameSpeed.
Claim. A certificate asserting that the flame speed function $S(k)$ on the phi-ladder satisfies $S(k)>0$, $S(k+1)=S(k)·φ$, $S(k)<S(k+1)$, and $S(k+1)/S(k)=φ$ for every natural number $k$, where $S(k)$ is defined as the reference speed scaled by $φ^k$.
background
The module shows that laminar flame speed follows the phi-ladder: each integer step in chain-branching intensity multiplies speed by exactly φ. The upstream flameSpeed definition sets this as referenceSpeed times φ to the power k. The PrimitiveDistinction.from theorem supplies the foundational structural conditions derived from seven axioms that underwrite the ladder construction.
proof idea
This is a structure definition that packages four properties. The fields are filled directly from the lemmas flameSpeed_pos, flameSpeed_succ_ratio, flameSpeed_strictly_increasing, and flameSpeed_adjacent_ratio, each obtained by algebraic reduction on the exponential definition of flameSpeed.
why it matters
The certificate supplies the bundled properties required by the downstream flameSpeedCert definition. It fills the phi-ladder step in the Recognition framework, where φ is the self-similar fixed point forced at T6 and the eight-tick octave at T7 supports the rung indexing. The exact ratio prediction aligns with the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.