WitnessCodeBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The concrete witness relation records have polynomial cost per witness.

lemma OAI.TwoPointCorrelations.card_witnessSystemData_exp line 10

theorem OAI.TwoPointCorrelations.card_witnessSystemData_scale line 37

Source documentation

The selected-system metadata fits within the same exp(O(L log²L)) allowance as the underlying word patterns.

theorem card_witnessSystemData_scale (n N : ℕ) (ι : Type*) [Fintype ι]
    (L : ℝ) (hL : 1 ≤ L) (hlog : 1 ≤ Real.log L)
    (hlabels : Fintype.card ι ≤ N + 1) (hnN : n ≤ N + 1)
    (hn : (n : ℝ) ≤ 4 * L) (hN : (N : ℝ) + 1 ≤ L ^ (2 : ℕ)) :
    (Fintype.card (WitnessSystemData n N ι) : ℝ) ≤
      Real.exp (63 * L * (Real.log L) ^ 2) := by
…

Mentions: OAI.TwoPointCorrelations.WitnessSystemData