loadPenalty_zero_of_critical
plain-language theorem explainer
When the load ratio lies strictly between its lower threshold rhoMin and saturation, the associated penalty vanishes identically. Control theorists for recognition-bandwidth systems cite this to certify zero-cost operation inside the stable band. The proof unfolds the penalty, applies linear arithmetic to the two band inequalities, rewrites both max expressions to zero, and finishes with ring.
Claim. If $rhoMin < demand / bandwidth(area) < 1$, then $max(0, rhoMin - demand / bandwidth(area)) + max(0, demand / bandwidth(area) - 1) = 0$.
background
The module develops control lemmas for the load ratio rho = demand / bandwidth(area) in bounded recognition systems. The critical band is the open interval (rhoMin, 1), described as close to saturation but still below it. The penalty is the sum of the positive parts of (rhoMin - rho) and (rho - 1), quantifying deviation from this band. The local setting is a theorem sketch supporting healthy operation on the native 8-tick cadence with supervisory horizon lcm(8,45). Upstream results supply the InCriticalBand definition as the conjunction of the two strict inequalities, the loadPenalty definition as the indicated sum of max terms, and the loadRatio definition as demand over bandwidth.
proof idea
The proof unfolds loadPenalty to expose the two max terms. It applies linarith to each conjunct of the InCriticalBand hypothesis to obtain rhoMin - loadRatio <= 0 and loadRatio - 1 <= 0. Two rewrites with max_eq_left reduce the expression to zero, after which ring completes the algebraic simplification.
why it matters
This lemma supplies the zero-penalty case inside the critical band and is invoked by the criticalRecognitionLoading_certificate theorem, which further asserts IsSubcritical s.area s.demand, attention bounded by phi^3, and z at least phi^45. It closes a structural step in the control theorem for recognition bandwidth, consistent with the eight-tick octave and the narrow stable regime near saturation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.