ForestBoxCardinality.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The expanded physical forest box still has a short cardinality bound

The tree interval width 20db has at most (b+1)^2 integer positions when every large capacity is at least 20d. This provides a uniform bound for the positive equality-softened balanced sums before taking limits.

lemma OAI.ContingencyTables.ForestBoxCardinality.width_add_one_le_square line 19
abbrev OAI.ContingencyTables.ForestBoxCardinality.Assignments line 28
theorem OAI.ContingencyTables.ForestBoxCardinality.cardinality_le_square line 31
theorem OAI.ContingencyTables.ForestBoxCardinality.cardinality_le_two_pow line 43
Source documentation
The full balanced physical box, including every expanded tree interval, has at most 2^K profiles under the source's bit-size allowance.
```
theorem cardinality_le_two_pow (A : Instance I J) (hW : 20*A.d ≤ A.W)
    (L K : ℕ) (hL : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^L) (hK : 2*L ≤ K) :
    Fintype.card (Assignments A) ≤ 2^K := by
…
```
Mentions: OAI.ContingencyTables.ForestBoxCardinality.Assignments