ConstructionWordFamily.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A counted family covering the actual cyclic label words

The coordinate representatives of a cyclic progression are real affine progressions modulo integers. Literal partition labels are integer-periodic, so the actual label word belongs to the global family derived from affine comparisons. The centered second-system start is shifted by 1/2; its step is not shifted. No independence of the cyclic coordinates is assumed.

theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabelWord_eq_partitionWord line 26
Source documentation
Exact identification of the actual cyclic word with a word of the two literal circle partitions, including their half-open boundary conventions.
```
theorem fullLabelWord_eq_partitionWord (s : Data k) (hk : 3 ≤ k)
    (ad : Group s × Group s) :
    fullLabelWord s hk ad =
      (uniformPartition (uniformCount k) (uniformCount_pos hk)).fullWord
        (adaptivePartition (mesh s hk)) (dimension k) k
        (xRep s.q (dimension k) ad.1)
        (xRep s.q (dimension k) ad.2)
        (fun i => yRep s.q (dimension k) (lambda k) ad.1 i + 1 / 2)
        (yRep s.q (dimension k) (lambda k) ad.2) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.Group, OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabelWord, OAI.QuantitativeVanDerWaerden.uniformPartition, OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount, OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount_pos, OAI.QuantitativeVanDerWaerden.adaptivePartition, OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh, OAI.QuantitativeVanDerWaerden.xRep, OAI.QuantitativeVanDerWaerden.yRep, OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.exists_fullLabelWord_family line 63
Source documentation
A finite family covering every actual cyclic progression word. The cardinality bound is proved from the two literal partitions, not supplied as a hypothesis. The step may be zero.
```
theorem exists_fullLabelWord_family (s : Data k) (hk : 3 ≤ k) :
    ∃ words : Finset (Fin k → Label s hk),
      (∀ ad : Group s × Group s, fullLabelWord s hk ad ∈ words) ∧
      words.card ≤
        (16 * (3 * k ^ 2 *
          (uniformCount k + Fintype.card (mesh s hk).Label) + 1) ^ 6) ^
          (2 * dimension k) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.Label, OAI.QuantitativeVanDerWaerden.ConstructionModel.Group, OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabelWord, OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount, OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.exists_fullWordFamily line 80
Source documentation
The same bound with the actual adaptive mesh cardinality substituted.
```
theorem exists_fullWordFamily (s : Data k) (hk : 3 ≤ k) :
    ∃ words : Finset (Fin k → Label s hk),
      words.card ≤
        (16 * (3 * k ^ 2 *
          (uniformCount k + 2 * scalarMeshSize k s.q) + 1) ^ 6) ^
          (2 * dimension k) ∧
      ∀ a d : Group s, fullLabelWord s hk (a, d) ∈ words := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.Label, OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount, OAI.QuantitativeVanDerWaerden.ConstructionModel.Group, OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabelWord