IntegerRecursivePotential.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Telescoping the actual raw integer recursion

The literal future kernel commutation and nonnegative square identity control every future correction after a split. No signature property of the weighted correction kernel is used.

lemma OAI.ContingencyTables.IntegerWeightedTransport.correction_future_lower line 21
lemma OAI.ContingencyTables.IntegerWeightedTransport.integerRemovalMatrix_add line 41
lemma OAI.ContingencyTables.IntegerWeightedTransport.correction_form_cons line 48
theorem OAI.ContingencyTables.IntegerWeightedTransport.recursivePotential_bound line 59
Source documentation
The entire leaf potential is bounded by the root potential minus the sum of the actual root future forms. All recursive hypotheses are derived from the original valid total slice.
```
theorem recursivePotential_bound : ∀ (Ms : List ℕ) {I : Type u} [Fintype I] [DecidableEq I]
    (F : (Coordinates I Ms → ℕ) → ℝ) (m z : I → ℕ) (R : ℕ) (h : I → ℝ),
    (∀ U ∈ Ms, 2 ≤ U) → (∀ x, 0 ≤ F x) →
    BalancedBox.PositiveSlice F (bounds m Ms) (R+Ms.sum) →
    BalancedBox.RemovalSlice F (bounds m Ms) (R+Ms.sum) →
    BalancedBox.InBox m z → (∑ i, z i)=R+1 →
    holeLinear (eliminate Ms F) z h=0 →
    recursivePotential Ms F z h ≤ holePotential (eliminate Ms F) z h -
      (integerRemovalMatrix (correctionKernel Ms F) z).toBilin' h h := by
…
```
Mentions: OAI.ContingencyTables.BalancedBox.PositiveSlice, OAI.ContingencyTables.BalancedBox.RemovalSlice, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.IntegerWeightedTransport.holeLinear, OAI.ContingencyTables.IntegerWeightedTransport.recursivePotential, OAI.ContingencyTables.IntegerWeightedTransport.holePotential, OAI.ContingencyTables.IntegerWeightedTransport.correctionKernel