semanticGate_implies_gap_ready
plain-language theorem explainer
The semantic condensation gate includes phi to the 45 as a lower bound on the control variable z among its admissibility conditions. Researchers modeling recognition bandwidth and controller stability cite this extraction when confirming gap readiness from gate satisfaction. The proof is a direct one-line term projection from the gate's defining conjunction.
Claim. If the semantic condensation gate holds for real numbers entropy, entropyFloor, attention, signature, signatureMin, signatureMax and z, then $phi^{45} leq z$.
background
The Critical Recognition Loading module sketches control conditions for recognition systems. The load ratio rho equals demanded recognition rate over maximum bandwidth, with healthy operation in the sub-saturation band rho_min < rho < 1. The actuator uses the native 8-tick cadence while the controller judges stability on the 360-tick supervisory horizon from lcm(8,45). The semantic condensation gate defines query-level admissibility as the conjunction entropyFloor < entropy, signatureMin leq signature leq signatureMax, attention leq phi^3, and phi^45 leq z.
proof idea
The proof is a term-mode extraction. The hypothesis h is the five-fold conjunction from the gate definition, and the access h.2.2.2.2 isolates the final conjunct phi^(45 : N) leq z.
why it matters
This lemma is invoked by the criticalRecognitionLoading_certificate theorem, which concludes that a controller state satisfying IsCriticalRecognitionLoading is subcritical, obeys the attention bound, and meets phi^45 leq s.z. It supplies a structural piece for the control theorem in the module, linking to the phi ladder and the 45-tick component of the supervisory horizon. It touches the Recognition Science framework at the eight-tick octave and phi uniqueness steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.