loadRatio_pos
plain-language theorem explainer
The load ratio, defined as demanded recognition rate over recognition bandwidth of a positive area, is strictly positive when both area and demand are positive. Control theorists modeling recognition systems would cite this to keep the central variable rho in the positive reals before imposing the sub-saturation band. The proof is a term-mode one-liner that unfolds the definition and applies the positivity of bandwidth together with the rule for quotients of positives.
Claim. Let $A > 0$ be the area of a bounded recognition region and let $R > 0$ be the demanded recognition rate. Then the load ratio $R / B(A) > 0$, where $B(A)$ denotes the recognition bandwidth of the region.
background
The Critical Recognition Loading module sketches a control theorem for the operating regime suggested by recognition bandwidth and the semantic condensation gate. Its central variable is the load ratio rho = R_dem / R_max, with the claim that healthy operation lives in the narrow sub-saturation 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 proof is a term-mode one-liner. It unfolds the definition of loadRatio to expose the quotient demand / bandwidth area, then applies the upstream theorem bandwidth_pos to obtain positivity of the denominator and invokes div_pos on the positive numerator and denominator.
why it matters
This result secures positivity of the load ratio, a prerequisite for the regime classifications IsUnderloaded, IsSubcritical, IsOverloaded and InCriticalBand that appear as siblings in the same module. It fills a structural gap in the control sketch whose fuller runtime or physics deployment theorem remains to be written. The surrounding framework ties the 8-tick cadence and the semantic condensation gate to the Recognition Composition Law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.