rhoCriticalMin
plain-language theorem explainer
The lower edge of the forced critical recognition band equals one over phi squared. Recognition control models cite this constant to bound the load ratio below which the system enters the subcritical regime. The declaration is a one-line abbreviation of the band-geometry lower bound.
Claim. The forced lower edge of the control band is defined by $ρ_{crit,min} = φ^{-2}$.
background
The module introduces the load ratio ρ = R_dem / R_max as the central control variable for recognition bandwidth. Healthy operation requires ρ_min < ρ < 1, with the actuator running on the native 8-tick cadence and stability judged on the 360-tick supervisory horizon from lcm(8,45). Upstream result rhoBandLower supplies the lower cognitive band boundary ρ_min = 1/φ² from the phase-transition geometry.
proof idea
One-line abbreviation that directly imports the lower band boundary from RecognitionBandGeometry.
why it matters
This definition supplies the fixed lower threshold used by InForcedCriticalBand and IsForcedCriticalRecognitionLoading. It anchors the control band in the phase-transition geometry, feeding the certificate theorem that enforces subcritical operation with attention bounded by phi cubed and z at least phi to the 45. It closes the structural lemma for the eight-tick cadence controller.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.