`InForcedCriticalBand`

definition

show as: view math explainer →

module: IndisputableMonolith.Unification.CriticalRecognitionLoading
domain: Unification
line: 90 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Unification.CriticalRecognitionLoading on GitHub at line 90.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  87  RecognitionBandGeometry.rhoBandLower_eq
  88
  89/-- The fixed control band used by the runtime. -/
  90def InForcedCriticalBand (area demand : ℝ) : Prop :=
  91  InCriticalBand rhoCriticalMin area demand
  92
  93theorem loadRatio_pos {area demand : ℝ} (hArea : 0 < area) (hDemand : 0 < demand) :
  94    0 < loadRatio area demand := by
  95  unfold loadRatio
  96  exact div_pos hDemand (bandwidth_pos hArea)
  97
  98theorem criticalBand_implies_subcritical
  99    {rhoMin area demand : ℝ} (hArea : 0 < area)
 100    (h : InCriticalBand rhoMin area demand) :
 101    IsSubcritical area demand := by
 102  rcases h with ⟨_, hlt⟩
 103  unfold IsSubcritical
 104  unfold loadRatio at hlt
 105  have hB : 0 < bandwidth area := bandwidth_pos hArea
 106  rw [div_lt_one hB] at hlt
 107  simpa using hlt
 108
 109theorem criticalBand_not_overloaded
 110    {rhoMin area demand : ℝ} (hArea : 0 < area)
 111    (h : InCriticalBand rhoMin area demand) :
 112    ¬ IsOverloaded area demand := by
 113  unfold IsOverloaded
 114  have hSub : demand < bandwidth area := by
 115    simpa [IsSubcritical] using criticalBand_implies_subcritical hArea h
 116  exact not_le_of_gt hSub
 117
 118/-! ## §3. Semantic free energy and condensation gate -/
 119
 120/-- Query-level semantic free energy. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.