lean/SpectreKnot/CompFull.lean
99 lines · 23 declarations, each with its own page · on GitHub ·
Computation 7.3, from the tables alone: the unreduced abstract compositions of §7.1, glued port by port in the Lean kernel. This does not use the reduced walk, the skeletons exported from JavaScript, or the zigzag lemma. compositions_level1_signature states the result as theorems about the glued compositions (via Comp.check_sound).
← SpectreKnot/Compose.leanSpectreKnot/Subdivide.lean →
All 39 files, and the declarations of this one
1/-
2Computation 7.3, from the tables alone: the unreduced abstract compositions of §7.1, glued port by port in the
3Lean kernel. This does not use the reduced walk, the skeletons exported from JavaScript, or the zigzag lemma.
4`compositions_level1_signature` states the result as theorems about the glued compositions (via `Comp.check_sound`).
5-/
6import SpectreKnot.Compose
8namespace SpectreKnot.Compose
10/-- The nine kinds. -/
13/-! The kernel's runs, one composition per theorem (one run needs about 1.5 GB). -/
15/-- Γ, `ω = +1`: the level-1 composition passes `check`. -/
16theorem check_Gamma_plus : (Comp.ofPattern .Gamma (letterLen 1) (dOff 1) true).check true = true := by decide +kernel
17/-- Γ, `ω = −1`: the level-1 composition passes `check`. -/
18theorem check_Gamma_minus : (Comp.ofPattern .Gamma (letterLen 1) (dOff 1) false).check false = true := by decide +kernel
19/-- Δ, `ω = +1`: the level-1 composition passes `check`. -/
20theorem check_Delta_plus : (Comp.ofPattern .Delta (letterLen 1) (dOff 1) true).check true = true := by decide +kernel
21/-- Δ, `ω = −1`: the level-1 composition passes `check`. -/
22theorem check_Delta_minus : (Comp.ofPattern .Delta (letterLen 1) (dOff 1) false).check false = true := by decide +kernel
23/-- Θ, `ω = +1`: the level-1 composition passes `check`. -/
24theorem check_Theta_plus : (Comp.ofPattern .Theta (letterLen 1) (dOff 1) true).check true = true := by decide +kernel
25/-- Θ, `ω = −1`: the level-1 composition passes `check`. -/
26theorem check_Theta_minus : (Comp.ofPattern .Theta (letterLen 1) (dOff 1) false).check false = true := by decide +kernel
27/-- Λ, `ω = +1`: the level-1 composition passes `check`. -/
28theorem check_Lambda_plus : (Comp.ofPattern .Lambda (letterLen 1) (dOff 1) true).check true = true := by decide +kernel
29/-- Λ, `ω = −1`: the level-1 composition passes `check`. -/
30theorem check_Lambda_minus : (Comp.ofPattern .Lambda (letterLen 1) (dOff 1) false).check false = true := by
31 decide +kernel
32/-- Ξ, `ω = +1`: the level-1 composition passes `check`. -/
33theorem check_Xi_plus : (Comp.ofPattern .Xi (letterLen 1) (dOff 1) true).check true = true := by decide +kernel
34/-- Ξ, `ω = −1`: the level-1 composition passes `check`. -/
35theorem check_Xi_minus : (Comp.ofPattern .Xi (letterLen 1) (dOff 1) false).check false = true := by decide +kernel
36/-- Π, `ω = +1`: the level-1 composition passes `check`. -/
37theorem check_Pi_plus : (Comp.ofPattern .Pi (letterLen 1) (dOff 1) true).check true = true := by decide +kernel
38/-- Π, `ω = −1`: the level-1 composition passes `check`. -/
39theorem check_Pi_minus : (Comp.ofPattern .Pi (letterLen 1) (dOff 1) false).check false = true := by decide +kernel
40/-- Σ, `ω = +1`: the level-1 composition passes `check`. -/
41theorem check_Sigma_plus : (Comp.ofPattern .Sigma (letterLen 1) (dOff 1) true).check true = true := by decide +kernel
42/-- Σ, `ω = −1`: the level-1 composition passes `check`. -/
43theorem check_Sigma_minus : (Comp.ofPattern .Sigma (letterLen 1) (dOff 1) false).check false = true := by decide +kernel
44/-- Φ, `ω = +1`: the level-1 composition passes `check`. -/
45theorem check_Phi_plus : (Comp.ofPattern .Phi (letterLen 1) (dOff 1) true).check true = true := by decide +kernel
46/-- Φ, `ω = −1`: the level-1 composition passes `check`. -/
47theorem check_Phi_minus : (Comp.ofPattern .Phi (letterLen 1) (dOff 1) false).check false = true := by decide +kernel
48/-- Ψ, `ω = +1`: the level-1 composition passes `check`. -/
49theorem check_Psi_plus : (Comp.ofPattern .Psi (letterLen 1) (dOff 1) true).check true = true := by decide +kernel
50/-- Ψ, `ω = −1`: the level-1 composition passes `check`. -/
51theorem check_Psi_minus : (Comp.ofPattern .Psi (letterLen 1) (dOff 1) false).check false = true := by decide +kernel
53/-- **Computation 7.3** (the kernel's runs, collected). -/
54theorem compositions_level1 : ∀ (T : Kind) (ω : Bool), (Comp.ofPattern T (letterLen 1) (dOff 1) ω).check ω = true
55 | .Gamma, true => check_Gamma_plus
56 | .Gamma, false => check_Gamma_minus
57 | .Delta, true => check_Delta_plus
58 | .Delta, false => check_Delta_minus
59 | .Theta, true => check_Theta_plus
60 | .Theta, false => check_Theta_minus
61 | .Lambda, true => check_Lambda_plus
62 | .Lambda, false => check_Lambda_minus
63 | .Xi, true => check_Xi_plus
64 | .Xi, false => check_Xi_minus
65 | .Pi, true => check_Pi_plus
66 | .Pi, false => check_Pi_minus
67 | .Sigma, true => check_Sigma_plus
68 | .Sigma, false => check_Sigma_minus
69 | .Phi, true => check_Phi_plus
70 | .Phi, false => check_Phi_minus
71 | .Psi, true => check_Psi_plus
72 | .Psi, false => check_Psi_minus
74/-- **Computation 7.3**, as theorems. For every kind `T` and both signs `ω`, in the composition of §7.1 with
75the level-1 lengths `(ℓ₁, d₁)`, its children carrying the signature: the gluing is well formed; the walk from every
76port ends on the parent's rim (no closed strand); every parent rim vertex is a hook except the Γ child's corners `A`
77and `B`; these are adjacent in the right order; and they carry the crossover. -/
78theorem compositions_level1_signature (T : Kind) (ω : Bool) :
79 let C := Comp.ofPattern T (letterLen 1) (dOff 1) ω
80 let G := C.toGluing
81 let n := C.rimVertexPorts.length
82 G.WF ∧
83 (∀ x, G.Valid x → ∃ r, G.FullReach x r) ∧
84 (∀ t, t < n → t ≠ C.tA → t ≠ C.tB → G.FullReach (C.vtx t).1 (C.vtx t).2) ∧
85 C.tA < n ∧ C.tB < n ∧ C.tB = (if ω then (C.tA + 1) % n else (C.tA + n - 1) % n) ∧
86 G.FullReach (C.vtx C.tA).2 (C.vtx C.tB).2 ∧ G.FullReach (C.vtx C.tA).1 (C.vtx C.tB).1 := by
87 exact Comp.check_sound _ (compositions_level1 T ω)
89/-- For the negative control: give child `c` a crossover at two non-adjacent corners (`B = A + 2`). -/
90def Comp.spreadCorners (C : Comp) (c : Nat) : Comp :=
91 { C with kids := C.kids.modify c fun k => { k with B := (k.A + 2) % k.E } }
93/-- Negative control: if one child's crossover corners are not adjacent (for the first child and for the Γ child of a
94Δ), the parent fails the check. -/
95theorem negative_control :
96 ([0, 7].all fun c => !((Comp.ofPattern .Delta (letterLen 1) (dOff 1) true).spreadCorners c).check true) = true := by
97 decide +kernel
99end SpectreKnot.Compose