CompanionFactorialApplication.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

The companion's literal completion count gives both labelled factorial signatures

The labels below are actual copies of the retained small cells. Their fiber cardinalities are the capacities, so the original first and dual factorial displays and the W² chain-state comparison have no abstract signature or completion hypothesis.

structure OAI.ContingencyTables.CompanionFactorialApplication.Instance line 29
Source documentation
Actual tightened bounded margins, a maximum large-cell forest, and one feasible baseline table determine the completion counts and factorial signatures.
```
structure Instance where
…
```
def OAI.ContingencyTables.CompanionFactorialApplication.SmallCell line 53
def OAI.ContingencyTables.CompanionFactorialApplication.View line 55
def OAI.ContingencyTables.CompanionFactorialApplication.bounds line 57
def OAI.ContingencyTables.CompanionFactorialApplication.h line 59
lemma OAI.ContingencyTables.CompanionFactorialApplication.h_positive line 62
lemma OAI.ContingencyTables.CompanionFactorialApplication.large_width line 65
lemma OAI.ContingencyTables.CompanionFactorialApplication.count_identity line 77
theorem OAI.ContingencyTables.CompanionFactorialApplication.h_removal line 87
Source documentation
The original free-assignment count has its actual raw removal slice.
```
theorem h_removal (A : Instance I J) (alpha : ℝ) (ha : 0≤alpha) (R : ℕ) :
    RemovalSlice (h A alpha) (bounds A) R := by
…
```
Mentions: OAI.ContingencyTables.CompanionFactorialApplication.Instance, OAI.ContingencyTables.CompanionFactorialApplication.h, OAI.ContingencyTables.CompanionFactorialApplication.bounds
theorem OAI.ContingencyTables.CompanionFactorialApplication.h_reflected line 98
Source documentation
The globally reflected count supplies the dual addition input.
```
theorem h_reflected (A : Instance I J) (alpha : ℝ) (ha : 0≤alpha) (R : ℕ) :
    RemovalSlice (fun z => h A alpha (IntegerReflection.reflect (bounds A) z)) (bounds A) R := by
…
```
Mentions: OAI.ContingencyTables.CompanionFactorialApplication.Instance, OAI.ContingencyTables.CompanionFactorialApplication.h, OAI.ContingencyTables.IntegerReflection.reflect, OAI.ContingencyTables.CompanionFactorialApplication.bounds
def OAI.ContingencyTables.CompanionFactorialApplication.Labels line 112
def OAI.ContingencyTables.CompanionFactorialApplication.labelCell line 114
lemma OAI.ContingencyTables.CompanionFactorialApplication.label_width line 116
lemma OAI.ContingencyTables.CompanionFactorialApplication.label_capacity line 138
def OAI.ContingencyTables.CompanionFactorialApplication.denominator line 153
lemma OAI.ContingencyTables.CompanionFactorialApplication.denominator_positive line 155
def OAI.ContingencyTables.CompanionFactorialApplication.f line 160
def OAI.ContingencyTables.CompanionFactorialApplication.g line 163
theorem OAI.ContingencyTables.CompanionFactorialApplication.first_properties line 168
Source documentation
The manuscript's actual factorial lift is positive on its degree and has its omission signature, derived from the literal count.
```
theorem first_properties (A : Instance I J) (alpha : ℝ) (ha : 0≤alpha) :
    BinaryContraction.DegreePositive (f A alpha) (Fintype.card (Labels A)) ∧
      BinaryContraction.OmissionProperty (f A alpha) (Fintype.card (Labels A)) := by
…
```
Mentions: OAI.ContingencyTables.CompanionFactorialApplication.Instance, OAI.ContingencyTables.BinaryContraction.DegreePositive, OAI.ContingencyTables.CompanionFactorialApplication.f, OAI.ContingencyTables.CompanionFactorialApplication.Labels, OAI.ContingencyTables.BinaryContraction.OmissionProperty
theorem OAI.ContingencyTables.CompanionFactorialApplication.second_properties line 190
Source documentation
The dual factorial lift retains positivity and has its actual addition signature from the globally reflected raw count.
```
theorem second_properties (A : Instance I J) (alpha : ℝ) (ha : 0≤alpha) :
    BinaryContraction.DegreePositive (g A alpha) (Fintype.card (Labels A)) ∧
      BinaryContraction.AdditionProperty (g A alpha) (Fintype.card (Labels A)) := by
…
```
Mentions: OAI.ContingencyTables.CompanionFactorialApplication.Instance, OAI.ContingencyTables.BinaryContraction.DegreePositive, OAI.ContingencyTables.CompanionFactorialApplication.g, OAI.ContingencyTables.CompanionFactorialApplication.Labels, OAI.ContingencyTables.BinaryContraction.AdditionProperty
theorem OAI.ContingencyTables.CompanionFactorialApplication.chain_comparison line 216
Source documentation
The actual paired-label chain has the required pointwise q=W² comparison, with the source count appearing identically in both lifts.
```
theorem chain_comparison (A : Instance I J) (alpha : ℝ) (S : Set (Labels A×Bool))
    (hS : CommonBasesFPRAS.ChainState TwoLiftStates.pairs S) :
    (1/(A.W:ℝ)^2)*f A alpha S≤g A alpha S ∧ g A alpha S≤(A.W:ℝ)^2*f A alpha S := by
…
```
Mentions: OAI.ContingencyTables.CompanionFactorialApplication.Instance, OAI.ContingencyTables.CompanionFactorialApplication.Labels, OAI.CommonBasesFPRAS.ChainState, OAI.ContingencyTables.TwoLiftStates.pairs, OAI.ContingencyTables.CompanionFactorialApplication.f, OAI.ContingencyTables.CompanionFactorialApplication.g