MaillardThresholdCert
plain-language theorem explainer
MaillardThresholdCert bundles three properties of the J-cost function to certify the sharp threshold for the Maillard reaction in Recognition Science. A chemist or RS modeler would cite it when anchoring chemical activation to the crossing of unit water-activity ratio. The declaration is a pure structure definition whose fields are supplied directly by three sibling lemmas in the same module.
Claim. A structure certifying that the J-cost function $J$ satisfies $J(1)=0$, $J(r)>0$ for every $r>0$ with $r≠1$, and $J(r)=J(r^{-1})$ for every $r>0$.
background
The J-cost function is imported from the Cost module and defined by $J(r)=(r+r^{-1})/2-1$, the unique solution to the Recognition Composition Law that vanishes at unity. In the MaillardThresholdFromJCost module this function models the recognition cost of the surface water-activity ratio $r_{H_2O}$. The module documentation states: “Below threshold: J(r_H₂O)≈0 (water activity maintains recognition equilibrium). Above threshold: dehydration drives J(r_H₂O)>J(φ), triggering Maillard cascade.” The three fields of the structure encode exactly these equilibrium, positivity, and inversion-symmetry requirements.
proof idea
The declaration is a structure definition containing no proof body. Its three fields are simply declared as the required properties of J-cost; they receive concrete values from the sibling lemmas below_threshold_equilibrium, above_threshold_positive, and maillard_symmetric when the concrete certificate maillardThresholdCert is constructed.
why it matters
The structure supplies the interface that lets the Maillard reaction be treated as a J-cost threshold crossing inside the Recognition Science framework. It is instantiated by maillardThresholdCert and thereby feeds any downstream argument that chemical activation energies arise from the same J-uniqueness (T5) and phi-ladder scaling used for the eight-tick octave and spatial dimension D=3. No open scaffolding questions are closed by this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.