LeafMargin.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.StarModel.coord_eq_inr line 18
lemma OAI.HyperbolicObstruction.StarModel.rowSupport_nonempty line 27
lemma OAI.HyperbolicObstruction.StarModel.selected_active line 32
def OAI.HyperbolicObstruction.StarModel.leafPins line 60
Source documentation
The entire e-field, in all branches, is pinned in the leaf count.
```
def leafPins (U : Finset F) (e : F) : Finset (Var (B := B) U) :=
…
```
Mentions: OAI.HyperbolicObstruction.StarModel.Var
lemma OAI.HyperbolicObstruction.StarModel.mem_leafPins line 64
lemma OAI.HyperbolicObstruction.StarModel.card_inter_leaf line 68
lemma OAI.HyperbolicObstruction.StarModel.free_card_leaf line 100

theorem OAI.HyperbolicObstruction.StarModel.leaf_critical_gap line 115

Source documentation

Exact critical excess for the shared unconditioned entries in a leaf count. Every nonempty selected set is a genuine union of row supports.

theorem leaf_critical_gap (P : SparsePattern.Pattern F R) (U : Finset F) (e : F) (he : e ∉ U)
    (budget : ∀ W : Finset F, (min 2 W.card : ℕ) ≤ P.exponent W)
    (supports : ∀ r, 3 ≤ (P.support r).card)
    (gap : ∀ W, W.Nonempty → Disjoint U W → 1 ≤ P.exponent (U ∪ W) - P.exponent U)
    (J : Finset (Pos (B := B) P.support U)) (hJ : J.Nonempty) :
…

Mentions: OAI.HyperbolicObstruction.SparsePattern.Pattern, OAI.HyperbolicObstruction.StarModel.Pos