QuadraticEncoding.lean`

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.LittleFinitistic.QuadraticEncoding.Relations line 12
Source documentation
Coefficients of the finite quadratic relation list, including degrees zero and one.
```
structure Relations (k : Type u) (d t : ℕ) where
…
```
abbrev OAI.LittleFinitistic.QuadraticEncoding.Arrows line 17
abbrev OAI.LittleFinitistic.QuadraticEncoding.Paths line 18
def OAI.LittleFinitistic.QuadraticEncoding.basis line 20
def OAI.LittleFinitistic.QuadraticEncoding.commutation line 22
def OAI.LittleFinitistic.QuadraticEncoding.homogenized line 25
def OAI.LittleFinitistic.QuadraticEncoding.relationSpace line 31
Source documentation
Exactly the span of a'_h s - s' a_h and all homogenized p_j.
```
def relationSpace (P : Relations k d t) : Submodule k (Paths k d) :=
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.Relations, OAI.LittleFinitistic.QuadraticEncoding.Paths
def OAI.LittleFinitistic.QuadraticEncoding.composition line 35
Source documentation
Compose arrows, then quotient only the length-two path space by the specified relations.
```
def composition (P : Relations k d t) :
    Arrows k d →ₗ[k] Arrows k d →ₗ[k] (Paths k d ⧸ relationSpace P) :=
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.Relations, OAI.LittleFinitistic.QuadraticEncoding.Arrows, OAI.LittleFinitistic.QuadraticEncoding.Paths, OAI.LittleFinitistic.QuadraticEncoding.relationSpace
abbrev OAI.LittleFinitistic.QuadraticEncoding.B line 40
Source documentation
The six path-endpoint components of the manuscript's directed encoding.
```
abbrev B (P : Relations k d t) := ThreeVertexAlgebra (composition P)
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.Relations, OAI.LittleFinitistic.ThreeVertexAlgebra, OAI.LittleFinitistic.QuadraticEncoding.composition
theorem OAI.LittleFinitistic.QuadraticEncoding.finiteDimensional line 44
theorem OAI.LittleFinitistic.QuadraticEncoding.globalDimension_le_two line 53
Source documentation
Actual global dimensions of the constructed finite-dimensional encoding.
```
theorem globalDimension_le_two :
    (⨆ N : ModuleCat.{max u v} (B P), projectiveDimension N) ≤ (2 : ℕ) ∧
    (⨆ N : ModuleCat.{max u v} (B P)ᵐᵒᵖ, projectiveDimension N) ≤ (2 : ℕ) :=
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.B
def OAI.LittleFinitistic.QuadraticEncoding.lengthTwo line 59
Source documentation
Includes a length-two residue class as the 0-to-2 component.
```
def lengthTwo : (Paths k d ⧸ relationSpace P) →ₗ[k] B P where
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.Paths, OAI.LittleFinitistic.QuadraticEncoding.relationSpace, OAI.LittleFinitistic.QuadraticEncoding.B
def OAI.LittleFinitistic.QuadraticEncoding.pathMap line 70
theorem OAI.LittleFinitistic.QuadraticEncoding.pathMap_eq_zero_iff line 73
Source documentation
This records that no additional linear length-two relation was introduced.
```
theorem pathMap_eq_zero_iff (z : Paths k d) : pathMap P z = 0 ↔ z ∈ relationSpace P := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.Paths, OAI.LittleFinitistic.QuadraticEncoding.pathMap, OAI.LittleFinitistic.QuadraticEncoding.relationSpace
def OAI.LittleFinitistic.QuadraticEncoding.arrow01 line 81
Source documentation
Arrows s,a_1,...,a_d from vertex 0 to 1; index zero is s.
```
def arrow01 (i : Fin (d + 1)) : B P := (0, 0, 0, basis i, 0, 0)
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.B, OAI.LittleFinitistic.QuadraticEncoding.basis
def OAI.LittleFinitistic.QuadraticEncoding.arrow12 line 83
Source documentation
Arrows s',a'_1,...,a'_d from vertex 1 to 2; index zero is s'.
```
def arrow12 (i : Fin (d + 1)) : B P := (0, 0, 0, 0, basis i, 0)
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.B, OAI.LittleFinitistic.QuadraticEncoding.basis
lemma OAI.LittleFinitistic.QuadraticEncoding.arrow_product line 85
theorem OAI.LittleFinitistic.QuadraticEncoding.commutation_holds line 92
Source documentation
Equation a'_h s = s' a_h, with exactly the manuscript's composition order.
```
theorem commutation_holds (h : Fin d) :
    arrow12 P h.succ * arrow01 P 0 = arrow12 P 0 * arrow01 P h.succ := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.arrow12, OAI.LittleFinitistic.QuadraticEncoding.arrow01
theorem OAI.LittleFinitistic.QuadraticEncoding.homogenized_holds line 98
Source documentation
Every homogenized defining equation holds in the constructed algebra.
```
theorem homogenized_holds (j : Fin t) :
    (∑ h, ∑ l, P.quadratic j h l • (arrow12 P h.succ * arrow01 P l.succ)) +
    (∑ h, P.linear j h • (arrow12 P 0 * arrow01 P h.succ)) +
    P.constant j • (arrow12 P 0 * arrow01 P 0) = 0 := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.arrow12, OAI.LittleFinitistic.QuadraticEncoding.arrow01