above_threshold_positive
plain-language theorem explainer
The theorem shows that any positive real ratio r not equal to 1 carries strictly positive J-cost. Food chemists working on the Maillard browning threshold would cite it to confirm that dehydration above the water-activity equilibrium activates the recognition cascade. The proof is a direct one-line application of the general J-cost positivity lemma.
Claim. For every real number $r$ with $0 < r$ and $r ≠ 1$, the recognition cost satisfies $0 < J(r)$.
background
The module treats the Maillard reaction as a J-cost crossing of the surface-water-activity ratio. Below threshold the ratio maintains equilibrium with J-cost near zero; above threshold dehydration drives J-cost positive and triggers the cascade. J-cost is the function that vanishes only at r = 1 and is defined via the Recognition Composition Law in the Cost module.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one (from IndisputableMonolith.Cost) to the supplied hypotheses 0 < r and r ≠ 1.
why it matters
It supplies the cascade_above field inside the maillardThresholdCert definition that bundles the three Maillard properties. The result fills the F7 claim that activation occurs when J(r_H₂O) enters the band (0.11, 0.13). It links the positivity property of J-cost to the phi-ladder and eight-tick octave that govern rate acceleration in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.