flameSpeed_pos
plain-language theorem explainer
Flame speed on the φ-ladder is strictly positive for every natural-number rung k. Combustion theorists cite the result to guarantee that ratios and monotonicity statements remain well-defined before invoking field_simp or linarith on adjacent rungs. The proof reduces directly to the positivity of φ^k via unfolding and a single application of pow_pos.
Claim. For every natural number $k$, the flame speed at rung $k$ satisfies $0 < S_L(k)$, where $S_L(k) := S_0 · φ^k$ and the reference speed $S_0 = 1$ in RS-native units.
background
The module treats laminar flame speed as a direct consequence of the φ-ladder: each integer increase in chain-branching rung multiplies speed by exactly φ. The definition flameSpeed k expands to referenceSpeed * phi ^ k with referenceSpeed fixed at 1. This construction inherits the rung function from upstream modules (Masses.AnchorPolicy, Engineering.AsteroidOreSpectroscopy) and the positivity of phi from Constants.
proof idea
The term proof unfolds flameSpeed and referenceSpeed, introduces the auxiliary 0 < phi ^ k via pow_pos Constants.phi_pos k, and closes with linarith.
why it matters
The result supplies the positivity hypothesis required by flameSpeed_adjacent_ratio, flameSpeed_strictly_increasing, and the certificate FlameSpeedCert. It anchors the exact φ-multiplication prediction stated in the module documentation for canonical fuels and aligns with the self-similar fixed point T6 of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.