IntegerReflection.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Actual box reflection and integer addition signatures

Reflection of every coordinate converts a valid two-addition entry into a two-removal entry. A balanced summed pair is reflected by reversing its finite index, so the same marginal closure applies to additions.

def OAI.ContingencyTables.IntegerReflection.reflect line 20
lemma OAI.ContingencyTables.IntegerReflection.reflect_removeTwo line 23
theorem OAI.ContingencyTables.IntegerReflection.addition_eq_reflected_removal line 53
Source documentation
Exact matrix identity, including all invalid pair entries.
```
theorem addition_eq_reflected_removal (h : (I → ℕ) → ℝ) (N r n : I → ℕ)
    (hr : ∀ i, r i+n i=N i) :
    integerAdditionMatrix h r n = integerRemovalMatrix (fun z => h (reflect N z)) n := by
…
```
Mentions: OAI.ContingencyTables.IntegerReflection.reflect
theorem OAI.ContingencyTables.IntegerReflection.addition_onePositive_of_reflection line 65
Source documentation
The addition signature follows from the raw removal signature of its globally reflected weight, without a binary-lift assumption.
```
theorem addition_onePositive_of_reflection (h : (I → ℕ) → ℝ) (N r n : I → ℕ)
    (hr : ∀ i, r i+n i=N i)
    (hsig : OnePositiveDirection (integerRemovalMatrix (fun z => h (reflect N z)) n).toBilin') :
    OnePositiveDirection (integerAdditionMatrix h r n).toBilin' := by
…
```
Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.IntegerReflection.reflect
lemma OAI.ContingencyTables.IntegerReflection.reflect_profile line 73
theorem OAI.ContingencyTables.IntegerReflection.marginal_reflect line 82
Source documentation
Reflection commutes with actual balanced marginalization by reversal of the finite summation index.
```
theorem marginal_reflect (F : ((I ⊕ Bool) → ℕ) → ℝ) (N z : I → ℕ) (M : ℕ) :
    marginal (fun x => F (reflect (profile N M M) x)) M z =
      marginal F M (reflect N z) := by
…
```
Mentions: OAI.ContingencyTables.IntegerReflection.reflect