CompanionArithmeticStep.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Coordinate arithmetic for the companion proposal

The arithmetic and abstract proposals consume equal fixed word lengths. Oracle and acceptance words are disjoint, and their full one-step laws agree, giving the same trajectory error bound.

def OAI.ContingencyTables.CompanionArithmeticStep.regroup line 21
lemma OAI.ContingencyTables.CompanionArithmeticStep.word_finish_law line 27
abbrev OAI.ContingencyTables.CompanionArithmeticStep.RestWord line 40
def OAI.ContingencyTables.CompanionArithmeticStep.wordSplit line 43
def OAI.ContingencyTables.CompanionArithmeticStep.finish line 48
def OAI.ContingencyTables.CompanionArithmeticStep.step line 60
lemma OAI.ContingencyTables.CompanionArithmeticStep.source_step_eq_finish line 67
theorem OAI.ContingencyTables.CompanionArithmeticStep.step_law line 94
Source documentation
Exact equality of complete one-step laws, including all holding probability. Weight calls and the acceptance coin have not been reused.
```
theorem step_law (A : Instance I J) (C K j k : ℕ)
    (hK : 1≤K) (hW : 100*A.d*K≤A.W) (xi : ℚ)
    (v : Grid (I := Fin (dimension A)) K) (w : CompanionRationalUpdates.Pair A → CompanionRationalUpdates.Pair A → ℚ)
…
```
Mentions: OAI.ContingencyTables.CompanionRationalUpdates.Pair
def OAI.ContingencyTables.CompanionArithmeticStep.recordedWalk line 114
Source documentation
The full recorded finite-word path therefore retains the proved joint-history distribution, rather than merely its terminal marginal.
```
def recordedWalk (A : Instance I J) (C K j k N n : ℕ)
    (hK : 1≤K) (hW : 100*A.d*K≤A.W) (xi : ℚ)
    (v : Grid (I := Fin (dimension A)) K) (w : CompanionRationalUpdates.Pair A → CompanionRationalUpdates.Pair A → ℚ)
…
```
Mentions: OAI.ContingencyTables.CompanionRationalUpdates.Pair
theorem OAI.ContingencyTables.CompanionArithmeticStep.recordedWalk_law line 121