pith. machine review for the scientific record. sign in
def definition def or abbrev high

tempAtRung

show as:
view Lean formalization →

Maillard reaction temperature at rung k on the phi-ladder is defined as the reference onset scaled by phi to the power k. Chemists applying Recognition Science to sugar-amine reactions cite this to generate the explicit temperature sequence from 140°C onset onward. The definition is a direct scaling that supplies the geometric progression used by downstream certification theorems.

claimThe Maillard reaction temperature at rung $k$ is $T_k = T_0 · ϕ^k$, where $T_0$ denotes the reference onset temperature (RS-native value 1, calibrated to 140°C).

background

The phi-ladder is the geometric sequence generated by the self-similar fixed point phi forced in the UnifiedForcingChain (T6). Reference temperature is the dimensionless unit 1 in RS-native units, calibrated so that rung 0 matches the empirical Maillard onset at 140°C. The module extends the J-cost band application to explicit rung temperatures for any sugar-amine pair, with predicted values rung 1 ≈ 226°C (peak browning) and rung 2 ≈ 366°C (char boundary). Upstream referenceTemp supplies the calibrated base value.

proof idea

Direct definition: tempAtRung k is referenceTemp multiplied by phi raised to k. It inherits the real-number power operation and the constant referenceTemp without further reduction.

why it matters in Recognition Science

This definition supplies the temperature values required by MaillardTemperatureCert, which certifies positivity, the one-step ratio equal to phi, strict monotonicity, and adjacent ratio phi. It completes the explicit ladder step in the Maillard module, linking the J-cost wrapper to the phi-ladder from the forcing chain (T5–T7). The construction supports structural predictions for browning and charring thresholds without additional hypotheses.

scope and limits

formal statement (Lean)

  37def tempAtRung (k : ℕ) : ℝ := referenceTemp * phi ^ k

proof body

Definition body.

  38

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.