Bounds.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.formulaBits_length line 11
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_variables line 19
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_clauses line 24
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_two line 29
def OAI.MaxCutGames.Foundations.Hastad.SourceBounds.bitCountFormula line 35
Source documentation
The two padded long-code tables and one global dummy bit.
```
def bitCountFormula (n m u : ℕ) : ℕ :=
…
```
def OAI.MaxCutGames.Foundations.Hastad.SourceBounds.bitCoefficient line 39
Source documentation
Depends on the fixed repetition count alone.
```
def bitCoefficient (u : ℕ) : ℕ := 2 ^ (2 ^ u) + 2 ^ (8 ^ u) + 1
```
def OAI.MaxCutGames.Foundations.Hastad.SourceBounds.testCoefficient line 43
Source documentation
The slot tuples, two queries, and noise tapes per clause tuple. The empty-context branch uses the global dummy and adds no random tape.
```
def testCoefficient (u D : ℕ) : ℕ :=
…
```
def OAI.MaxCutGames.Foundations.Hastad.SourceBounds.occurrenceCoefficient line 47
Source documentation
The total encoding also handles an empty formula with one dummy equation.
```
def occurrenceCoefficient (u D : ℕ) : ℕ := testCoefficient u D + 1
```
Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceBounds.testCoefficient
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.one_le_input_power line 49
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.bitCountFormula_le_input line 55
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.testCountFormula_le_input line 70
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.testCountFormula_add_one_le_input line 80
def OAI.MaxCutGames.Foundations.Hastad.SourceBounds.sourceSizeBound line 89
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.sourceBits_length_le line 92
def OAI.MaxCutGames.Foundations.Hastad.SourceBounds.sourcePolynomial line 103
Source documentation
One explicit output-length polynomial for each fixed u,D.
```
noncomputable def sourcePolynomial (u D : ℕ) : Polynomial ℕ :=
…
```
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.sourcePolynomial_eval line 108
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.card_testTape line 116
Source documentation
Exact cardinality of the actual fixed query/noise tape.
```
theorem card_testTape (u D : ℕ) :
    Fintype.card (SourceTape.TestTape (I u) (J u) D) =
      2 ^ (2 ^ u) * (D ^ (8 ^ u) * 2 ^ (8 ^ u)) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceTape.TestTape
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.testTapeEncoding_size line 122
Source documentation
The executable radix enumeration has the same fixed size.
```
theorem testTapeEncoding_size (u D : ℕ) :
    (SourceOccurrences.testTapeEncoding u D).size =
      2 ^ (2 ^ u) * (D ^ (8 ^ u) * 2 ^ (8 ^ u)) := rfl
```
Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.testTapeEncoding

theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.card_sourceIndex line 127

Source documentation

Cardinality of the actual complete random-tape population.

theorem card_sourceIndex (F : Formula) (u D : ℕ) :
    Fintype.card (SourceIndex F u D) =
      (F.clauses.length ^ u * 3 ^ u) *
        (2 ^ (2 ^ u) * (D ^ (8 ^ u) * 2 ^ (8 ^ u))) := by
…

theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.nBits_le_input line 135
Source documentation
Bound on the actual variable count, including padded addresses and dummy.
```
theorem nBits_le_input (F : Formula) (u : ℕ) :
    nBits F u ≤ bitCoefficient u * (Complexity.formulaBits F).length ^ u := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceBounds.bitCoefficient, OAI.MaxCutGames.Foundations.Complexity.formulaBits
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.rawSourceList_length_eq line 141
Source documentation
Exact list size retains every repeated sampled context and equation.
```
theorem rawSourceList_length_eq (F : Formula) (u D : ℕ) :
    (rawSourceList F u D).length = testCoefficient u D * F.clauses.length ^ u := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceBounds.testCoefficient
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.rawSourceList_length_le_input line 147
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.sourceList_length_le_input line 155
Source documentation
Bound on the total actual list, also covering the empty-formula branch.
```
theorem sourceList_length_le_input (F : Formula) (u D : ℕ) :
    (sourceList F u D).length ≤
      occurrenceCoefficient u D * (Complexity.formulaBits F).length ^ u := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceBounds.occurrenceCoefficient, OAI.MaxCutGames.Foundations.Complexity.formulaBits
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.sourceInput_bits_polynomial line 165
theorem OAI.MaxCutGames.Foundations.Hastad.SourceBounds.fixed_parameters_source_size line 174
Source documentation
Fixed parameters supply one polynomial uniformly for all actual inputs.
```
theorem fixed_parameters_source_size (u D : ℕ) (hD : 0 < D) :
    ∃ p : Polynomial ℕ, ∀ F : Formula,
      (SourceEncoding.inputBits (sourceInput F u D hD)).length ≤
        p.eval (Complexity.formulaBits F).length :=
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.formulaBits