criticalBand_implies_subcritical
plain-language theorem explainer
Systems whose load ratio lies strictly between rhoMin and 1 remain subcritical. Recognition Science control arguments cite this implication to guarantee that critical-band operation never saturates bandwidth. The proof extracts the upper bound from the InCriticalBand hypothesis, rewrites the load ratio definition, and applies positivity of bandwidth together with the division inequality.
Claim. If $0 < A$ and $r < D / R(A) < 1$, then $D < R(A)$, where $R(A)$ is the recognition bandwidth of area $A$ and $r$ is the forced lower edge of the control band.
background
The module sketches control theorems for recognition systems. The load ratio is defined as demand divided by bandwidth(area). InCriticalBand asserts that this ratio lies between rhoMin and 1. IsSubcritical asserts that demand lies below bandwidth(area). Bandwidth itself is area divided by the product of Planck area, recognition cost ln(phi), and the eight-tick cadence. An upstream result establishes that bandwidth is positive for positive area.
proof idea
The proof performs case analysis on the InCriticalBand hypothesis to isolate the conjunct loadRatio < 1. It unfolds IsSubcritical and loadRatio, obtains positivity of bandwidth via the upstream bandwidth_pos lemma, rewrites the strict inequality using div_lt_one, and concludes by simplification.
why it matters
This result supports the structural lemmas for critical recognition loading. It is used by criticalBand_not_overloaded to establish that the system is not overloaded and by criticalRecognitionLoading_certificate to certify subcriticality together with bounds on attention and z. It contributes to the control theorem for the operating regime suggested by recognition bandwidth, consistent with the eight-tick cadence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.