CyclicSignatures.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Literal signatures of the actual affine cyclic progressions

The family below is defined from the actual centered representative sequence. Its signatures retain the adaptive mesh's interval identities and the integer norm band. The label color is fixed before the Bernoulli perturbation.

def OAI.QuantitativeVanDerWaerden.CyclicColoring.affineProgressions line 26
Source documentation
The designated affine family is the actual nonzero-step family whose centered representative vectors are affine in the sample index.
```
def affineProgressions (q D dilation k : ℕ) [NeZero (q ^ D)] :
    Finset (CyclicGroup q D × CyclicGroup q D) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.CyclicGroup
theorem OAI.QuantitativeVanDerWaerden.CyclicColoring.affineProgressions_subset line 34
theorem OAI.QuantitativeVanDerWaerden.CyclicColoring.mem_affineProgressions line 39
def OAI.QuantitativeVanDerWaerden.CyclicColoring.actualFullLabel line 49
Source documentation
The first-system labels together with the actual second-system boxes.
```
def actualFullLabel {U : Type uU} (mesh : AdaptiveMesh) (q D dilation : ℕ)
    (first : CyclicGroup q D → Fin D → U) (n : CyclicGroup q D) :
    FullLabel D U mesh.Label :=
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.FullLabel
def OAI.QuantitativeVanDerWaerden.CyclicColoring.actualFullLabelWord line 54
theorem OAI.QuantitativeVanDerWaerden.CyclicColoring.card_actual_affine_signatures_le line 63
Source documentation
The actual signature count used by the sparse-perturbation budget. Its only label-count term is the full nonzero-step cyclic label-word image.
```
theorem card_actual_affine_signatures_le {U : Type uU} [DecidableEq U]
    (mesh : AdaptiveMesh) (q D dilation k : ℕ) [NeZero (q ^ D)]
    (first : CyclicGroup q D → Fin D → U)
    (color : FullLabel D U mesh.Label → Bool) :
    ((affineProgressions q D dilation k).image (cyclicSignature (k := k)
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.FullLabel, OAI.QuantitativeVanDerWaerden.CyclicColoring.affineProgressions