GreedyCellMachine.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A binary arithmetic machine for one greedy table cell

This is an existing finite tree-machine compiler applied to the actual minimum/subtraction step. It supplies an executable component for the feasible-table initializer, rather than an assumed arithmetic oracle.

def OAI.ContingencyTables.GreedyFeasibleTable.cellUpdate line 18
Source documentation
Assigned entry, remaining row margin, and remaining column margin.
```
def cellUpdate (x : ℕ×ℕ) : ℕ×(ℕ×ℕ) :=
…
```
def OAI.ContingencyTables.GreedyFeasibleTable.cellUpdateRealizer line 23
Source documentation
A fixed finite program over binary-encoded natural numbers. The compiler's correct field proves its literal execution and step bound.
```
def cellUpdateRealizer : Realizer cellUpdate :=
…
```
Mentions: OAI.ContingencyTables.GreedyFeasibleTable.cellUpdate
lemma OAI.ContingencyTables.GreedyFeasibleTable.cellUpdate_balance line 28