maillardTemperatureCert
plain-language theorem explainer
The Maillard-temperature-ladder certificate packages the positivity, multiplicative step, strict monotonicity, and exact phi-ratio properties of the rung temperatures into one structure. Researchers modeling the Maillard reaction in sugar-amine systems would reference it to obtain the predicted temperature sequence starting at 140°C. The definition is a direct record construction that wires in the four supporting lemmas already established for the tempAtRung function.
Claim. Let $T(k)$ denote the temperature at rung $k$ on the phi-ladder with base $T(0)=140^circ$C. The certificate asserts $T(k)>0$, $T(k+1)=phi cdot T(k)$, $T(k)<T(k+1)$, and $T(k+1)/T(k)=phi$ for every natural number $k$.
background
The module develops the Maillard reaction temperature on the phi-ladder. The reference temperature is set at 140°C for rung 0, with subsequent rungs obtained by multiplication by the golden ratio phi. The structure MaillardTemperatureCert collects four properties required for the ladder to serve as a structural prediction for any sugar-amine pair.
proof idea
The definition is a record constructor that directly supplies the four fields of MaillardTemperatureCert. It assigns temp_pos to the theorem tempAtRung_pos, one_step_ratio to tempAtRung_succ_ratio, strictly_increasing to tempAtRung_strictly_increasing, and adjacent_ratio_eq_phi to temp_adjacent_ratio. No additional tactics are required beyond the existing proofs of those lemmas.
why it matters
This definition supplies the complete certificate for the Maillard temperature ladder, enabling its use in the broader Maillard wrapper that applies the J-cost band to surface-temperature ratios. It realizes the explicit rung predictions (140°C, 140·phi, 140·phi²) described in the module documentation. Within the Recognition framework it instantiates the phi-ladder structure for chemical thresholds, consistent with the self-similar fixed point forced at T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.