maillardThresholdCert
plain-language theorem explainer
The maillardThresholdCert definition packages three J-cost properties into a single certificate for the Maillard reaction threshold. Food chemists modeling browning and flavor formation in the Recognition Science framework would cite it to connect water-activity ratios to the 140°C activation. It is assembled as a direct record constructor from the equilibrium, positivity, and symmetry lemmas.
Claim. The Maillard threshold certificate asserts that the recognition cost satisfies $J(1)=0$, that $J(r)>0$ whenever $r>0$ and $r≠1$, and that $J(r)=J(r^{-1})$ for every $r>0$.
background
In the Recognition Science treatment of chemistry the Maillard reaction threshold is the point at which the J-cost of the surface water-activity ratio crosses a critical band. The J-cost function is the standard recognition cost $J(x)=(x+x^{-1})/2-1$, which vanishes at unit activity (normal hydration) and becomes positive under dehydration. The module documentation states that below threshold the system remains at recognition equilibrium while above it dehydration drives $J(r_{H_2O})>J(φ)$ and triggers the cascade.
proof idea
The definition is a one-line record constructor that directly supplies the three fields of MaillardThresholdCert from the lemmas below_threshold_equilibrium, above_threshold_positive, and maillard_symmetric.
why it matters
This definition supplies the certified interface for the Maillard reaction threshold (F7) in the chemistry extension of Recognition Science. It packages the J-cost crossing into a single structure that can be referenced when linking the phi-ladder and eight-tick octave to temperature-dependent rates. No downstream theorem yet consumes the certificate, leaving open the question of its integration into explicit reaction-rate derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.