SignatureCounting.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Counting literal signatures on affine progressions

Only coefficient triples whose evaluations lie in the specified bounded interval are counted. Integer threshold comparisons, including equality, determine their floor words. The proved arrangement estimate in dimension three gives 25 * (k * (B + 1) + 1)^8; no cubic arrangement bound is asserted.

The full label word and the floor word determine each original color and literal (box, integer band) key. The product count never renames keys.

def OAI.QuantitativeVanDerWaerden.quadraticValue line 33
Source documentation
Evaluation of the three actual quadratic coefficients.
```
def quadraticValue (θ : Fin 3 → ℝ) (j : ℕ) : ℝ :=
…
```
def OAI.QuantitativeVanDerWaerden.quadraticFloorWord line 36
def OAI.QuantitativeVanDerWaerden.boundedQuadraticDomain line 41
Source documentation
The evaluation restriction is essential: unrestricted coefficient triples have infinitely many literal integer floor words.
```
def boundedQuadraticDomain (k B : ℕ) : Set (Fin 3 → ℝ) :=
…
```
def OAI.QuantitativeVanDerWaerden.quadraticComparisonForm line 44
theorem OAI.QuantitativeVanDerWaerden.quadraticComparisonForm_eval line 48
def OAI.QuantitativeVanDerWaerden.quadraticComparisonForms line 54
Source documentation
One form for every position and every threshold 0,...,B.
```
def quadraticComparisonForms (k B : ℕ) : Fin (k * (B + 1)) → AffineForm 3 :=
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AffineForm
theorem OAI.QuantitativeVanDerWaerden.quadraticComparisonForms_eval line 59
theorem OAI.QuantitativeVanDerWaerden.floor_le_of_comparisons line 68
Source documentation
Testing the threshold equal to the first floor forces the corresponding lower bound for the second floor. The threshold is an original integer.
```
private theorem floor_le_of_comparisons {B : ℕ} {x y : ℝ}
    (hx0 : 0 ≤ x) (hxB : x ≤ (B : ℝ))
    (h : ∀ b : Fin (B + 1), ternarySign (x - b.val) = ternarySign (y - b.val)) :
    ⌊x⌋ ≤ ⌊y⌋ := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ternarySign
theorem OAI.QuantitativeVanDerWaerden.floor_eq_of_comparisons line 88
theorem OAI.QuantitativeVanDerWaerden.quadraticFloorWord_eq_of_signVector_eq line 97
Source documentation
Sign equality determines the entire floor word, with both zero and upper boundary evaluations allowed.
```
theorem quadraticFloorWord_eq_of_signVector_eq (k B : ℕ)
    {θ η : Fin 3 → ℝ} (hθ : θ ∈ boundedQuadraticDomain k B)
    (hη : η ∈ boundedQuadraticDomain k B)
    (h : signVector (quadraticComparisonForms k B) θ =
      signVector (quadraticComparisonForms k B) η) :
    quadraticFloorWord k θ = quadraticFloorWord k η := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.boundedQuadraticDomain, OAI.QuantitativeVanDerWaerden.signVector, OAI.QuantitativeVanDerWaerden.quadraticComparisonForms, OAI.QuantitativeVanDerWaerden.quadraticFloorWord
def OAI.QuantitativeVanDerWaerden.normSqCoefficients line 110
Source documentation
The genuine coefficients of the squared norm on an affine line.
```
def normSqCoefficients {D : ℕ} (A B : Vec D) : Fin 3 → ℝ :=
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Vec
theorem OAI.QuantitativeVanDerWaerden.quadraticValue_normSqCoefficients line 113
theorem OAI.QuantitativeVanDerWaerden.normSq_scaled_le line 122
Source documentation
Coarse natural bound used in the counting estimate. Centered coordinate bounds imply this for the actual q-scaled representative.
```
theorem normSq_scaled_le {D : ℕ} (q : ℕ) (x : Vec D)
    (hx : ∀ i, -(1 / 2 : ℝ) ≤ x i ∧ x i < 1 / 2) :
    normSq (fun i => (q : ℝ) * x i) ≤ ((D * q ^ 2 : ℕ) : ℝ) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Vec, OAI.QuantitativeVanDerWaerden.normSq
theorem OAI.QuantitativeVanDerWaerden.normSq_scaled_yRep_bounds line 136
theorem OAI.QuantitativeVanDerWaerden.finite_quadraticFloorWords line 143
Source documentation
The exact finite image of bounded quadratic floor words. In particular, the family also covers triples not arising from squared norms.
```
theorem finite_quadraticFloorWords (k B : ℕ) :
    ∃ W : Finset (Fin k → ℤ),
      (∀ w, w ∈ W ↔ ∃ θ ∈ boundedQuadraticDomain k B, quadraticFloorWord k θ = w) ∧
      W.card ≤ 25 * (k * (B + 1) + 1) ^ 8 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.boundedQuadraticDomain, OAI.QuantitativeVanDerWaerden.quadraticFloorWord

def OAI.QuantitativeVanDerWaerden.literalSignature line 154

Source documentation

The color and box are fixed functions of the full label, while the band is the literal integer value. No signature-dependent coding is used.

def literalSignature {Label : Type uLabel} {Box : Type uBox} {k : ℕ}
    (color : Label → Bool) (boxOf : Label → Box)
    (labels : Fin k → Label) (bands : Fin k → ℤ) : Fin k → Bool × (Box × ℤ) :=
…

