tempAtRung_pos
plain-language theorem explainer
The declaration establishes that the Maillard temperature at rung k on the phi-ladder is strictly positive for every natural number k. Food chemists modeling sugar-amine browning thresholds would cite it to keep the predicted scale physical. The proof is a short term-mode script that unfolds the definition and applies power positivity of phi.
Claim. For every natural number $k$, the Maillard temperature at rung $k$ satisfies $0 < T(k)$, where $T(k) = 1 · φ^k$ and the reference temperature is normalized to unity.
background
The MaillardTemperatureLadder module builds an explicit temperature scale on the phi-ladder. referenceTemp is the dimensionless constant 1, calibrated to the Maillard onset at 140°C. tempAtRung(k) is defined as referenceTemp multiplied by phi raised to the power k. The upstream Constants structure from LawOfExistence supplies the axiom 0 < phi.
proof idea
The proof unfolds tempAtRung and referenceTemp to reduce the goal to 0 < phi^k. It applies the lemma pow_pos using Constants.phi_pos to obtain strict positivity of the power. linarith then closes the inequality.
why it matters
This positivity result is required by the MaillardTemperatureCert definition, which bundles it with the adjacent ratio equaling phi and the strict increase property. It anchors the predicted ladder (rung 0 at 140°C, rung 1 at 140 φ °C, rung 2 at 140 φ² °C) to the phi-ladder and eight-tick octave of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.