cert_inhabited
plain-language theorem explainer
The declaration establishes existence of a StabilizationCert by direct construction from a prior term. Combustion theorists would cite it to confirm that the critical Damköhler number lies in the empirical interval with zero associated cost at criticality. The proof is a one-line term that instantiates the structure using the already-defined cert.
Claim. There exists a certificate asserting that the critical Damköhler number $d$ satisfies $1 < d$ and $1.2 < d < 2.5$, together with the property that the Damköhler cost satisfies $d ≠ 0 → damkohlerCost(d,d) = 0$ for all real $d$.
background
The module treats flame stabilization through the Damköhler number Da = τ_flow / τ_chem. StabilizationCert packages three properties: the critical value exceeds 1, lies inside the band (1.2, 2.5), and the cost function damkohlerCost vanishes on the diagonal for nonzero arguments. The module documentation states that Recognition Science predicts Da_crit = φ with J(φ) the recognition quantum, and that empirical ignition boundaries fall in (1.3, 2.0), consistent with φ ≈ 1.618. The sole upstream dependency is the definition of StabilizationCert itself.
proof idea
The proof is a term-mode construction. It applies the structure constructor to the term cert, which already satisfies the three fields da_gt_one, da_in_band, and cost_at_critical.
why it matters
The theorem shows the StabilizationCert structure is inhabited, completing the structural development of the combustion timescale result. It supports the module claim that the critical Damköhler number lies in (1.2, 2.5) and aligns with the forcing-chain prediction Da_crit = φ. No downstream theorems are recorded, so the result functions as a terminal structural fact. It touches the open empirical question of whether flame experiments remain inside the falsifier band (1.2, 2.5).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.