pith. sign in
module module high

IndisputableMonolith.Physics.CombustionFromJCost

show as:
view Lean formalization →

The CombustionFromJCost module establishes stoichiometric combustion as the recognition equilibrium where J-cost vanishes. Researchers deriving chemical equilibria from the Recognition Science functional equation would cite it for equilibrium conditions. The module supplies definitions for regimes, stoichiometric equilibrium, off-stoichiometric cost, and certificates, drawing on the J-function from the Cost import and the time quantum from Constants; it contains no proofs.

claimStoichiometric combustion is the recognition equilibrium at which $J=0$. Off-stoichiometric cost is measured by the J-function applied to the reactant ratio, with CombustionCert certifying that a given regime achieves the minimum J-cost.

background

The module sits inside the Recognition Science derivation of physics from a single functional equation. Constants supplies the RS-native time quantum with doc-comment stating that the fundamental RS time quantum is the tick with value 1. Cost supplies the J-cost function whose zero set defines recognition equilibrium. Sibling definitions introduce CombustionRegime to classify reaction conditions, stoichiometric_equilibrium for the J=0 case, and combustionCert to witness the equilibrium.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies concrete physical content for the J-uniqueness step (T5) by identifying stoichiometric combustion with J=0. It feeds downstream physics derivations that interpret equilibria in RS-native units, consistent with the forcing chain from T0 to T8. No used-by edges are recorded yet, but the definitions close the gap between the abstract J-functional equation and observable chemical balance.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)