IsCriticalRecognitionLoading
plain-language theorem explainer
IsCriticalRecognitionLoading packages the full critical-loading condition as the conjunction of the InCriticalBand predicate on load ratio and the SemanticCondensationGate on entropy, signature, and attention. Control theorists working on recognition bandwidth regimes would cite this definition when stating the healthy sub-saturation operating band for a bounded region. The definition is a direct conjunction of the two component predicates with no further reduction.
Claim. The predicate IsCriticalRecognitionLoading($rho_{min}$, $s$) holds precisely when $rho_{min} < loadRatio(s.area, s.demand) < 1$ and the semantic condensation gate is satisfied: $s.entropyFloor < s.entropy$, $s.signatureMin ≤ s.signature ≤ s.signatureMax$, $s.attention ≤ phi^3$, and $phi^{45} ≤ s.z$, where $s$ is a ControllerState carrying area, demand, entropy, entropyFloor, attention, signature, signatureMin, signatureMax, and $z$.
background
The Critical Recognition Loading module sketches a control theorem for the operating regime of recognition bandwidth. The central variable is the load ratio $rho = R_{dem}/R_{max}$, with healthy operation required to lie in the narrow band $rho_{min} < rho < 1$. The ControllerState structure supplies the minimal runtime fields needed by the governor: area, demand, entropy, entropyFloor, attention, signature, signatureMin, signatureMax, and $z$ (MODULE_DOC). Upstream entropy is defined as proportional to total defect in InitialCondition and as $S = k beta ⟨E⟩ + k ln Z$ in the Boltzmann and partition-function settings. InCriticalBand enforces the strict inequality on load ratio while SemanticCondensationGate checks the entropy floor, signature bounds, attention ≤ $phi^3$, and $z ≥ phi^{45}$.
proof idea
The definition is a one-line conjunction that applies InCriticalBand to rhoMin, area, and demand and then conjoins the result with SemanticCondensationGate applied to the entropy, entropyFloor, attention, signature, signatureMin, signatureMax, and z fields of the ControllerState.
why it matters
This definition supplies the full critical-loading condition used by the criticalRecognitionLoading_certificate theorem (which derives subcriticality, attention ≤ $phi^3$, and $z ≥ phi^{45}$) and by the non-parameterized IsForcedCriticalRecognitionLoading. It fills the control variable for the sub-saturation band in the Recognition Science framework, consistent with the eight-tick octave and the phase-transition geometry that forces the lower edge rhoCriticalMin. It touches the open question of embedding the governor in a full physics deployment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.