Complex.lean — FrcCore

1import FrcCore.Geometry23/-!4# FrcCore.Complex — the orbital shell and its spherical completion, coded and decided56The completion of the orbital shell `S_p` (Def. 3.1 of 2-geometry) as a finite cell complex on vertex codes:7`N = 0`, the interior vertices `(a, m)` for `1 ≤ a ≤ π − 1`, `m < n`, and `S`; the faces as cyclic vertex lists8(north triangles, quadrilaterals, south triangles); the edges as the faces' sides. `closed p` checks that every9edge lies in exactly two faces and that every vertex link is a single cycle (2:C3, the exhaustive incidence of10the ledger); `cellular p u` checks whether the reindexing `ρ_u` carries faces to faces (2:B4); `poleExchange`11checks the meridian reversal on the completion. Everything is a computation the kernel evaluates by `decide`.12No axioms.13-/1415namespace FRC16namespace Complex1718/-- The vertex code of `(a, m)` on the shell with `n` phases: `1 + (a − 1)·n + m`. -/19def vtx (n a m : Nat) : Nat := 1 + (a - 1) * n + m % n2021/-- The south pole: the vertex after the last interior latitude `a = π − 1`. -/22def south (n pi : Nat) : Nat := 1 + (pi - 1) * n2324/-- The faces of the completion, as vertex lists. -/25def faces (n pi : Nat) : List (List Nat) :=26  let north := (List.range n).map fun m => [0, vtx n 1 m, vtx n 1 (m + 1)]27  let quads := ((List.range (pi - 2)).map fun a' => (List.range n).map fun m =>28      [vtx n (a' + 1) m, vtx n (a' + 2) m, vtx n (a' + 2) (m + 1), vtx n (a' + 1) (m + 1)]).foldr (· ++ ·) []29  let souths := (List.range n).map fun m => [vtx n (pi - 1) m, south n pi, vtx n (pi - 1) (m + 1)]30  north ++ quads ++ souths3132/-- The sides of a face, as unordered pairs `(min, max)`. -/33def sides : List Nat → List (Nat × Nat)34  | [] => []35  | f@(v :: _) =>36    let rec go : List Nat → List (Nat × Nat)37      | [] => []38      | [w] => [(min w v, max w v)]39      | w :: (w' :: rest) => (min w w', max w w') :: go (w' :: rest)40    go f4142def vertexCount (n pi : Nat) : Nat := south n pi + 14344/-- A face with its sides computed once: `(vertices, sides)`. -/45abbrev Face := List Nat × List (Nat × Nat)4647def withSides (fs : List (List Nat)) : List Face := fs.map fun f => (f, sides f)4849/-- Two faces are adjacent around `v` when they share a side through `v`. -/50def adjacentAt (v : Nat) (f f' : Face) : Bool :=51  f.2.any fun s => (s.1 == v || s.2 == v) && f'.2.contains s5253/-- The neighbours of `cur` around `v` other than `prev` (and `cur` itself). -/54def nextFaces (v : Nat) (L : List Face) (prev cur : Face) : List Face :=55  L.filter fun f' => !(f'.1 == cur.1) && !(f'.1 == prev.1) && adjacentAt v cur f'5657/-- Walk the link from `f0` along `cur`, never turning back, for `fuel` steps; the number of steps taken until58`f0` is reached again (`fuel` if never). -/59def walk (v : Nat) (L : List Face) (f0 : Face) : Nat → Face → Face → Nat → Nat60  | 0, _, _, k => k61  | fuel + 1, prev, cur, k =>62    match nextFaces v L prev cur with63    | f' :: [] => if f'.1 == f0.1 then k + 1 else walk v L f0 fuel cur f' (k + 1)64    | [] => fuel + k + 165    | _ :: _ :: _ => fuel + k + 16667/-- The link of `v` is a single cycle: every face around `v` has exactly two neighbours there, and the walk from68the first face returns to it after exactly `|L|` steps. -/69def linkIsCycle (fs : List Face) (v : Nat) : Bool :=70  let L := fs.filter fun f => f.1.contains v71  match L with72  | [] => false73  | f0 :: _ =>74    L.all (fun f => (L.filter (fun f' => !(f'.1 == f.1) && adjacentAt v f f')).length == 2) &&75    (match nextFaces v L f0 f0 with76     | f1 :: _ => walk v L f0 L.length f0 f1 1 == L.length77     | [] => false)7879/-- The number of occurrences of `s` in `E`. -/80def count (s : Nat × Nat) : List (Nat × Nat) → Nat81  | [] => 082  | e :: E => (if e == s then 1 else 0) + count s E8384/-- Every side of every face lies in exactly two faces: the sides are bucketed by their smaller vertex and each85side occurs exactly twice in its bucket. -/86def edgesInTwoFaces (fs : List (List Nat)) : Bool :=87  let E := (withSides fs).foldr (fun f acc => f.2 ++ acc) []88  let V := fs.foldr (fun f acc => f.foldr (fun w acc' => if acc'.contains w then acc' else w :: acc') acc) []89  V.all fun v =>90    let B := E.filter fun s => s.1 == v91    B.all fun s => count s B == 29293/-- 2:C3, the exhaustive incidence: the completion is a closed surface. -/94def closed (p : Nat) : Bool :=95  let n := p - 196  let pi := n / 297  let fs := faces n pi98  edgesInTwoFaces fs && (List.range (vertexCount n pi)).all fun v => linkIsCycle (withSides fs) v99100/-- The reindexing `ρ_u` on vertex codes: `(a, m) ↦ (a, u·m mod n)`, the poles fixed. -/101def rhoV (n pi u : Nat) (v : Nat) : Nat :=102  if v == 0 then 0 else if v == south n pi then v else103    let a := (v - 1) / n + 1104    let m := (v - 1) % n105    vtx n a (u * m)106107/-- The meridian reversal on the completion: `N ↔ S`, `(a, m) ↦ (π − a, m)`. -/108def sigmaV (n pi : Nat) (v : Nat) : Nat :=109  if v == 0 then south n pi else if v == south n pi then 0 else110    let a := (v - 1) / n + 1111    let m := (v - 1) % n112    vtx n (pi - a) m113114/-- A vertex map is cellular when it carries every face onto a face (as vertex sets). -/115def cellularMap (fs : List (List Nat)) (φ : Nat → Nat) : Bool :=116  fs.all fun f => fs.any fun f' => (f.map φ).all (fun w => f'.contains w) && f'.all (fun w => (f.map φ).contains w)117118/-- 2:B4 — whether `ρ_u` is a cellular automorphism of the completion. -/119def cellular (p u : Nat) : Bool :=120  let n := p - 1121  let pi := n / 2122  cellularMap (faces n pi) (rhoV n pi u)123124/-- 2:B4 — whether the pole exchange is cellular on the completion. -/125def poleExchange (p : Nat) : Bool :=126  let n := p - 1127  let pi := n / 2128  cellularMap (faces n pi) (sigmaV n pi)129130/-- 2:C2 [value] — the counts on `𝔽₁₃`: `62` vertices, `72` faces of the completion. -/131theorem counts13 : vertexCount 12 6 = 62 ∧ (faces 12 6).length = 72 := by decide +kernel132133/-- 2:C3 [value] — the completion is a closed surface on `𝔽₅`, by exhaustive incidence. -/134theorem closed5 : closed 5 = true := by decide +kernel135/-- 2:C3 [value] — the completion is a closed surface on `𝔽₁₃` (62 vertices, 72 faces). -/136theorem closed13 : closed 13 = true := by decide +kernel137/-- 2:C3 [value] — the completion is a closed surface on `𝔽₁₇` (114 vertices, 128 faces); the kernel decides138it in a few seconds. -/139theorem closed17 : closed 17 = true := by decide +kernel140141142/-- The orbital shell before the collapse: the terminal latitude `a = π` kept, so the last ring of quadrilaterals143ends on it and nothing closes over it. -/144def facesOpen (n pi : Nat) : List (List Nat) :=145  let north := (List.range n).map fun m => [0, vtx n 1 m, vtx n 1 (m + 1)]146  let quads := ((List.range (pi - 1)).map fun a' => (List.range n).map fun m =>147      [vtx n (a' + 1) m, vtx n (a' + 2) m, vtx n (a' + 2) (m + 1), vtx n (a' + 1) (m + 1)]).foldr (· ++ ·) []148  north ++ quads149150/-- 2:C3, 2:B4 [value] — the shell itself is not closed (its terminal latitude is a boundary: those sides lie in151one face only), so the meridian reversal has nothing to act on before the collapse. -/152theorem open13 : edgesInTwoFaces (facesOpen 12 6) = false ∧ (facesOpen 12 6).length = 72 := by decide +kernel153154/-- 2:B4, 2:C4 [value] — on `𝔽₁₃` (`n = 12`) the reindexing `ρ_u` is cellular exactly for `u ∈ {1, 11}` among the155units `{1, 5, 7, 11}`, and the pole exchange is cellular on the completion. -/156theorem census13 :157    cellular 13 1 = true ∧ cellular 13 5 = false ∧ cellular 13 7 = false ∧ cellular 13 11 = true ∧158    poleExchange 13 = true := by decide +kernel159160end Complex161end FRC162163namespace FRC.Geometry164-- Ledger predicates of 2-geometry (generated by make_predicates.py from docs/2-geometry/2-geometry-ledger.json; edit the ledger, not this section)165/-- 2:B4 (p02008) — Cellular automorphisms of the index grid: $m\mapsto\pm m+c$, the dihedral group of the phase cycle; on the completion also meridian reversal $a\mapsto\pi-a$, exchanging the poles. The reindexing $\rho_{u}\colon m\mapsto um$ preserves latitude adjacency only for $u\equiv\pm1\pmod{\p-1}$; $\sigma$ is not a map of $\Sp$ ($\north$ one vertex, $L_{\pi}$ has $\p-1$); decided on $\p\le29$. -/166theorem p02008 : (∀ (n u : Nat), (3 : Nat) ≤ n → ((∀ (m : Nat), m < n → FRC.Geometry.Adj n (FRC.Geometry.rho n u m) (FRC.Geometry.rho n u ((m + (1 : Nat)) % n))) ↔ u % n = (1 : Nat) ∨ u % n = n - (1 : Nat))) ∧ FRC.Complex.cellular (13 : Nat) (1 : Nat) = true ∧ FRC.Complex.cellular (13 : Nat) (5 : Nat) = false ∧ FRC.Complex.cellular (13 : Nat) (7 : Nat) = false ∧ FRC.Complex.cellular (13 : Nat) (11 : Nat) = true ∧ FRC.Complex.poleExchange (13 : Nat) = true :=167  And.intro @FRC.Geometry.rho_adj_iff (@FRC.Complex.census13)168/-- 2:C2 (p02010) — Counts: $|V|=\pi(\p-1)+1$, $|E|=2\pi(\p-1)$, $|F|=\pi(\p-1)$, $\chi(\Sp)=1$; the completion has $(\pi-1)(\p-1)+2$ vertices, $(2\pi-1)(\p-1)$ edges, $\pi(\p-1)$ faces, $\chi=2$ (Rem.~\ref{rem:cell-counts}). -/169theorem p02010 : (∀ (m n : Nat), (m + (1 : Nat)) * n + (1 : Nat) + (m + (1 : Nat)) * n = (2 : Nat) * ((m + (1 : Nat)) * n) + (1 : Nat) ∧ m * n + (2 : Nat) + (m + (1 : Nat)) * n = ((2 : Nat) * m + (1 : Nat)) * n + (2 : Nat)) ∧ FRC.Complex.vertexCount (12 : Nat) (6 : Nat) = (62 : Nat) ∧ (FRC.Complex.faces (12 : Nat) (6 : Nat)).length = (72 : Nat) :=170  And.intro @FRC.Geometry.euler_characteristic (@FRC.Complex.counts13)171/-- 2:C3 (p02011) — Canonical spherical completion: collapsing $L_{\pi}$ to $\south$ gives a closed orientable surface --- every edge in two faces, every vertex link a cycle --- with $\chi=2$, hence $S^{2}$ (A3), on every shell (Thm.~\ref{thm:combinatorial-sphere}; decided on $\p\in\{5,13,17,29\}$ by exhaustive incidence). -/172theorem p02011 : FRC.Complex.closed (5 : Nat) = true ∧ FRC.Complex.closed (13 : Nat) = true ∧ FRC.Complex.closed (17 : Nat) = true ∧ FRC.Complex.edgesInTwoFaces (FRC.Complex.facesOpen (12 : Nat) (6 : Nat)) = false ∧ (FRC.Complex.facesOpen (12 : Nat) (6 : Nat)).length = (72 : Nat) :=173  And.intro @FRC.Complex.closed5 (And.intro @FRC.Complex.closed13 (And.intro @FRC.Complex.closed17 (@FRC.Complex.open13)))174/-- 2:C4 (p02012) — Frame covariance: $\Sp$ is one complex for every generator --- the index grid $I_{\p}\times\Phi_{\p}$ with its step relations; the frame $\gen'=\gen^{u}$ moves the field labels, $a\gen^{m}\mapsto a\gen^{um}$, by the automorphism $\rho_{u}$ of $\Phi_{\p}$, not the cells. The map $\varphi_{u}$ of Prop.~\ref{prop:shell-covariance} is cellular only for $u\equiv\pm1$. -/175theorem p02012 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (u : Nat) (a : FRC.Shell p) (m : Nat), FRC.Geometry.label (g ^ u) a m = FRC.Geometry.label g a (FRC.Geometry.rho (p - (1 : Nat)) u m)) ∧ FRC.Complex.cellular (13 : Nat) (1 : Nat) = true ∧ FRC.Complex.cellular (13 : Nat) (5 : Nat) = false ∧ FRC.Complex.cellular (13 : Nat) (7 : Nat) = false ∧ FRC.Complex.cellular (13 : Nat) (11 : Nat) = true ∧ FRC.Complex.poleExchange (13 : Nat) = true :=176  And.intro @FRC.Geometry.label_covariance (@FRC.Complex.census13)177-- end ledger predicates178end FRC.Geometry179