pith. sign in
theorem

flameSpeed_adjacent_ratio

proved
show as:
module
IndisputableMonolith.Combustion.FlameSpeedFromPhiLadder
domain
Combustion
line
61 · github
papers citing
none yet

plain-language theorem explainer

The ratio of laminar flame speeds at consecutive rungs of the phi-ladder equals the golden ratio phi exactly. Combustion theorists would cite this when deriving parameter-free scaling laws for premixed flames across fuels. The proof is a one-line wrapper that rewrites via the successor relation and cancels the positive denominator by field simplification.

Claim. For every natural number $k$, the ratio of flame speed at rung $k+1$ to flame speed at rung $k$ equals $phi$, where flame speed at rung $k$ is defined as reference speed times $phi^k$.

background

Flame speed at rung $k$ is defined as referenceSpeed multiplied by $phi$ raised to the power $k$. The positivity theorem establishes that this quantity is strictly positive for every natural number $k$, using the positivity of $phi$ and the reference speed. The successor-ratio theorem states that flame speed at $k+1$ equals flame speed at $k$ multiplied by $phi$, obtained by unfolding the definition and applying the power-succ rule followed by ring simplification.

proof idea

The proof rewrites the target ratio by the successor-ratio lemma, introduces the positivity fact for the denominator, and applies field_simp to cancel the common positive factor.

why it matters

This supplies the adjacent-ratio component required by the flameSpeedCert structure, which bundles positivity, successor scaling, strict increase, and the exact phi ratio. It realizes the module-level claim that adjacent-rung flame speeds stand in the ratio phi with no fitted parameters. In the broader Recognition Science setting the phi-ladder originates from the self-similar fixed point T6 and the eight-tick octave T7, here specialized to combustion.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.