StabilizationCert
plain-language theorem explainer
StabilizationCert packages the three predicates that certify flame stabilization under the J-cost model: the critical Damköhler number exceeds 1, lies inside the interval (1.2, 2.5), and the associated cost vanishes on the diagonal. Combustion theorists would cite the record to confirm that the golden-ratio threshold satisfies both the theoretical minimum-cost condition and the observed stability window. The definition is a direct record constructor with no reduction steps or lemmas applied.
Claim. A stabilization certificate is a structure on the critical Damköhler number $D_c = φ$ asserting $1 < D_c$, $1.2 < D_c < 2.5$, and $J(D/D_c) = 0$ for every nonzero measured Damköhler number $D$.
background
In the Recognition Science combustion module, flame stabilization requires flow residence time to exceed chemical ignition delay, expressed by the Damköhler number Da = τ_flow / τ_chem. The upstream definition criticalDamkohler sets this threshold to phi, while damkohlerCost(da_measured, da_critical) returns Jcost(da_measured / da_critical). The module doc states that RS predicts Da_crit = φ at which J(φ) supplies the recognition quantum, the minimum nonzero cost for a flow state to recognize the chemical threshold. Empirical ignition and extinction boundaries occur for Da in (1.3, 2.0), consistent with φ ≈ 1.618.
proof idea
The declaration is a structure definition that directly records the three field predicates: the strict inequality 1 < criticalDamkohler, the band membership (1.2, 2.5), and the universal zero-cost condition on the diagonal of damkohlerCost. No tactics, reductions, or upstream lemmas are invoked inside the body; the record simply assembles the predicates supplied by the sibling definitions.
why it matters
StabilizationCert supplies the concrete record that is instantiated by the downstream definition cert and shown nonempty by cert_inhabited. It completes the structural slot in the flame-stabilization plan by bundling the phi-based critical Damköhler number with its empirical consistency and the diagonal vanishing of the J-cost. In the larger framework the construction links the T6 self-similar fixed point φ to the combustion domain through the Recognition Composition Law applied to the Damköhler ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.