pith. sign in
module module high

IndisputableMonolith.Chemistry.HaberBoschFromJCost

show as:
view Lean formalization →

The module Chemistry.HaberBoschFromJCost instantiates the reusable J-cost band template for the Haber-Bosch ammonia synthesis. It certifies the process by establishing that J vanishes at the stoichiometric ratio and remains nonnegative for all positive ratios. Researchers assembling the Recognition Science master certification chain cite this module as one of the domain certificates. The structure follows the six-clause template imported from CanonicalJBand with no additional lemmas.

claimFor the stoichiometric ratio $r$ of the reaction $N_2 + 3H_2 = 2NH_3$, the certification requires $J(r)=0$ together with $J(x)≥0$ for all $x>0$, where $J(x)=(x+x^{-1})/2-1$.

background

Recognition Science derives all physics from the single functional equation whose solution yields the J-cost function $J(x)=(x+x^{-1})/2-1$. The upstream CanonicalJBand module supplies the reusable six-clause template applied across every domain certificate in the master chain. That template demands two core properties: matched-zero ($J(1)=0$) and nonnegativity ($J(x)≥0$ for $x>0$). The present chemistry module applies this template to the Haber-Bosch process, introducing sibling definitions for catalysis stages and the resulting certificate.

proof idea

This is a definition module that directly instantiates the CanonicalJBand template. It defines HeterogeneousCatalysisStage, catalysisStageCount, HaberBoschCert and the associated haberBoschCert theorem by substituting the chemical ratio into the six-clause template. The argument consists of one-line applications of the imported matched-zero and nonnegativity clauses with no custom tactics or lemmas.

why it matters in Recognition Science

The module supplies the chemistry instance required by the master certification chain described in CanonicalJBand. It contributes one of the domain certificates needed for B-tier whole-science openings and the Plan v7 collection of roughly forty domain certificates. By closing the chemistry slot it advances the overall Recognition Science framework that derives constants and processes from the J functional equation.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)