TwoLiftStates.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Actual paired states and the two factorial weights

Every physical cell contains an arbitrary finite bundle of paired labels. The plain and one-hole/one-full predicates imply the exact cell count identities. Thus the literal subset lifts agree on plain states and obey the manuscript's W² comparison on every actual chain state.

def OAI.ContingencyTables.TwoLiftStates.group line 21
def OAI.ContingencyTables.TwoLiftStates.pair line 23
def OAI.ContingencyTables.TwoLiftStates.pairs line 25
def OAI.ContingencyTables.TwoLiftStates.width line 28
def OAI.ContingencyTables.TwoLiftStates.viewCount line 31
def OAI.ContingencyTables.TwoLiftStates.occupancy line 34
lemma OAI.ContingencyTables.TwoLiftStates.pair_mem line 37
lemma OAI.ContingencyTables.TwoLiftStates.pair_injective line 41
lemma OAI.ContingencyTables.TwoLiftStates.groupCount_eq_viewCount line 46
lemma OAI.ContingencyTables.TwoLiftStates.width_eq_sum line 56
lemma OAI.ContingencyTables.TwoLiftStates.viewCount_compl line 60
lemma OAI.ContingencyTables.TwoLiftStates.viewCount_le_width line 70
lemma OAI.ContingencyTables.TwoLiftStates.viewCounts_eq_occupancy line 76
lemma OAI.ContingencyTables.TwoLiftStates.occupancy_single line 86
lemma OAI.ContingencyTables.TwoLiftStates.occupancy_empty line 91
lemma OAI.ContingencyTables.TwoLiftStates.occupancy_full line 98
theorem OAI.ContingencyTables.TwoLiftStates.plain_counts line 106
Source documentation
Every actual plain state is balanced in every physical cell.
```
theorem plain_counts (cell : P → C) (S : Set (P × Bool))
    (hS : PlainState pairs S) (c : C) :
    viewCount cell S c false + viewCount cell S c true = width cell c := by
…
```
Mentions: OAI.ContingencyTables.TwoLiftStates.pairs, OAI.ContingencyTables.TwoLiftStates.viewCount, OAI.ContingencyTables.TwoLiftStates.width
lemma OAI.ContingencyTables.TwoLiftStates.defect_occupancy line 114
theorem OAI.ContingencyTables.TwoLiftStates.defect_counts line 133
Source documentation
Cell occupancies of an actual defect have exactly one unit missing at its hole and one unit extra at its full pair, including coinciding cells.
```
theorem defect_counts (cell : P → C) (S : Set (P × Bool)) (p q : P)
    (hS : DefectState pairs (pair p) (pair q) S) (c : C) :
    viewCount cell S c false + viewCount cell S c true + (if cell p=c then 1 else 0) =
      width cell c + (if cell q=c then 1 else 0) := by
…
```
Mentions: OAI.ContingencyTables.TwoLiftStates.pairs, OAI.ContingencyTables.TwoLiftStates.pair, OAI.ContingencyTables.TwoLiftStates.viewCount, OAI.ContingencyTables.TwoLiftStates.width
def OAI.ContingencyTables.TwoLiftStates.denominator line 158
lemma OAI.ContingencyTables.TwoLiftStates.firstLift_eq_cells line 160
lemma OAI.ContingencyTables.TwoLiftStates.secondLift_eq_cells line 169
theorem OAI.ContingencyTables.TwoLiftStates.plain_lifts_agree line 184
Source documentation
Exact agreement of the two literal subset lifts on every plain state.
```
theorem plain_lifts_agree (cell : P → C) (h : ((C × Bool) → ℕ) → ℝ)
    (S : Set (P × Bool)) (hS : PlainState pairs S) :
    secondLift (group cell) h (denominator cell) S = firstLift (group cell) h (denominator cell) S := by
…
```
Mentions: OAI.ContingencyTables.TwoLiftStates.pairs, OAI.ContingencyTables.TwoLiftStates.group, OAI.ContingencyTables.TwoLiftStates.denominator

theorem OAI.ContingencyTables.TwoLiftStates.defect_lifts_compare line 191

Source documentation

The paper's exact W² comparison on every actual defect state.

theorem defect_lifts_compare (cell : P → C) (h : ((C × Bool) → ℕ) → ℝ)
    (S : Set (P × Bool)) (hS : ∃ p q, DefectState pairs (pair p) (pair q) S)
    (W : ℕ) (hW : 0 < W) (hbW : ∀ c, width cell c < W)
    (hh : 0 ≤ h (groupCount (group cell) S)) :
    (1/(W:ℝ)^2) * firstLift (group cell) h (denominator cell) S ≤
        secondLift (group cell) h (denominator cell) S ∧
    secondLift (group cell) h (denominator cell) S ≤
        (W:ℝ)^2 * firstLift (group cell) h (denominator cell) S := by
…

Mentions: OAI.ContingencyTables.TwoLiftStates.pairs, OAI.ContingencyTables.TwoLiftStates.pair, OAI.ContingencyTables.TwoLiftStates.width, OAI.ContingencyTables.TwoLiftStates.group, OAI.ContingencyTables.TwoLiftStates.denominator

lemma OAI.ContingencyTables.TwoLiftStates.denominator_positive line 226
lemma OAI.ContingencyTables.TwoLiftStates.firstLift_nonnegative line 231

theorem OAI.ContingencyTables.TwoLiftStates.chain_lifts_compare line 239

Source documentation

Both inequalities hold on every actual chain state, with no extra assumption about which cells contain the hole and full pair.

theorem chain_lifts_compare (cell : P → C) (h : ((C × Bool) → ℕ) → ℝ)
    (S : Set (P × Bool)) (hS : ChainState pairs S)
    (W : ℕ) (hW : 0 < W) (hbW : ∀ c, width cell c < W)
    (hh : 0 ≤ h (groupCount (group cell) S)) :
    (1/(W:ℝ)^2) * firstLift (group cell) h (denominator cell) S ≤
        secondLift (group cell) h (denominator cell) S ∧
    secondLift (group cell) h (denominator cell) S ≤
        (W:ℝ)^2 * firstLift (group cell) h (denominator cell) S := by
…

Mentions: OAI.ContingencyTables.TwoLiftStates.pairs, OAI.ContingencyTables.TwoLiftStates.width, OAI.ContingencyTables.TwoLiftStates.group, OAI.ContingencyTables.TwoLiftStates.denominator

theorem OAI.ContingencyTables.TwoLiftStates.firstLift_le_square_secondLift line 261
Source documentation
The pointwise comparison used by the actual original-chain variance argument is supplied by the factorial state counts.
```
theorem firstLift_le_square_secondLift (cell : P → C) (h : ((C × Bool) → ℕ) → ℝ)
    (S : Set (P × Bool)) (hS : ChainState pairs S)
    (W : ℕ) (hW : 0 < W) (hbW : ∀ c, width cell c < W)
    (hh : 0 ≤ h (groupCount (group cell) S)) :
    firstLift (group cell) h (denominator cell) S ≤
        (W:ℝ)^2 * secondLift (group cell) h (denominator cell) S := by
…
```
Mentions: OAI.ContingencyTables.TwoLiftStates.pairs, OAI.ContingencyTables.TwoLiftStates.width, OAI.ContingencyTables.TwoLiftStates.group, OAI.ContingencyTables.TwoLiftStates.denominator