AllBalancedWidths.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual balanced finite family allows every small-cell capacity

The proved zero/one boundary cases complete the finite balanced elimination theorem. The physical equality-softened tree marginal can therefore eliminate the original small cells directly.

theorem OAI.ContingencyTables.BalancedBox.marginal_removal_slice_all line 20
theorem OAI.ContingencyTables.BalancedFamily.eliminate_slices_all line 42
Source documentation
Every original small-cell width, including zero and one, may be eliminated on its precise box-valid total slice.
```
theorem eliminate_slices_all (Ms : List ℕ) (m : I → ℕ) (R : ℕ)
    (F : (Coordinates I Ms → ℕ) → ℝ)
    (hpos : PositiveSlice F (bounds m Ms) (R+Ms.sum))
    (hsig : RemovalSlice F (bounds m Ms) (R+Ms.sum)) :
    PositiveSlice (eliminate Ms F) m R ∧ RemovalSlice (eliminate Ms F) m R := by
…
```
Mentions: OAI.ContingencyTables.BalancedFamily.Coordinates, OAI.ContingencyTables.BalancedFamily.bounds, OAI.ContingencyTables.BalancedFamily.eliminate
lemma OAI.ContingencyTables.EqualityReindex.softenedWeight_reindex line 66

theorem OAI.ContingencyTables.EqualityReindex.physical_softened_slices_all line 78

Source documentation

The literal physical positive factor family can retain one tree pair while summing all other original pairs, at every capacity.

theorem physical_softened_slices_all (Ms : List ℕ) (m : S → ℕ) (R : ℕ)
    (e : Coordinates S Ms ≃ D) (line : D → G) (root : G → Bool)
    (rate offset slope : G → ℝ) (urate ell uslope cap : D → ℝ) (L : ℝ)
    (hrate : ∀ g,0 ≤ rate g) (hu : ∀ d,0 ≤ urate d) (hL : 0 ≤ L) :
    PositiveSlice (eliminate Ms (fun z =>
      softenedWeight line root rate offset slope urate ell uslope cap L (z ∘ e.symm))) m R ∧
    RemovalSlice (eliminate Ms (fun z =>
      softenedWeight line root rate offset slope urate ell uslope cap L (z ∘ e.symm))) m R := by
…