tempAtRung_strictly_increasing
plain-language theorem explainer
Maillard temperatures increase strictly along the phi-ladder. Reaction-kinetics researchers cite the result to order rungs from onset through charring. The proof rewrites the successor step, invokes positivity and the bound phi greater than 1.5, then applies a multiplication inequality.
Claim. For every natural number $k$, $T(k) < T(k+1)$ where $T(k) := T_0 phi^k$ and $T_0$ denotes the reference Maillard onset temperature.
background
The module supplies an explicit temperature ladder for the Maillard reaction on the phi-ladder. The definition tempAtRung sets the temperature at rung $k$ to referenceTemp times phi to the power $k$, with referenceTemp fixed at the 140°C onset. Upstream lemmas establish positivity of every such temperature and the exact successor relation tempAtRung(k+1) equals tempAtRung(k) times phi. The constant phi satisfies the tighter bound phi greater than 1.5.
proof idea
The tactic proof rewrites the target inequality via tempAtRung_succ_ratio. It obtains positivity of tempAtRung k from tempAtRung_pos. It derives 1 less than phi from phi_gt_onePointFive by linarith. It applies mul_lt_mul_of_pos_left to the inequality 1 less than phi and the positive temperature, then closes with simpa.
why it matters
The theorem supplies the strictly_increasing field inside the maillardTemperatureCert definition. That certificate bundles the ladder properties to certify the predicted Maillard temperatures. It anchors the chemistry module to the phi-ladder of Recognition Science, where phi is the self-similar fixed point forced at step T6 of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.