flameSpeedCert
plain-language theorem explainer
The flame-speed-from-φ-ladder certificate assembles positivity, exact φ-multiplication, strict monotonicity, and adjacent-ratio equality for the laminar flame speed function into one structure. Combustion theorists would cite it to confirm the parameter-free scaling prediction across integer rungs of chain-branching intensity. The definition is a direct construction that supplies the four component theorems already established in the same module.
Claim. The structure FlameSpeedCert asserts that the function flameSpeed : ℕ → ℝ satisfies ∀k ∈ ℕ, flameSpeed k > 0; ∀k, flameSpeed(k+1) = flameSpeed k ⋅ φ; ∀k, flameSpeed k < flameSpeed(k+1); and ∀k, flameSpeed(k+1)/flameSpeed k = φ, where φ denotes the golden ratio.
background
The module defines laminar flame speed on the φ-ladder: each integer step in chain-branching intensity multiplies S_L exactly by φ. The function flameSpeed k gives the speed at rung k, constructed as referenceSpeed scaled by φ^k. FlameSpeedCert is the structure that packages four properties: speed_pos (positivity at every rung), one_step_ratio (exact multiplication by φ), strictly_increasing (strict monotonicity), and adjacent_ratio_eq_phi (ratio exactly φ).
proof idea
The definition constructs the FlameSpeedCert instance by direct field assignment: speed_pos receives flameSpeed_pos, one_step_ratio receives flameSpeed_succ_ratio, strictly_increasing receives flameSpeed_strictly_increasing, and adjacent_ratio_eq_phi receives flameSpeed_adjacent_ratio. Each component theorem was proved by unfolding the flameSpeed definition, applying the power rule, using positivity of φ, and performing field simplification.
why it matters
This definition supplies the complete certificate realizing the module's structural claim that adjacent-rung flame speeds scale exactly by φ with no fitted parameters. It closes the Lean formalization of the empirical bench (methane-air rung 0, ethylene-air rung 1, hydrogen-air rung 2) described in the module documentation. In the Recognition Science framework it instantiates the self-similar fixed-point scaling forced by phi (T6) inside the combustion domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.