IsCriticalRecognitionLoading
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not fix the numerical value of rhoMin.
- Does not compute loadRatio from first principles.
- Does not enforce the 8-tick or 360-tick cadence.
- Does not derive entropy from defect counts.
formal statement (Lean)
185def IsCriticalRecognitionLoading (rhoMin : ℝ) (s : ControllerState) : Prop :=
proof body
Definition body.
186 InCriticalBand rhoMin s.area s.demand ∧
187 SemanticCondensationGate
188 s.entropy s.entropyFloor s.attention
189 s.signature s.signatureMin s.signatureMax s.z
190
191/-- The non-parameterized critical-loading condition. -/