SliceFactorial.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual fixed-total signatures give the labelled factorial properties

Every subset count is in its true label-capacity box and its total is the subset's cardinality. These identities connect the proved integer slice signatures to the first factorial lift, without any binary-signature input.

lemma OAI.ContingencyTables.SliceFactorial.groupCount_inBox line 22
theorem OAI.ContingencyTables.SliceFactorial.firstLift_degreePositive line 32
Source documentation
Positivity of the proved actual total-slice marginal gives positivity of the literal labelled factorial lift on exactly that subset degree.
```
theorem firstLift_degreePositive (group : L → C) (h : (C → ℕ) → ℝ) (D : ℝ) (R : ℕ)
    (hD : 0 < D) (hpos : PositiveSlice h (groupCount group Set.univ) R) :
    DegreePositive (firstLift group h D) R := by
…
```

theorem OAI.ContingencyTables.SliceFactorial.firstLift_omission_slice line 43

Source documentation

The exact box-valid raw removal signature implies the omission property of the manuscript's first lift at its original degree.

theorem firstLift_omission_slice (group : L → C) (h : (C → ℕ) → ℝ) (D : ℝ) (R : ℕ)
    (hD : 0 < D) (hh : ∀ z, 0 ≤ h z)
    (hsig : RemovalSlice h (groupCount group Set.univ) R) :
    OmissionProperty (firstLift group h D) R := by
…

theorem OAI.ContingencyTables.SliceFactorial.firstLift_tendsto line 57

Source documentation

Pointwise limits of actual integer marginals pass directly to their literal subset factorial displays.

theorem firstLift_tendsto {K : Type*} {l : Filter K}
    (group : L → C) (F : K → (C → ℕ) → ℝ) (h : (C → ℕ) → ℝ) (D : ℝ)
    (hlim : ∀ z, Filter.Tendsto (fun t => F t z) l (nhds (h z))) (S : Set L) :
    Filter.Tendsto (fun t => firstLift group (F t) D S) l (nhds (firstLift group h D S)) :=
…