StarLower.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Actual lower requirements of a finite-count star. This connects the rank superadditivity to the output formulas, and proves the marked slack from the logarithmic parameter gap (including zero side mass).

def OAI.UniformKServer.StarLower.childBeta line 19
def OAI.UniformKServer.StarLower.parentBeta line 22
def OAI.UniformKServer.StarLower.lower line 25
def OAI.UniformKServer.StarLower.parentLower line 28
theorem OAI.UniformKServer.StarLower.child_allowed line 31
theorem OAI.UniformKServer.StarLower.parent_allowed line 36
theorem OAI.UniformKServer.StarLower.parameter_le line 40
theorem OAI.UniformKServer.StarLower.decomposition line 54
theorem OAI.UniformKServer.StarLower.inactive line 63
theorem OAI.UniformKServer.StarLower.lower_nonneg line 78
theorem OAI.UniformKServer.StarLower.core_nonneg line 83
theorem OAI.UniformKServer.StarLower.flex_mono line 86
theorem OAI.UniformKServer.StarLower.parent_dominates line 95

theorem OAI.UniformKServer.StarLower.lower_difference line 100

Source documentation

No active-size or positive side-mass hypothesis is used in this identity.

theorem lower_difference (d : Data Ω ι k) (β γ : ℝ) (t : ℕ) (ω : Ω) (i : ι) :
    lower d β t ω i-lower d γ t ω i =
      (γ-β)*(coreInput d t ω i+flexGap (input d i) t ω) := by
…

Mentions: OAI.UniformKServer.StarLower.lower

theorem OAI.UniformKServer.StarLower.dominant_slack line 108
Source documentation
The source's dominant-output-slack inequality. Its constant is explicit and absolute, and the assertion retains u=0 and T=0.
```
theorem dominant_slack (d : Data Ω ι k) (hk : 1 ≤ k) (t : ℕ) (ω : Ω)
    (s : EpochGeometry.State ι) (hs : EpochGeometry.valid (held d t ω) s)
    (o : ι) (ho : EpochGeometry.dominant s=some o) (U : ℝ)
    (hU : EpochParameters.sideReference (held d t ω) o U) :
    (ParentBeta.cBeta/288)*(U/EpochGeometry.total s.base)/EpochAlpha.ell k*
        trueFlex (input d o) (parentBeta d t ω) t ω ≤
      lower d (parentBeta d t ω) t ω o-lower d (childBeta d t ω o) t ω o := by
…
```
Mentions: OAI.UniformKServer.EpochGeometry.State, OAI.UniformKServer.EpochGeometry.valid, OAI.UniformKServer.EpochGeometry.dominant, OAI.UniformKServer.EpochParameters.sideReference, OAI.UniformKServer.ParentBeta.cBeta, OAI.UniformKServer.EpochGeometry.total, OAI.UniformKServer.EpochAlpha.ell, OAI.UniformKServer.StarLower.parentBeta, OAI.UniformKServer.StarLower.lower, OAI.UniformKServer.StarLower.childBeta