AlgorithmStatements.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Main algorithm statements for result 200

The samplers and counter use a finite transition table, independent fair bits, binary inputs and explicit bit-operation runtime bounds. No counting or sampling oracle is part of the machine. The exact sampler's expected runtime uses a summable tail series, avoiding the default value of an undefined infinite sum.

abbrev OAI.ContingencyTables.Algorithms.Machine line 20
Also declared: ComparatorChallenges/ContingencyTables.lean:103 (same declaration text).
abbrev OAI.ContingencyTables.Algorithms.Symbol line 21
Also declared: ComparatorChallenges/ContingencyTables.lean:104 (same declaration text).
def OAI.ContingencyTables.Algorithms.encodeMatrix line 23
Also declared: ComparatorChallenges/ContingencyTables.lean:106 (same declaration text).
def OAI.ContingencyTables.Algorithms.encodeMargins line 26
Also declared: ComparatorChallenges/ContingencyTables.lean:109 (same declaration text).
def OAI.ContingencyTables.Algorithms.encodeSamplingInput line 31
Also declared: ComparatorChallenges/ContingencyTables.lean:114 (same declaration text).
def OAI.ContingencyTables.Algorithms.encodeCountingInput line 34
Also declared: ComparatorChallenges/ContingencyTables.lean:117 (same declaration text).
theorem OAI.ContingencyTables.Algorithms.alphabetSize_neZero line 39
Source documentation
The tape alphabet has positive cardinality.
Also declared: ComparatorChallenges/ContingencyTables.lean:122 (same declaration text).
```
theorem alphabetSize_neZero : NeZero (8 : ℕ) := inferInstance
```
def OAI.ContingencyTables.Algorithms.OutputsTable line 42
Source documentation
A halted tape contains the row-major binary matrix encoding.
Also declared: ComparatorChallenges/ContingencyTables.lean:125 (same declaration text).
```
def OutputsTable (A : Machine) (input : List Symbol) {t m n : ℕ}
    (bits : Fin t → Bool) (X : Fin m → Fin n → ℕ) : Prop :=
…
```
Mentions: OAI.ContingencyTables.Algorithms.Machine, OAI.ContingencyTables.Algorithms.Symbol
def OAI.ContingencyTables.Algorithms.tableMass line 49
Also declared: ComparatorChallenges/ContingencyTables.lean:132 (same declaration text).
def OAI.ContingencyTables.Algorithms.haltMass line 55
Also declared: ComparatorChallenges/ContingencyTables.lean:138 (same declaration text).
def OAI.ContingencyTables.Algorithms.samplingSize line 60
Also declared: ComparatorChallenges/ContingencyTables.lean:143 (same declaration text).
def OAI.ContingencyTables.Algorithms.BoundedSamplingStatement line 65
Source documentation
Paper 200-01, Theorem main(i): bounded runtime on every random tape and total variation at most 2⁻ᵏ, with freely varying dimensions.
Also declared: ComparatorChallenges/ContingencyTables.lean:148 (same declaration text).
```
def BoundedSamplingStatement : Prop :=
…
```
def OAI.ContingencyTables.Algorithms.ExactSamplingStatement line 79
Source documentation
Paper 200-01, Theorem main(ii): every halted output is feasible, each table has limiting mass 1/|Ω|, termination has probability one, and the expected number of bit operations is bounded by a uniform polynomial.
Also declared: ComparatorChallenges/ContingencyTables.lean:162 (same declaration text).
```
def ExactSamplingStatement : Prop :=
…
```
def OAI.ContingencyTables.Algorithms.count line 93
Also declared: ComparatorChallenges/ContingencyTables.lean:176 (same declaration text).
def OAI.ContingencyTables.Algorithms.countingTime line 96
Also declared: ComparatorChallenges/ContingencyTables.lean:179 (same declaration text).
def OAI.ContingencyTables.Algorithms.goodCountingTapes line 101
Also declared: ComparatorChallenges/ContingencyTables.lean:184 (same declaration text).
def OAI.ContingencyTables.Algorithms.CountingStatement line 111
Source documentation
Paper 200-02, Theorem main. The input length includes the rational accuracy parameters, and infeasible inputs always produce exactly zero.
Also declared: ComparatorChallenges/ContingencyTables.lean:194 (same declaration text).
```
def CountingStatement : Prop :=
…
```