criticalBand_not_overloaded
plain-language theorem explainer
If a recognition system satisfies rho_min < demand over bandwidth(area) < 1 with positive area, then demand stays strictly below the bandwidth ceiling. Recognition control theorists would cite this to enforce the sub-saturation operating regime. The proof is a short tactic sequence that unfolds the overload predicate, invokes the subcritical implication lemma, and negates the resulting inequality.
Claim. If $0 < A$ and $r < D / R(A) < 1$, then $D < R(A)$, where $R(A)$ is the recognition bandwidth of a region with boundary area $A$ and $r$ is the forced lower edge of the control band.
background
The module sketches a control theorem for the operating regime of recognition bandwidth and the semantic condensation gate. The central variable is the load ratio rho = R_dem / R_max, with healthy operation required in the narrow band rho_min < rho < 1. The actuator runs on the native 8-tick cadence while stability is judged on the 360-tick supervisory horizon forced by lcm(8,45).
proof idea
The tactic proof unfolds IsOverloaded to expose bandwidth area <= demand. It then applies criticalBand_implies_subcritical (using the area positivity hypothesis) via simpa on IsSubcritical to obtain the strict inequality demand < bandwidth area. The final step applies not_le_of_gt to reach the negation.
why it matters
This lemma ensures the critical band definition stays below the overload threshold, supporting the structural claim of healthy operation in rho_min < rho < 1 inside the unification module. It fills a gap in the theorem sketch that precedes the semantic free energy and condensation gate section. The result aligns with the eight-tick octave and recognition bandwidth definition but has no recorded downstream uses yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.