CompanionMinMass.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Binary-size minimum mass of the actual companion transversal law

The factorial denominator cancels against the two complementary factorials. The surviving binomial coefficient is bounded by 2^b, giving the p+K exponent used in the paper's restart schedule.

lemma OAI.ContingencyTables.InitialTransversals.localWeight_lower line 17
theorem OAI.ContingencyTables.InitialTransversals.firstLift_plain_lower line 43
Source documentation
On every actual paired transversal, the constant-count factorial display is at least M times 2 to the negative number of copy labels.
```
theorem firstLift_plain_lower (b : C → ℕ) (M : ℝ) (hM : 0 ≤ M)
    (S : Set (Copy b×Bool)) (hS : PlainState pairs S) :
    M*(1/2:ℝ)^(∑ c,b c) ≤
      firstLift (group (cell b)) (fun _ => M) (denominator b) S := by
…
```
Mentions: OAI.ContingencyTables.InitialTransversals.Copy, OAI.ContingencyTables.InitialTransversals.cell, OAI.ContingencyTables.InitialTransversals.denominator
lemma OAI.ContingencyTables.CompanionMinMass.label_card line 68
lemma OAI.ContingencyTables.CompanionMinMass.initial_weight_lower line 72

theorem OAI.ContingencyTables.CompanionMinMass.law_lower line 89

Source documentation

If the finite small-profile domain has at most 2^K points, every actual phase-j transversal has mass at least 2^(-(j+p+K)).

theorem law_lower (A : Instance I J) (K j : ℕ)
    (hB : (∏ s : SmallCell A,((A.b s.val.1 s.val.2:ℝ)+1)) ≤ (2:ℝ)^K)
    (S : Set (Labels A×Bool)) (hS : PlainState pairs S) :
    (1/2:ℝ)^(j+Fintype.card (Labels A)+K) ≤ law A j S := by
…