Generator.lean`

50 declarations, 0 contain sorry, 0 declared as axioms

def OAI.RationalHitting.Generator.D line 10
def OAI.RationalHitting.Generator.regular line 13
Source documentation
Entrywise regular representation, flattening and fixed row-major reindexing.
```
def regular (e : ℕ) : Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e))
    (CyclotomicRing.R e) →+* Mat (D e) :=
…
```
Mentions: OAI.RationalHitting.CyclotomicRing.dimension, OAI.RationalHitting.CyclotomicRing.R, OAI.RationalHitting.Mat, OAI.RationalHitting.Generator.D
def OAI.RationalHitting.Generator.grid line 20
Source documentation
The fixed lexicographic three-dimensional integer grid, encoded by Fin H.
```
def grid (H : ℕ) : List (Fin 3 → Fin H) :=
…
```
lemma OAI.RationalHitting.Generator.mem_grid line 24
lemma OAI.RationalHitting.Generator.grid_length line 30
def OAI.RationalHitting.Generator.Zring line 34
Source documentation
The polynomial lift is evaluated over the exact rational quotient.
```
def Zring (n N e : ℕ) (x : Fin 3 → ℕ) (i : Fin (n+1)) :
    Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) (CyclotomicRing.R e) :=
…
```
Mentions: OAI.RationalHitting.CyclotomicRing.dimension, OAI.RationalHitting.CyclotomicRing.R
def OAI.RationalHitting.Generator.Z line 39
def OAI.RationalHitting.Generator.tupleAt line 41
def OAI.RationalHitting.Generator.atPoint line 45
Source documentation
The filtering step tests only Z_0, and receives no formula.
```
def atPoint (n N e : ℕ) (x : Fin 3 → ℕ) : Option (Tuple n (D e)) :=
…
```
Mentions: OAI.RationalHitting.Tuple, OAI.RationalHitting.Generator.D
def OAI.RationalHitting.Generator.output line 48
lemma OAI.RationalHitting.Generator.length_output_le line 53

lemma OAI.RationalHitting.Generator.transfer line 58

Source documentation

The actual emitted rational normalization is the homomorphic image of the quotient normalization. Consequently every original inverse occurrence is kept.

lemma transfer {n N e : ℕ} (x : Fin 3 → ℕ) (f : Formula n)
    (z : (Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e))
      (CyclotomicRing.R e))ˣ)
    (hz : (z : Matrix _ _ _) = Zring n N e x 0)
    (v : Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) (CyclotomicRing.R e))
    (hf : f.Eval (algebraMap ℚ _) (fun i => (↑z⁻¹ : Matrix _ _ _) * Zring n N e x i.succ) v)
    (hu : IsUnit v) :
    ∃ a, Evaluates f (tupleAt n N e x) a ∧ IsUnit a := by
…

Mentions: OAI.RationalHitting.Formula, OAI.RationalHitting.CyclotomicRing.dimension, OAI.RationalHitting.CyclotomicRing.R, OAI.RationalHitting.Generator.Zring, OAI.RationalHitting.Evaluates, OAI.RationalHitting.Generator.tupleAt

lemma OAI.RationalHitting.Generator.emitted line 78
abbrev OAI.RationalHitting.Generator.WitnessField line 95
instance OAI.RationalHitting.Generator.witnessCharZero line 96
def OAI.RationalHitting.Generator.witnessEmbedding line 100
def OAI.RationalHitting.Generator.finPencil line 103
lemma OAI.RationalHitting.Generator.finPencil_unit line 107
def OAI.RationalHitting.Generator.onePencil line 116
def OAI.RationalHitting.Generator.conditions line 118
lemma OAI.RationalHitting.Generator.condition_nonzero line 122
lemma OAI.RationalHitting.Generator.condition_degree line 155
lemma OAI.RationalHitting.Generator.integer_grid line 167
lemma OAI.RationalHitting.Generator.specialized_unit line 188
lemma OAI.RationalHitting.Generator.onePencil_unit line 201
theorem OAI.RationalHitting.Generator.output_hits line 216
Source documentation
The finite formula-independent list hits every admissible nonzero formula at a defined and invertible original-tree value.
```
theorem output_hits {n s N e H : ℕ} (hs : 1 ≤ s)
    (hN : 1 ≤ N) (hMN : CyclotomicRing.dimension e = N+2*(n+1)^3*(2*s+1))
    (hM : (2*s+1)*(2*(n+1)^3*(2*s+1)) < CyclotomicRing.dimension e)
    (hH : (s+2)*(3*(2*s+1)*(CyclotomicRing.dimension e)^2) < H) :
    Hits s (output n N e H) := by
…
```
Mentions: OAI.RationalHitting.CyclotomicRing.dimension, OAI.RationalHitting.Hits, OAI.RationalHitting.Generator.output
def OAI.RationalHitting.Parameters.w line 248
Source documentation
The parameters, with M the least power of two strictly above BΔ.
```
def w (n : ℕ) := n+1
```
def OAI.RationalHitting.Parameters.B line 249
def OAI.RationalHitting.Parameters.delta line 250
def OAI.RationalHitting.Parameters.exponent line 251
def OAI.RationalHitting.Parameters.M line 252
def OAI.RationalHitting.Parameters.N line 253
def OAI.RationalHitting.Parameters.H line 254
theorem OAI.RationalHitting.Parameters.threshold_pos line 256
theorem OAI.RationalHitting.Parameters.threshold_lt line 260
theorem OAI.RationalHitting.Parameters.M_le line 263
theorem OAI.RationalHitting.Parameters.M_minimal line 270
theorem OAI.RationalHitting.Parameters.N_pos line 274
theorem OAI.RationalHitting.Parameters.M_eq line 281
theorem OAI.RationalHitting.Parameters.grid_large line 286
theorem OAI.RationalHitting.Parameters.w_bound line 292
theorem OAI.RationalHitting.Parameters.B_bound line 294
theorem OAI.RationalHitting.Parameters.delta_bound line 296
theorem OAI.RationalHitting.Parameters.polynomial_M line 304
theorem OAI.RationalHitting.Parameters.polynomial_H line 312
def OAI.RationalHitting.Generator.list line 331
Source documentation
The list with all parameters fixed by the unary inputs.
```
def list (n s : ℕ) : Output n :=
…
```
Mentions: OAI.RationalHitting.Output
theorem OAI.RationalHitting.Generator.list_hits line 334
theorem OAI.RationalHitting.Generator.list_dimension_bound line 341
theorem OAI.RationalHitting.Generator.list_length_bound line 350

theorem OAI.RationalHitting.Generator.algebraic_generator line 358

Source documentation

The algebraic hitting property and the polynomial list-cardinality bound.

theorem algebraic_generator : ∃ G : (n s : ℕ) → Output n,
    ∀ n s, 1 ≤ n → 1 ≤ s →
      (G n s).dimension ≤ 256*(n+s+1)^10 ∧
      (G n s).tuples.length ≤ 24577^3*(n+s+1)^51 ∧ Hits s (G n s) := by
…

Mentions: OAI.RationalHitting.Output, OAI.RationalHitting.Hits