flameSpeed_strictly_increasing
plain-language theorem explainer
Flame speed on the phi-ladder increases strictly with each integer rung. Combustion modelers cite it to confirm monotonicity from the structural ratio alone. The tactic proof rewrites via the successor ratio, invokes positivity of the speed at rung k, derives phi greater than one, applies the positive multiplication inequality, and simplifies.
Claim. For every natural number $k$, the laminar flame speed at rung $k$ is strictly less than the laminar flame speed at rung $k+1$, where speed at rung $k$ equals reference speed times $phi^k$.
background
The module defines laminar flame speed on the phi-ladder so that each integer step in chain-branching intensity multiplies speed by exactly phi. Upstream results supply the definition flame speed at rung k equals reference speed times phi to the power k, the theorem that this quantity remains positive for every natural k, and the successor ratio theorem that speed at k+1 equals speed at k times phi. The local setting is the Recognition Science derivation of combustion quantities from the phi-ladder structure with no fitted parameters.
proof idea
The proof rewrites the target inequality using the successor ratio theorem, invokes the positivity theorem for flame speed at k, obtains phi greater than one from the constant lemma via linarith, applies the multiplication inequality for a positive left factor to reach speed at k times 1 less than speed at k times phi, and closes with simpa.
why it matters
This theorem supplies the strict increase component inside the flameSpeedCert bundle that also collects positivity, one-step ratio, and adjacent ratio equality. It supports the exact phi-ladder prediction for laminar flame speeds across fuels, consistent with T6 where phi is forced as the self-similar fixed point and with the Recognition Composition Law. No open questions appear in the supplied results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.