temp_adjacent_ratio
plain-language theorem explainer
The theorem states that Maillard temperatures at consecutive phi-ladder rungs stand in the fixed ratio phi. Chemists deriving structural temperature steps from the J-cost framework cite it to confirm the geometric progression. The proof is a one-line wrapper that rewrites via the successor scaling lemma and clears the denominator with the positivity fact.
Claim. For every natural number $k$, $T_{k+1}/T_k = phi$, where the rung temperature is defined by $T_k := T_0 phi^k$ and $T_0$ is the reference onset temperature at rung zero.
background
The MaillardTemperatureLadder module builds an explicit temperature sequence for the Maillard reaction by scaling a reference onset temperature by successive powers of phi. The function tempAtRung(k) returns the temperature at rung k, defined as referenceTemp multiplied by phi to the power k. The upstream result tempAtRung_succ_ratio states that tempAtRung(k+1) equals tempAtRung(k) times phi, while tempAtRung_pos asserts that every rung temperature is positive. This setting follows the module's description of the Maillard reaction temperature ladder, with rung 0 at 140°C and each higher rung multiplying by phi, yielding predicted peaks near 226°C and char boundaries near 366°C.
proof idea
The proof rewrites the left-hand side using the successor ratio lemma tempAtRung_succ_ratio, which replaces the numerator with the product of the denominator and phi. It then invokes field_simp, supplying the non-zero condition from tempAtRung_pos k to cancel the common factor and obtain phi.
why it matters
This result supplies the adjacent ratio property required by the MaillardTemperatureCert definition, which aggregates positivity, one-step scaling, strict increase, and the phi ratio into a single certificate object. It completes the explicit ladder construction that follows from the phi self-similarity forced in the Recognition framework. The certificate is then available for downstream verification of temperature thresholds against empirical Maillard data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.