IntegerTransportLevels.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Summing the actual integer-branch recursion by exposure level

The branches are the U+1 balanced profiles of each ordinary slot. Local potential increments and future-form monotonicity telescope to the root bound used before the softened limit. No positivity of future forms or signature property of their weighted sums is assumed.

abbrev OAI.ContingencyTables.IntegerWeightedTransport.BranchPath line 17
def OAI.ContingencyTables.IntegerWeightedTransport.levelSum line 19
lemma OAI.ContingencyTables.IntegerWeightedTransport.levelSum_succ line 21
theorem OAI.ContingencyTables.IntegerWeightedTransport.level_future_lower line 31
Source documentation
A future slot's total quadratic form increases up to the level at which that slot is processed.
```
theorem level_future_lower (U : ℕ)
    (Q : ∀ k, BranchPath U k → ℕ → ℝ)
    (hfuture : ∀ k t, k < t → ∀ s : BranchPath U k,
      Q k s t ≤ ∑ j : Fin (U+1),
        Q (k+1) (Fin.snoc (α := fun _ : Fin (k+1) => Fin (U+1)) s j) t)
…
```
Mentions: OAI.ContingencyTables.IntegerWeightedTransport.BranchPath
theorem OAI.ContingencyTables.IntegerWeightedTransport.integer_leaf_potential_bound line 50
Source documentation
The sum of all leaf potentials is at most the root potential minus the root's future corrections. This is the manuscript's recursion-level telescoping step for U+1 ordinary integer branches.
```
theorem integer_leaf_potential_bound (U : ℕ)
    (P : ∀ k, BranchPath U k → ℝ) (Q : ∀ k, BranchPath U k → ℕ → ℝ)
    (hsplit : ∀ k, ∀ s : BranchPath U k,
      (∑ j : Fin (U+1), P (k+1)
        (Fin.snoc (α := fun _ : Fin (k+1) => Fin (U+1)) s j)) ≤ P k s - Q k s k)
…
```
Mentions: OAI.ContingencyTables.IntegerWeightedTransport.BranchPath