theorem OAI.QuantitativeVanDerWaerden.card_literalSignatures_le_mul line 161

Source documentation

Finite-image factorization: one full label word and one band word suffice. The ambient label and box types need not be finite.

theorem card_literalSignatures_le_mul {ι : Type uIndex} {Label : Type uLabel} {Box : Type uBox} {k : ℕ}
    [DecidableEq Label] [DecidableEq Box]
    (P : Finset ι) (labels : ι → Fin k → Label) (bands : ι → Fin k → ℤ)
    (color : Label → Bool) (boxOf : Label → Box) (W : Finset (Fin k → ℤ))
    (hW : ∀ p ∈ P, bands p ∈ W) :
    (P.image (fun p => literalSignature color boxOf (labels p) (bands p))).card ≤
      (P.image labels).card * W.card := by
…

Mentions: OAI.QuantitativeVanDerWaerden.literalSignature

theorem OAI.QuantitativeVanDerWaerden.card_quadraticSignatures_le line 182

theorem OAI.QuantitativeVanDerWaerden.card_affineNormSignatures_le line 197

Source documentation

Actual affine squared-norm words have the preceding coefficient witnesses. Affinity and the evaluation bound are stated for the finite family being counted.

theorem card_affineNormSignatures_le {ι : Type uIndex} {Label : Type uLabel} {Box : Type uBox} {k D B : ℕ}
    [DecidableEq Label] [DecidableEq Box]
    (P : Finset ι) (labels : ι → Fin k → Label) (point : ι → Fin k → Vec D)
    (color : Label → Bool) (boxOf : Label → Box)
    (haff : ∀ p ∈ P, ∃ A C : Vec D,
      ∀ j : Fin k, point p j = fun i => A i + (j.val : ℝ) * C i)
    (hbound : ∀ p ∈ P, ∀ j, normSq (point p j) ≤ (B : ℝ)) :
    (P.image (fun p => literalSignature color boxOf (labels p)
      (fun j => ⌊normSq (point p j)⌋))).card ≤
      (P.image labels).card * (25 * (k * (B + 1) + 1) ^ 8) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.Vec, OAI.QuantitativeVanDerWaerden.normSq, OAI.QuantitativeVanDerWaerden.literalSignature

theorem OAI.QuantitativeVanDerWaerden.card_affine_yRep_signatures_le line 223

Source documentation

The concrete centered cyclic representative supplies its own bounded evaluation domain. The coarse natural threshold is exactly D*q^2.

theorem card_affine_yRep_signatures_le {ι : Type uIndex} {Label : Type uLabel} {Box : Type uBox} {k q D dilation : ℕ}
    [DecidableEq Label] [DecidableEq Box]
    (P : Finset ι) (labels : ι → Fin k → Label)
    (n : ι → Fin k → CyclicGroup q D) (color : Label → Bool) (boxOf : Label → Box)
    (haff : ∀ p ∈ P, ∃ A C : Vec D, ∀ j : Fin k,
      (fun i => (q : ℝ) * yRep q D dilation (n p j) i) =
        fun i => A i + (j.val : ℝ) * C i) :
    (P.image (fun p => literalSignature color boxOf (labels p)
      (fun j => ⌊normSq (fun i => (q : ℝ) * yRep q D dilation (n p j) i)⌋))).card ≤
      (P.image labels).card * (25 * (k * (D * q ^ 2 + 1) + 1) ^ 8) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.Vec, OAI.QuantitativeVanDerWaerden.yRep, OAI.QuantitativeVanDerWaerden.literalSignature, OAI.QuantitativeVanDerWaerden.normSq

theorem OAI.QuantitativeVanDerWaerden.card_affine_yRep_fullLabel_signatures_le line 240

Source documentation

With full labels the original second-system box is precisely the second projection, an entire vector of literal interval identities.

theorem card_affine_yRep_fullLabel_signatures_le {ι : Type uIndex} {U : Type uU} {V : Type uV} {k q D dilation : ℕ}
    [DecidableEq U] [DecidableEq V]
    (P : Finset ι) (labels : ι → Fin k → FullLabel D U V)
    (n : ι → Fin k → CyclicGroup q D) (color : FullLabel D U V → Bool)
    (haff : ∀ p ∈ P, ∃ A C : Vec D, ∀ j : Fin k,
      (fun i => (q : ℝ) * yRep q D dilation (n p j) i) =
        fun i => A i + (j.val : ℝ) * C i) :
    (P.image (fun p => literalSignature color Prod.snd (labels p)
      (fun j => ⌊normSq (fun i => (q : ℝ) * yRep q D dilation (n p j) i)⌋))).card ≤
      (P.image labels).card * (25 * (k * (D * q ^ 2 + 1) + 1) ^ 8) :=
…

Mentions: OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.FullLabel, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.Vec, OAI.QuantitativeVanDerWaerden.yRep, OAI.QuantitativeVanDerWaerden.literalSignature, OAI.QuantitativeVanDerWaerden.normSq

def OAI.QuantitativeVanDerWaerden.signatureKeyMap line 254
Source documentation
In the finite-key application this map is the subtype's injective inclusion into the ambient literal box/band pairs.
```
def signatureKeyMap {K : Type uK} {L : Type uL} {k : ℕ} (f : K → L)
    (σ : Fin k → Bool × K) : Fin k → Bool × L :=
…
```
theorem OAI.QuantitativeVanDerWaerden.signatureKeyMap_injective line 258
theorem OAI.QuantitativeVanDerWaerden.card_signatureKeyMap_image line 266