RootedFactorialApplication.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual factorial lifts of the selected-root completion count

def OAI.ContingencyTables.RootedFactorialApplication.f line 16
def OAI.ContingencyTables.RootedFactorialApplication.g line 19
theorem OAI.ContingencyTables.RootedFactorialApplication.first_properties line 24
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) (R : RootedCompletion.Selection A.T) (alpha : ℝ) (ha : 0≤alpha) :
    BinaryContraction.DegreePositive (f A R alpha) (Fintype.card (Labels A)) ∧
      BinaryContraction.OmissionProperty (f A R alpha) (Fintype.card (Labels A)) := by
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.BinaryContraction.DegreePositive, OAI.ContingencyTables.RootedFactorialApplication.f, OAI.ContingencyTables.BinaryContraction.OmissionProperty
theorem OAI.ContingencyTables.RootedFactorialApplication.second_properties line 46
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) (R : RootedCompletion.Selection A.T) (alpha : ℝ) (ha : 0≤alpha) :
    BinaryContraction.DegreePositive (g A R alpha) (Fintype.card (Labels A)) ∧
      BinaryContraction.AdditionProperty (g A R alpha) (Fintype.card (Labels A)) := by
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.BinaryContraction.DegreePositive, OAI.ContingencyTables.RootedFactorialApplication.g, OAI.ContingencyTables.BinaryContraction.AdditionProperty
theorem OAI.ContingencyTables.RootedFactorialApplication.chain_comparison line 72
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) (R : RootedCompletion.Selection A.T) (alpha : ℝ) (S : Set (Labels A×Bool))
    (hS : CommonBasesFPRAS.ChainState TwoLiftStates.pairs S) :
    (1/(A.W:ℝ)^2)*f A R alpha S≤g A R alpha S ∧ g A R alpha S≤(A.W:ℝ)^2*f A R alpha S := by
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.CommonBasesFPRAS.ChainState, OAI.ContingencyTables.TwoLiftStates.pairs, OAI.ContingencyTables.RootedFactorialApplication.f, OAI.ContingencyTables.RootedFactorialApplication.g