ConstructionSignatureBudget.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The sparse budget for the actual construction

The outer choice contains every actual cyclic label word. Its proved row bound therefore controls the literal signatures of the actual affine family. All arithmetic and mesh estimates are discharged for the chosen prime-scale data; the resulting eventual threshold is uniform over those data and outer choices.

theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.actualFullLabel_eq_fullLabel line 28
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.actualFullLabelWord_eq_fullLabelWord line 33
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice.words_card_pos line 40
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice.card_global_words_le line 44
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice.log_words_card_le line 56
Source documentation
The degree-six global row count has entropy constant 520.
```
theorem log_words_card_le {s : Data k} {hk : 3 ≤ k}
    (o : OuterChoice s hk) (hk32 : 32 ≤ k) :
    Real.log (o.words.card : ℝ) ≤
      520 * (k : ℝ) ^ (3 / 10 : ℝ) * Real.log k := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice.card_affine_signatures_le line 92
Source documentation
The actual affine family retains the actual geometric keys and colors.
```
theorem card_affine_signatures_le {s : Data k} {hk : 3 ≤ k}
    [NeZero (s.q ^ dimension k)] (o : OuterChoice s hk) :
    ((affineProgressions s.q (dimension k) (lambda k) k).image
      (cyclicSignature (k := k) (fun n => o.color (fullLabel s hk n))
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice, OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda, OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabel
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice.log_affine_signatures_le line 106
Source documentation
Literal affine signatures have entropy constant 628, also when their finite image is empty.
```
theorem log_affine_signatures_le {s : Data k} {hk : 3 ≤ k}
    [NeZero (s.q ^ dimension k)] (o : OuterChoice s hk) (hk32 : 32 ≤ k) :
    Real.log (max 1
      (((affineProgressions s.q (dimension k) (lambda k) k).image
        (cyclicSignature (k := k) (fun n => o.color (fullLabel s hk n))
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice, OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda, OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabel
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.eventually_outerChoice_sparse_budget line 144
Source documentation
A single threshold makes the exact sparse-perturbation budget less than one for every actual arithmetic datum and every actual outer choice.
```
theorem eventually_outerChoice_sparse_budget :
    ∀ᶠ k : ℕ in atTop, ∀ hk : 3 ≤ k, ∀ s : Data k, ∀ o : OuterChoice s hk,
      letI : NeZero (s.q ^ dimension k) := groupSize_neZero s
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice, OAI.QuantitativeVanDerWaerden.ConstructionModel.groupSize_neZero