criticalRecognitionLoading_certificate
plain-language theorem explainer
If a ControllerState satisfies IsCriticalRecognitionLoading for a given rhoMin, then the system is subcritical with attention bounded above by phi cubed, z at least phi to the 45, pulseTicks dividing supervisoryTicks, and load penalty exactly zero. Recognition-bandwidth control theorists would cite this to certify the narrow healthy operating band rhoMin < rho < 1. The proof is a term-mode decomposition that applies five specialized lemmas, one to each conjunct of the goal.
Claim. Let $s$ be a controller state with area, demand, attention, and gap parameter $z$. If $s$ lies in the critical recognition loading band (i.e., its load ratio satisfies the InCriticalBand predicate and its entropy/attention/signature values satisfy the SemanticCondensationGate), then demand is strictly below the bandwidth of the area, attention satisfies $s.attention ≤ φ^3$, $z ≥ φ^{45}$, pulseTicks divides supervisoryTicks, and the load penalty vanishes.
background
The module defines the load ratio rho = demand / bandwidth(area) and asserts that stable operation occurs inside the open interval (rhoMin, 1). ControllerState packages the minimal runtime data (area, demand, attention, z, entropy, signatures) needed by the governor. IsCriticalRecognitionLoading is the conjunction of InCriticalBand rhoMin area demand and SemanticCondensationGate on the entropy/attention/signature fields. The upstream lemma criticalBand_implies_subcritical converts membership in the critical band into the IsSubcritical predicate (demand < bandwidth area). loadPenalty_zero_of_critical shows that any state inside the band incurs zero penalty.
proof idea
The proof is a term-mode refine that splits the five-way conjunction and discharges each conjunct by exact application of a dedicated lemma. criticalBand_implies_subcritical handles the subcriticality claim from the InCriticalBand component of the hypothesis. semanticGate_implies_attention_cap and semanticGate_implies_gap_ready extract the attention upper bound and z lower bound from the SemanticCondensationGate component. pulse_divides_supervisory supplies the divisibility fact, while loadPenalty_zero_of_critical supplies the zero-penalty fact.
why it matters
This certificate is the direct parent of forcedCriticalRecognitionLoading_certificate, which lifts the same conclusion to the forced variant of the loading condition. It supplies the structural control lemma required by the module's sketch of the recognition-bandwidth governor. The 360-tick supervisory horizon (lcm(8,45)) and the phi-powered bounds on attention and z tie directly to the eight-tick octave (T7) and the phi-ladder mass formula of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.