CyclicBlockLabels.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Literal cyclic labels on full blocks

An actual cyclic progression is re-anchored at each full block's initial position. Its two rational paths differ from the local realization only by integers, so the literal uniform and adaptive labels agree exactly.

theorem OAI.QuantitativeVanDerWaerden.CyclicBlockLabels.fullBlock_end_le line 20
def OAI.QuantitativeVanDerWaerden.CyclicBlockLabels.cyclicBlockRealization line 28
Source documentation
The actual cyclic representatives at the beginning of a full block, with the original displacement vectors retained.
```
def cyclicBlockRealization (q D lambda k h : ℕ)
    (a d : CyclicGroup q D) (u v : Fin D → ℝ) (b : Fin (k / h)) :
    AnchoredPatterns.Realization D where
…
```
Mentions: OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.Realization
theorem OAI.QuantitativeVanDerWaerden.CyclicBlockLabels.xRep_block_integer_difference line 36
theorem OAI.QuantitativeVanDerWaerden.CyclicBlockLabels.yRep_block_integer_difference line 57

theorem OAI.QuantitativeVanDerWaerden.CyclicBlockLabels.literalFullLabel_block_eq line 81

Source documentation

The canonical literal cyclic label is exactly the full label of the local block realization, including every mesh boundary.

theorem literalFullLabel_block_eq (mesh : AdaptiveMesh)
    (q D lambda meshN k h : ℕ) (hn : 0 < meshN) (hh : 0 < h)
    (a d : CyclicGroup q D) (u v : Fin D → ℝ) (t : Fin D → Fin h)
    (hX : ∀ j, j < k → ∀ i : Fin D, ∃ e : ℤ,
      xRep q D (a + j • d) i - xRep q D a i -
        (j : ℝ) / h * ((t i).val + u i) = e)
    (hY : ∀ j, j < k → ∀ i : Fin D, ∃ e : ℤ,
      yRep q D lambda (a + j • d) i - yRep q D lambda a i -
        (j : ℝ) / h * ((lambda : ℝ) * (t i).val + v i) = e)
    (b : Fin (k / h)) (z : Fin h) :
    literalFullLabel mesh q D lambda meshN hn
        (a + (BlockCoverage.blockIndex k h b z).val • d) =
…

Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.xRep, OAI.QuantitativeVanDerWaerden.yRep, OAI.QuantitativeVanDerWaerden.literalFullLabel, OAI.QuantitativeVanDerWaerden.BlockCoverage.blockIndex

theorem OAI.QuantitativeVanDerWaerden.CyclicBlockLabels.blockColorCount_eq_local line 112
Source documentation
Counting a color in the literal positions of a full block is the same as counting its pullback to the local indices Fin h.
```
theorem blockColorCount_eq_local (k h : ℕ)
    (color : Fin k → Bool) (c : Bool) (b : Fin (k / h)) :
    BlockCoverage.blockColorCount k h color c b =
      (Finset.univ.filter fun z : Fin h =>
        color (BlockCoverage.blockIndex k h b z) = c).card := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.BlockCoverage.blockColorCount, OAI.QuantitativeVanDerWaerden.BlockCoverage.blockIndex