CompanionInitializedRestartLaw.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact law of the complete executed initializer and restart prefix

def OAI.ContingencyTables.CompanionInitializedRestartProgram.parameters line 18
def OAI.ContingencyTables.CompanionInitializedRestartProgram.model line 22
theorem OAI.ContingencyTables.CompanionInitializedRestartProgram.output_padded_sameLaw line 40
Source documentation
The actual list program has the complete finite-word law, including every initialization bias, rejected return and fallback.
```
theorem output_padded_sameLaw (A : Instance (Fin m) (Fin n)) (C K H T N R L j padding : ℕ)
    (hC : 0 < C) (hj : j ≤ rationalHeight A C) (hK : 1 ≤ K)
    (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=CompanionOracleDensity.binWidth A C)
    (epsilon : TreeFraction.Fraction)
    (hxi : 0 < TreeFraction.val (CountingPhaseParametersProgram.noise (parameters A H T N R L epsilon)))
    (z : View A → ℕ) (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K)
…
```
Mentions: OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CountingPhaseParametersProgram.noise, OAI.ContingencyTables.CompanionInitializedRestartProgram.parameters, OAI.ContingencyTables.RootedCatalogGrid.freeCount
theorem OAI.ContingencyTables.CompanionInitializedRestartProgram.model_eq_initializedStages line 106
Source documentation
When the supplied restart time is the computed paper schedule, the reference experiment is precisely initializedStages.
```
theorem model_eq_initializedStages (A : Instance (Fin m) (Fin n)) (C K H N R L j : ℕ)
    (epsilon : TreeFraction.Fraction) (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W)
    (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K)
…
```
Mentions: OAI.ContingencyTables.RootedCatalogGrid.freeCount