DenseCandidateCounts.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Exact accepted counts throughout the enumerated completion box

abbrev OAI.ContingencyTables.DensePrograms.TrialCountContext line 12
def OAI.ContingencyTables.DensePrograms.candidateCountInput line 14
def OAI.ContingencyTables.DensePrograms.candidateCountInputRealizer line 17
lemma OAI.ContingencyTables.DensePrograms.polynomial_candidateCountInput line 23
def OAI.ContingencyTables.DensePrograms.candidateCount line 34
def OAI.ContingencyTables.DensePrograms.candidateCountRealizer line 37
lemma OAI.ContingencyTables.DensePrograms.polynomial_candidateCount line 40
def OAI.ContingencyTables.DensePrograms.candidateCounts line 44
def OAI.ContingencyTables.DensePrograms.candidateCountsRealizer line 47
def OAI.ContingencyTables.DensePrograms.candidateCountMeasure line 52
theorem OAI.ContingencyTables.DensePrograms.work_candidateCounts line 57
Source documentation
Work is polynomial in the number of candidate free vectors and the cached walk vector; no random tapes are enumerated.
```
theorem work_candidateCounts : WorkBound candidateCountsRealizer candidateCountMeasure := by
…
```
Mentions: OAI.ContingencyTables.DensePrograms.candidateCountsRealizer, OAI.ContingencyTables.DensePrograms.candidateCountMeasure
theorem OAI.ContingencyTables.DensePrograms.candidateCount_actual line 80

theorem OAI.ContingencyTables.DensePrograms.candidateCounts_sum line 98

Source documentation

The sum of all enumerated successful counts is exactly the accepted mass numerator. Rejected integer completions contribute zero.

theorem candidateCounts_sum {m n d : ℕ} (R : Option (Fin m) → ℕ)
    (P : Option (Fin n) → ℕ) (hd : 14≤d) (hq : m*n≤d)
    (hR : ∀ i,d^12≤R i) (hP : ∀ j,d^12≤P j) (htotal : ∑ i,R i=∑ j,P j)
    (h : ℕ) (cap : List Bool)
    (hcap : ∀ j : Fin (m*n),FairBits.offsetBitLength
      (integerWidth R P d (finProdFinEquiv.symm j)) h d≤cap.length) :
    (candidateCounts ((tabulateDenseWalk ((marginCode R,marginCode P),(d,h)),cap),
      ((marginCode R,marginCode P),(d,h)))).sum=
      ∑ X : Table R P,(denseTrialCounts R P d hd hR hP finProdFinEquiv h
        (canonicalOrigin (m*n) d (by omega))).count
          (tableTrial R P d hd hR hP finProdFinEquiv X) := by
…

Mentions: OAI.ContingencyTables.FairBits.offsetBitLength, OAI.ContingencyTables.DensePrograms.candidateCounts, OAI.ContingencyTables.DensePrograms.tabulateDenseWalk, OAI.ContingencyTables.DensePrograms.marginCode, OAI.ContingencyTables.Table, OAI.ContingencyTables.DensePrograms.canonicalOrigin

theorem OAI.ContingencyTables.DensePrograms.candidateCounts_failure line 124

Source documentation

The computed subtraction includes every rejected completion and every unused dyadic slot in the actual dense trial.

theorem candidateCounts_failure {m n d : ℕ} (R : Option (Fin m) → ℕ)
    (P : Option (Fin n) → ℕ) (hd : 14≤d) (hq : m*n≤d)
    (hR : ∀ i,d^12≤R i) (hP : ∀ j,d^12≤P j) (htotal : ∑ i,R i=∑ j,P j)
    (h : ℕ) (cap : List Bool)
    (hcap : ∀ j : Fin (m*n),FairBits.offsetBitLength
      (integerWidth R P d (finProdFinEquiv.symm j)) h d≤cap.length) :
    2^denseTrialBits R P d finProdFinEquiv h-
      (candidateCounts ((tabulateDenseWalk ((marginCode R,marginCode P),(d,h)),cap),
        ((marginCode R,marginCode P),(d,h)))).sum=
    ((denseTrialCounts R P d hd hR hP finProdFinEquiv h
      (canonicalOrigin (m*n) d (by omega))).push
        (trialSuccess R P d finProdFinEquiv htotal)).count none := by
…