Budget.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.HyperbolicObstruction.SparsePattern.Pattern line 16
Source documentation
Independent table entry types, with their coordinate supports and critical costs. The table model of Sections 2 and 4 is a concrete instance.
```
structure Pattern (F R : Type*) [Fintype F] [Fintype R] where
…
```
def OAI.HyperbolicObstruction.SparsePattern.Pattern.exponent line 25
lemma OAI.HyperbolicObstruction.SparsePattern.Pattern.exponent_submodular line 28
lemma OAI.HyperbolicObstruction.SparsePattern.Pattern.exponent_eq_card line 54

theorem OAI.HyperbolicObstruction.SparsePattern.Pattern.critical_closure line 60

Source documentation

The maximal critical closure in Section 4. The conclusions retain a full unit integer margin, not merely strictness.

theorem critical_closure (P : Pattern F R) (I : Finset F) (e : F)
    (he : e ∉ I) (hI : P.exponent I = I.card)
    (hbudget : ∀ W, I ⊆ W → (I.card : ℤ) ≤ P.exponent W)
    (htest : ∀ W, insert e I ⊆ W → ((insert e I).card : ℤ) ≤ P.exponent W) :
    ∃ U : Finset F, I ⊆ U ∧ P.exponent U = I.card ∧ e ∉ U ∧
      ∀ V : Finset F, V.Nonempty → Disjoint V U →
        1 ≤ P.exponent (U ∪ V) - P.exponent U := by
…

Mentions: OAI.HyperbolicObstruction.SparsePattern.Pattern