ConstructionHeavyLight.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Heavy and light positions in the actual construction

The real-valued heavy threshold used in the block argument and the integer light threshold used in the outer word tests classify exactly the same positions. Both multiplicities count the entire literal progression word.

theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.real_heavy_iff line 20
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.not_real_heavy_iff line 26
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.literalProgressionHeavy_iff_word_heavy line 32
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.selected_lightPositions_eq line 57
Source documentation
The two literal finite sets of light positions agree.
```
theorem selected_lightPositions_eq (s : Data k) (hk : 3 ≤ k) (a d : Group s) :
    BlockCoverage.lightPositions
      (literalProgressionHeavy (mesh s hk) s.q (dimension k) (lambda k)
        (uniformCount k) k (uniformCount_pos hk) a d (cutoff k)) =
      OuterWordTests.lightPositions (cutoff k) (fullLabelWord s hk (a, d)) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.Group, OAI.QuantitativeVanDerWaerden.BlockCoverage.lightPositions, OAI.QuantitativeVanDerWaerden.literalProgressionHeavy, OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh, OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda, OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount, OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount_pos, OAI.QuantitativeVanDerWaerden.OuterWordTests.lightPositions, OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabelWord
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.selected_lightCount_eq line 68
Source documentation
The block-coverage light count is exactly the outer-test light count.
```
theorem selected_lightCount_eq (s : Data k) (hk : 3 ≤ k) (a d : Group s) :
    BlockCoverage.lightCount
      (literalProgressionHeavy (mesh s hk) s.q (dimension k) (lambda k)
        (uniformCount k) k (uniformCount_pos hk) a d (cutoff k)) =
      (OuterWordTests.lightPositions (cutoff k) (fullLabelWord s hk (a, d))).card := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.Group, OAI.QuantitativeVanDerWaerden.BlockCoverage.lightCount, OAI.QuantitativeVanDerWaerden.literalProgressionHeavy, OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh, OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda, OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount, OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount_pos, OAI.QuantitativeVanDerWaerden.OuterWordTests.lightPositions, OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabelWord
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.selected_lightCount_le_of_few line 78
Source documentation
Failure of the many-light-positions branch supplies the real light-count bound required by the long-period coloring theorem.
```
theorem selected_lightCount_le_of_few (s : Data k) (hk : 3 ≤ k) (a d : Group s)
    (hfew : ¬ k ≤ 10 *
      (OuterWordTests.lightPositions (cutoff k) (fullLabelWord s hk (a, d))).card) :
    (BlockCoverage.lightCount
      (literalProgressionHeavy (mesh s hk) s.q (dimension k) (lambda k)
        (uniformCount k) k (uniformCount_pos hk) a d (cutoff k)) : ℝ) ≤
      (k : ℝ) / 10 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.Group, OAI.QuantitativeVanDerWaerden.OuterWordTests.lightPositions, OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabelWord, OAI.QuantitativeVanDerWaerden.BlockCoverage.lightCount, OAI.QuantitativeVanDerWaerden.literalProgressionHeavy, OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh, OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda, OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount, OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount_pos