The core module lean/FrcCore/Theme/Cells.lean — the substrate from first principles, no Mathlib, no axioms; one of the core's 137 modules (the index); it rests on 13 modules: Nat, Pigeonhole, Shell, Series, FrameCore, Frame, Parity, Transform, Orbit, Sum, Poly, Instances, Theme/Orbital: 4 theorems (20 definitions): 4 with no axioms, 0 at tier 1 (propext, Quot.sound), 0 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (green, the core; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import FrcCore.Theme.Orbital23/-!4# FrcCore.Theme.Cells — the orbital shell and its spherical completion, coded and decided (the geometry theme)56Moved here from the paper module `FrcCore/Complex.lean` on 6 November 2026, every name unchanged.78The completion of the orbital shell `S_p` (Def. 3.1 of 2-geometry) as a finite cell complex on vertex codes:9`N = 0`, the interior vertices `(a, m)` for `1 ≤ a ≤ π − 1`, `m < n`, and `S`; the faces as cyclic vertex lists10(north triangles, quadrilaterals, south triangles); the edges as the faces' sides. `closed p` checks that every11edge lies in exactly two faces and that every vertex link is a single cycle (2:C3, the exhaustive incidence of12the ledger); `cellular p u` checks whether the reindexing `ρ_u` carries faces to faces (2:B4); `poleExchange`13checks the meridian reversal on the completion. Everything is a computation the kernel evaluates by `decide`.14No axioms.15-/1617namespace FRC18namespace Complex1920/-- The vertex code of `(a, m)` on the shell with `n` phases: `1 + (a − 1)·n + m`. -/21
def vtx (n a m : Nat) : Nat := 1 + (a - 1) * n + m % n2223/-- The south pole: the vertex after the last interior latitude `a = π − 1`. -/24def south (n pi : Nat) : Nat := 1 + (pi - 1) * n2526/-- The faces of the completion, as vertex lists. -/27def faces (n pi : Nat) : List (List Nat) :=28 let north := (List.range n).map fun m => [0, vtx n 1 m, vtx n 1 (m + 1)]29 let quads := ((List.range (pi - 2)).map fun a' => (List.range n).map fun m =>30 [vtx n (a' + 1) m, vtx n (a' + 2) m, vtx n (a' + 2) (m + 1), vtx n (a' + 1) (m + 1)]).foldr (· ++ ·) []31 let souths := (List.range n).map fun m => [vtx n (pi - 1) m, south n pi, vtx n (pi - 1) (m + 1)]32 north ++ quads ++ souths3334/-- The sides of a face, as unordered pairs `(min, max)`. -/35def sides : List Nat → List (Nat × Nat)36 | [] => []37 | f@(v :: _) =>38 let rec go : List Nat → List (Nat × Nat)39 | [] => []40 | [w] => [(min w v, max w v)]41 | w :: (w' :: rest) => (min w w', max w w') :: go (w' :: rest)42 go f4344def vertexCount (n pi : Nat) : Nat := south n pi + 14546/-- A face with its sides computed once: `(vertices, sides)`. -/47abbrev Face := List Nat × List (Nat × Nat)4849def withSides (fs : List (List Nat)) : List Face := fs.map fun f => (f, sides f)5051/-- Two faces are adjacent around `v` when they share a side through `v`. -/52def adjacentAt (v : Nat) (f f' : Face) : Bool :=53 f.2.any fun s => (s.1 == v || s.2 == v) && f'.2.contains s5455/-- The neighbours of `cur` around `v` other than `prev` (and `cur` itself). -/56def nextFaces (v : Nat) (L : List Face) (prev cur : Face) : List Face :=57 L.filter fun f' => !(f'.1 == cur.1) && !(f'.1 == prev.1) && adjacentAt v cur f'5859/-- Walk the link from `f0` along `cur`, never turning back, for `fuel` steps; the number of steps taken until60`f0` is reached again (`fuel` if never). -/61def walk (v : Nat) (L : List Face) (f0 : Face) : Nat → Face → Face → Nat → Nat62 | 0, _, _, k => k63 | fuel + 1, prev, cur, k =>64 match nextFaces v L prev cur with65 | f' :: [] => if f'.1 == f0.1 then k + 1 else walk v L f0 fuel cur f' (k + 1)66 | [] => fuel + k + 167 | _ :: _ :: _ => fuel + k + 16869/-- The link of `v` is a single cycle: every face around `v` has exactly two neighbours there, and the walk from70the first face returns to it after exactly `|L|` steps. -/71def linkIsCycle (fs : List Face) (v : Nat) : Bool :=72 let L := fs.filter fun f => f.1.contains v73 match L with74 | [] => false75 | f0 :: _ =>76 L.all (fun f => (L.filter (fun f' => !(f'.1 == f.1) && adjacentAt v f f')).length == 2) &&77 (match nextFaces v L f0 f0 with78 | f1 :: _ => walk v L f0 L.length f0 f1 1 == L.length79 | [] => false)8081/-- The number of occurrences of `s` in `E`. -/82def count (s : Nat × Nat) : List (Nat × Nat) → Nat83 | [] => 084 | e :: E => (if e == s then 1 else 0) + count s E8586/-- Every side of every face lies in exactly two faces: the sides are bucketed by their smaller vertex and each87side occurs exactly twice in its bucket. -/88def edgesInTwoFaces (fs : List (List Nat)) : Bool :=89 let E := (withSides fs).foldr (fun f acc => f.2 ++ acc) []90 let V := fs.foldr (fun f acc => f.foldr (fun w acc' => if acc'.contains w then acc' else w :: acc') acc) []91 V.all fun v =>92 let B := E.filter fun s => s.1 == v93 B.all fun s => count s B == 29495/-- 2:C3, the exhaustive incidence: the completion is a closed surface. -/96def closed (p : Nat) : Bool :=97 let n := p - 198 let pi := n / 299 let fs := faces n pi100 edgesInTwoFaces fs && (List.range (vertexCount n pi)).all fun v => linkIsCycle (withSides fs) v101102/-- The reindexing `ρ_u` on vertex codes: `(a, m) ↦ (a, u·m mod n)`, the poles fixed. -/103def rhoV (n pi u : Nat) (v : Nat) : Nat :=104 if v == 0 then 0 else if v == south n pi then v else105 let a := (v - 1) / n + 1106 let m := (v - 1) % n107 vtx n a (u * m)108109/-- The meridian reversal on the completion: `N ↔ S`, `(a, m) ↦ (π − a, m)`. -/110def sigmaV (n pi : Nat) (v : Nat) : Nat :=111 if v == 0 then south n pi else if v == south n pi then 0 else112 let a := (v - 1) / n + 1113 let m := (v - 1) % n114 vtx n (pi - a) m115116/-- A vertex map is cellular when it carries every face onto a face (as vertex sets). -/117def cellularMap (fs : List (List Nat)) (φ : Nat → Nat) : Bool :=118 fs.all fun f => fs.any fun f' => (f.map φ).all (fun w => f'.contains w) && f'.all (fun w => (f.map φ).contains w)119120/-- 2:B4 — whether `ρ_u` is a cellular automorphism of the completion. -/121def cellular (p u : Nat) : Bool :=122 let n := p - 1123 let pi := n / 2124 cellularMap (faces n pi) (rhoV n pi u)125126/-- 2:B4 — whether the pole exchange is cellular on the completion. -/127def poleExchange (p : Nat) : Bool :=128 let n := p - 1129 let pi := n / 2130 cellularMap (faces n pi) (sigmaV n pi)131132/-- 2:C2 [value] — the counts on `𝔽₁₃`: `62` vertices, `72` faces of the completion. -/133
theorem counts13 : vertexCount 12 6 = 62 ∧ (faces 12 6).length = 72 := by decide +kernel134135/-- 2:C3 [value] — the completion is a closed surface on `𝔽₁₃` (62 vertices, 72 faces). -/136theorem closed13 : closed 13 = true := by decide +kernel137138139/-- The orbital shell before the collapse: the terminal latitude `a = π` kept, so the last ring of quadrilaterals140ends on it and nothing closes over it. -/141def facesOpen (n pi : Nat) : List (List Nat) :=142 let north := (List.range n).map fun m => [0, vtx n 1 m, vtx n 1 (m + 1)]143 let quads := ((List.range (pi - 1)).map fun a' => (List.range n).map fun m =>144 [vtx n (a' + 1) m, vtx n (a' + 2) m, vtx n (a' + 2) (m + 1), vtx n (a' + 1) (m + 1)]).foldr (· ++ ·) []145 north ++ quads146147/-- 2:C3, 2:B4 [value] — the shell itself is not closed (its terminal latitude is a boundary: those sides lie in148one face only), so the meridian reversal has nothing to act on before the collapse. -/149theorem open13 : edgesInTwoFaces (facesOpen 12 6) = false ∧ (facesOpen 12 6).length = 72 := by decide +kernel150151/-- 2:B4, 2:C4 [value] — on `𝔽₁₃` (`n = 12`) the reindexing `ρ_u` is cellular exactly for `u ∈ {1, 11}` among the152units `{1, 5, 7, 11}`, and the pole exchange is cellular on the completion. -/153theorem census13 :154 cellular 13 1 = true ∧ cellular 13 5 = false ∧ cellular 13 7 = false ∧ cellular 13 11 = true ∧155 poleExchange 13 = true := by decide +kernel156157end Complex158end FRC159