CompanionScaleSizes.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Explicit sizes at the companion's bounded-capacity scale

The unary copy labels are used only below the chosen cutoff, not below the original binary-encoded capacities. These estimates retain the cutoff dependency and then substitute the paper's actual polynomial scale. The initial precision is bounded without executing a real log.

def OAI.ContingencyTables.CompanionScaleSizes.strength line 19
def OAI.ContingencyTables.CompanionScaleSizes.bins line 22
def OAI.ContingencyTables.CompanionScaleSizes.cutoff line 24
def OAI.ContingencyTables.CompanionScaleSizes.finalPhase line 26
lemma OAI.ContingencyTables.CompanionScaleSizes.strength_source line 28
lemma OAI.ContingencyTables.CompanionScaleSizes.cutoff_eq line 38
lemma OAI.ContingencyTables.CompanionScaleSizes.strength_le line 42
lemma OAI.ContingencyTables.CompanionScaleSizes.cutoff_strength_le line 53
Source documentation
Choosing an integer reciprocal-accuracy bound suffices for every subsequent numeric loop bound.
```
lemma cutoff_strength_le (d K E : ℕ) (epsilon : ℚ) (hE : 1/epsilon≤(E:ℚ)) :
    cutoff d (strength d K epsilon)≤3276800*d^4*K^2*E := by
…
```
Mentions: OAI.ContingencyTables.CompanionScaleSizes.cutoff, OAI.ContingencyTables.CompanionScaleSizes.strength
lemma OAI.ContingencyTables.CompanionScaleSizes.label_count_le line 63
lemma OAI.ContingencyTables.CompanionScaleSizes.scheduled_label_count line 70
lemma OAI.ContingencyTables.CompanionScaleSizes.precision_le line 76
theorem OAI.ContingencyTables.CompanionScaleSizes.initialBits_polynomial_bound line 82
theorem OAI.ContingencyTables.CompanionScaleSizes.scheduled_initialBits line 90
Source documentation
After substituting W=100dB, B=16Cd², the complete initializer word length is an explicit polynomial in d, C, and its accuracy exponent.
```
theorem scheduled_initialBits (A : Instance I J) (C h : ℕ) (hW : A.W=cutoff A.d C) :
    initialBits A (precision A h)≤
      A.d*(1600*C*A.d^3+1)*(A.d*(4800*C*A.d^3+1)+1+h) := by
…
```
Mentions: OAI.ContingencyTables.CompanionScaleSizes.cutoff