ComputedCountingWords.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual counting experiment on original bounded-table inputs

This is the positive-label branch of the computed-input experiment. Its output is the stored adaptive rational estimate, after independent median amplification. Only the cited analytic/flow inputs are external.

def OAI.ContingencyTables.ComputedCountingWords.root line 21
def OAI.ContingencyTables.ComputedCountingWords.bitCount line 27
def OAI.ContingencyTables.ComputedCountingWords.estimate line 34
theorem OAI.ContingencyTables.ComputedCountingWords.positive_success line 44
Source documentation
The computed preprocessing and schedule satisfy every input of the proved adaptive-history theorem. There is no supplied forest, baseline, endpoint table, or oracle-error assumption in this statement.
```
theorem positive_success (hEK : PublishedEdmondsKarp.EdmondsKarp1972Theorem1)
    (hPL : ∀ q,PublishedInputs.FiniteBoxPrekopaLeindler q)
    (hCheeger : ∀ q k,PublishedInputs.FiniteCheeger (Grid (I:=Fin q) k))
…
```
Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.EdmondsKarp1972Theorem1, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger