RootedCatalogStep.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual oracle transition in computed catalog order

Axis proposals are uniform over a bounded dyadic code space. Changing the coordinate order preserves their frequencies, even though it need not preserve the value obtained from an individual proposal word.

lemma OAI.ContingencyTables.RootedCatalogGrid.freeCount_eq line 23
lemma OAI.ContingencyTables.RootedCatalogGrid.freeCount_le line 27
def OAI.ContingencyTables.RootedCatalogGrid.exponent line 31
def OAI.ContingencyTables.RootedCatalogGrid.finiteStepLaw line 35
theorem OAI.ContingencyTables.RootedCatalogGrid.finiteStepLaw_eq line 41
def OAI.ContingencyTables.RootedCatalogGrid.bitStep line 65
def OAI.ContingencyTables.RootedCatalogGrid.bitStepLaw line 74
lemma OAI.ContingencyTables.RootedCatalogGrid.bitStepLaw_eq_finite line 79
theorem OAI.ContingencyTables.RootedCatalogGrid.bitStepLaw_eq line 102
Source documentation
The actual catalog-order finite-word experiment has the exact transition law of the oracle mixing theorem.
```
theorem bitStepLaw_eq (A : Instance (Fin m) (Fin n)) (C a : ℕ) (hC : 0 < C)
    (haH : a≤rationalHeight A C) (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
    {K : ℕ} (hK : 1≤K) (hKB : (K:ℝ)≤CompanionOracleDensity.binWidth A C)
    (v : Grid (I := Fin (freeCount A)) K) :
…
```
Mentions: OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.RootedCatalogGrid.freeCount