The core module lean/FrcCore/Keys/Dirac.lean — the substrate from first principles, no Mathlib, no axioms; one of the core's 137 modules (the index); it rests on 15 modules: Nat, Pigeonhole, Shell, Series, Ring, FrameCore, Frame, Parity, Transform, Orbit, Sum, Theme/Quadratic, Theme/Extension, Instances, Theme/Dirac: 19 theorems (0 definitions): 19 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.Parity2import FrcCore.Theme.Dirac34/-!5# FrcCore.Keys.Dirac — the keyed theorems of the dirac theme (ledger migration, task LM19)67One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem8that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration9`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).10-/1112namespace FRC.Ledger1314-- Keys of the dirac theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)15/-- p08009 — 8:B3. The drive is canonical: the drive multiplier is a nonsquare on every shell and the only named residue that is one on every symmetry-complete shell; the classes of $2$, $2^{-1}$, $-2$, $\pi=-2^{-1}$ and $\im$ are fixed by the parity of $\kap$, that of $e$ by no rule; the reframing flip keeps the class. Decided on $\p<2000$. -/16
theorem p08009 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ¬∃ y, y * y = g) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {y : FRC.Shell p}, g * y = (1 : FRC.Shell p) → ¬∃ r, r * r = y) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ((∃ y, y * y = FRC.Shell.Frame.quarterTurn g κ) ↔ κ % (2 : Nat) = (0 : Nat))) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {h : FRC.Shell p}, (2 : FRC.Shell p) * h = (1 : FRC.Shell p) → ((∃ r, r * r = (2 : FRC.Shell p)) ↔ κ % (2 : Nat) = (0 : Nat)) ∧ ((∃ r, r * r = h) ↔ κ % (2 : Nat) = (0 : Nat)) ∧ ((∃ r, r * r = (-2 : FRC.Shell p)) ↔ κ % (2 : Nat) = (0 : Nat)) :=17 And.intro @FRC.Shell.Frame.drive_nonsquare (And.intro @FRC.Shell.Frame.inv_drive_nonsquare (And.intro @FRC.Dirac.quarter_class (@FRC.Dirac.two_class)))18/-- p08013 — 8:B7. Signature lives on $\Fp$: the Euclidean form is hyperbolic and $Q_\nu$ elliptic, with the zero counts of the two classes on every symmetry-complete shell below $60$; over $K$ every element of $\Fp$ is a square and the dichotomy collapses. -/19theorem p08013 : FRC.Dirac.euclidZeros (13 : Nat) = (2353 : Nat) ∧ FRC.Dirac.lorentzZeros (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (2041 : Nat) :=20 @FRC.Dirac.zeros1321/-- p08019 — 8:C5. The finite Cayley transform: the scalar Cayley map is defined on the whole shell, takes values in the norm-one cycle, and bijects the projective line onto it, which has $\p+1$ elements and is the unitary group of one channel. -/22theorem p08019 : FRC.Dirac.normOneCount (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (14 : Nat) ∧ FRC.Dirac.normOneCount (173 : Nat) (2 : FRC.Shell (173 : Nat)) = (174 : Nat) ∧ FRC.Dirac.unitCircleCount (13 : Nat) = (12 : Nat) ∧ FRC.Dirac.unitCircleCount (173 : Nat) = (172 : Nat) :=23 @FRC.Dirac.torus_counts24/-- p08022 — 8:D2. The Clifford relations of the gamma matrices. -/25theorem p08022 : FRC.Dirac.clifford (2 : FRC.Shell (13 : Nat)) (5 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.clifford (2 : FRC.Shell (173 : Nat)) (93 : FRC.Shell (173 : Nat)) = true ∧ FRC.Dirac.clifford (2 : FRC.Shell (1549 : Nat)) (1461 : FRC.Shell (1549 : Nat)) = true :=26 @FRC.Dirac.clifford_values27/-- p08025 — 8:D5. The boost group is the non-split cycle: the image of the extension's units with kernel the scalar line, the boost entries the coordinates of $z/\bar z$, cyclic of order $\p+1$; an order-three boost exists iff $3$ divides $\p+1$ (at $173$, not at $13$). -/28theorem p08025 : (FRC.Dirac.normOneCount (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (14 : Nat) ∧ FRC.Dirac.normOneCount (173 : Nat) (2 : FRC.Shell (173 : Nat)) = (174 : Nat) ∧ FRC.Dirac.unitCircleCount (13 : Nat) = (12 : Nat) ∧ FRC.Dirac.unitCircleCount (173 : Nat) = (172 : Nat)) ∧ FRC.Dirac.hasOrderThree (173 : Nat) (2 : FRC.Shell (173 : Nat)) = true ∧ FRC.Dirac.hasOrderThree (13 : Nat) (2 : FRC.Shell (13 : Nat)) = false :=29 And.intro @FRC.Dirac.torus_counts (@FRC.Dirac.triality_values)30/-- p08026 — 8:D6. Spin conjugation: the lift carries the two temporal gamma matrices to the stated combinations and fixes the other two. -/31theorem p08026 : FRC.Dirac.spinConj (2 : FRC.Shell (13 : Nat)) (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (12 : FRC.Shell (13 : Nat)) (10 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.spinConj (2 : FRC.Shell (173 : Nat)) (93 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat)) (172 : FRC.Shell (173 : Nat)) (170 : FRC.Shell (173 : Nat)) (2 : FRC.Shell (173 : Nat)) = true ∧ FRC.Dirac.spinConj (2 : FRC.Shell (1549 : Nat)) (1461 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat)) (1548 : FRC.Shell (1549 : Nat)) (1546 : FRC.Shell (1549 : Nat)) (2 : FRC.Shell (1549 : Nat)) = true :=32 @FRC.Dirac.spin_conjugation_values33/-- p08029 — 8:D9. The spinor form: under the plain conjugate transpose the gamma matrices carry mixed signs and the $\gamma^0$-twist fails; the odd product $X=\gamma^0\gamma^1\gamma^3$ is Hermitian with square $\nu$ and makes every gamma matrix anti-self-adjoint; the symmetric Dirac operator is self-adjoint and nilpotent for the $X$-form. Decided at $\p=13$, $173$ and $1549$. -/34theorem p08029 : FRC.Dirac.spinorForm (2 : FRC.Shell (13 : Nat)) (5 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.spinorForm (2 : FRC.Shell (173 : Nat)) (93 : FRC.Shell (173 : Nat)) = true ∧ FRC.Dirac.spinorForm (2 : FRC.Shell (1549 : Nat)) (1461 : FRC.Shell (1549 : Nat)) = true :=35 @FRC.Dirac.spinor_form_values36/-- p08040 — 8:F3. The free evolution is the drive: the drive pullback is unitary, the characters are its eigenvectors with the phase $g^{-k}$ per chronon, and every character line is isotropic except the two with eigenvalues $\pm1$, the meeting of the norm-one cycle and the drive cycle. Decided on $\F_{13}$ and $\F_{173}$. -/37theorem p08040 : (∀ {p : Nat} [FRC.Pos p] {g y : FRC.Shell p}, g * y = (1 : FRC.Shell p) → ∀ (j k : Nat), y ^ k * g ^ ((j + (1 : Nat)) * k) = g ^ (j * k)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {y : FRC.Shell p}, g * y = (1 : FRC.Shell p) → y ^ ((2 : Nat) * κ) = (-1 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (k : Nat), ((2 : Nat) * k % (p - (1 : Nat)) ≠ (0 : Nat) → FRC.Shell.sumRange (fun j => g ^ (j * k) * g ^ (j * k)) (p - (1 : Nat)) = (0 : FRC.Shell p)) ∧ ((2 : Nat) * k % (p - (1 : Nat)) = (0 : Nat) → FRC.Shell.sumRange (fun j => g ^ (j * k) * g ^ (j * k)) (p - (1 : Nat)) = (-1 : FRC.Shell p)) :=38 And.intro @FRC.Dirac.drive_eigen (And.intro @FRC.Dirac.exceptional_eigen (@FRC.Dirac.isotropy))39/-- p08041 — 8:F4. Two evolution sectors, one space: the drive's split-phase sector and the Cayley propagators' norm-one sector meet in $\{\pm1\}$ alone; the cycle Laplacian is self-adjoint, its Cayley steps commute with the drive, and the composite is unitary. -/40theorem p08041 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {y : FRC.Shell p}, g * y = (1 : FRC.Shell p) → y.IsPrimitive (p - (1 : Nat)) ∧ ∀ (u : FRC.Shell p), u * u = (1 : FRC.Shell p) → u = (1 : FRC.Shell p) ∨ u = (-1 : FRC.Shell p) :=41 @FRC.Dirac.sector_separation42/-- p08048 — 8:F6. The two spectra: the drive is semisimple with spectrum the drive cycle; the Dirac Cayley step at mass $m$ has the single eigenvalue $\varphi(-m)$ on the third cycle and the mass phases fill it once; the spectra meet in $\{\pm1\}$; the Hamiltonian form has the two eigenvalues $\varphi(\pm\im\nu m)$, a conjugate pair. Decided at $\p=13$ and $173$. -/43theorem p08048 : (∀ {p : Nat} [FRC.Pos p] {g y : FRC.Shell p}, g * y = (1 : FRC.Shell p) → ∀ (j k : Nat), y ^ k * g ^ ((j + (1 : Nat)) * k) = g ^ (j * k)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {y : FRC.Shell p}, g * y = (1 : FRC.Shell p) → y.IsPrimitive (p - (1 : Nat)) ∧ ∀ (u : FRC.Shell p), u * u = (1 : FRC.Shell p) → u = (1 : FRC.Shell p) ∨ u = (-1 : FRC.Shell p)) ∧ FRC.Dirac.normOneCount (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (14 : Nat) ∧ FRC.Dirac.normOneCount (173 : Nat) (2 : FRC.Shell (173 : Nat)) = (174 : Nat) ∧ FRC.Dirac.unitCircleCount (13 : Nat) = (12 : Nat) ∧ FRC.Dirac.unitCircleCount (173 : Nat) = (172 : Nat) :=44 And.intro @FRC.Dirac.drive_eigen (And.intro @FRC.Dirac.sector_separation (@FRC.Dirac.torus_counts))45/-- p08049 — 8:B4. The factorisation of the temporal coefficient: $\nu=g=2^{-1}\cdot(2g)$ on every shell, the class of $2^{-1}$ even iff $\kap$ is even, the class of $2g$ odd iff $\kap$ is even, the product odd always; the reframing flip preserves the parity class and reverses the one-way direction. -/46theorem p08049 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {h : FRC.Shell p}, (2 : FRC.Shell p) * h = (1 : FRC.Shell p) → h * ((2 : FRC.Shell p) * g) = g ∧ ((∃ y, y * y = (2 : FRC.Shell p) * g) ↔ κ % (2 : Nat) = (1 : Nat))) ∧ (171106 : FRC.Shell (2408561 : Nat)) * (171106 : FRC.Shell (2408561 : Nat)) = (1204281 : FRC.Shell (2408561 : Nat)) ∧ (2 : FRC.Shell (2408561 : Nat)) * (1204281 : FRC.Shell (2408561 : Nat)) = (1 : FRC.Shell (2408561 : Nat)) ∧ (1204281 : FRC.Shell (2408561 : Nat)) * (12 : FRC.Shell (2408561 : Nat)) = (6 : FRC.Shell (2408561 : Nat)) :=47 And.intro @FRC.Dirac.nu_factorisation (@FRC.Dirac.carrier_constants)48/-- p08051 — 8:D12. The worked shell $\F_{13}$ with the drive $2$: the boost at $x=y=1$ with $A=10$, $B=2$, the transported gamma matrices, the order $14$ of the boost cycle and no triality element; the named residues $2$, $2^{-1}$, $\im$, $e$, $\pi$ are nonsquares. -/49theorem p08051 : (FRC.Dirac.spinConj (2 : FRC.Shell (13 : Nat)) (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (12 : FRC.Shell (13 : Nat)) (10 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.spinConj (2 : FRC.Shell (173 : Nat)) (93 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat)) (172 : FRC.Shell (173 : Nat)) (170 : FRC.Shell (173 : Nat)) (2 : FRC.Shell (173 : Nat)) = true ∧ FRC.Dirac.spinConj (2 : FRC.Shell (1549 : Nat)) (1461 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat)) (1548 : FRC.Shell (1549 : Nat)) (1546 : FRC.Shell (1549 : Nat)) (2 : FRC.Shell (1549 : Nat)) = true) ∧ (FRC.Dirac.normOneCount (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (14 : Nat) ∧ FRC.Dirac.normOneCount (173 : Nat) (2 : FRC.Shell (173 : Nat)) = (174 : Nat) ∧ FRC.Dirac.unitCircleCount (13 : Nat) = (12 : Nat) ∧ FRC.Dirac.unitCircleCount (173 : Nat) = (172 : Nat)) ∧ (((2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ (5 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (5 : Nat) = (6 : FRC.Shell (13 : Nat)) ∧ ∀ (r : FRC.Shell (13 : Nat)), r * r ≠ (2 : FRC.Shell (13 : Nat)) ∧ r * r ≠ (7 : FRC.Shell (13 : Nat)) ∧ r * r ≠ (5 : FRC.Shell (13 : Nat)) ∧ r * r ≠ (6 : FRC.Shell (13 : Nat))) ∧ ((2 : FRC.Shell (173 : Nat)) * (87 : FRC.Shell (173 : Nat)) = (1 : FRC.Shell (173 : Nat)) ∧ (93 : FRC.Shell (173 : Nat)) * (93 : FRC.Shell (173 : Nat)) = (-1 : FRC.Shell (173 : Nat)) ∧ (2 : FRC.Shell (173 : Nat)) ^ (93 : Nat) = (45 : FRC.Shell (173 : Nat)) ∧ (86 : FRC.Shell (173 : Nat)) = (2 : FRC.Shell (173 : Nat)) * (43 : FRC.Shell (173 : Nat)) ∧ ∀ (r : FRC.Shell (173 : Nat)), r * r ≠ (2 : FRC.Shell (173 : Nat)) ∧ r * r ≠ (87 : FRC.Shell (173 : Nat)) ∧ r * r ≠ (93 : FRC.Shell (173 : Nat)) ∧ r * r ≠ (45 : FRC.Shell (173 : Nat)) ∧ r * r ≠ (86 : FRC.Shell (173 : Nat))) ∧ (-1 : FRC.Shell (13 : Nat)) * (10 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) + (2 : FRC.Shell (13 : Nat)) ∧ (-1 : FRC.Shell (13 : Nat)) * (2 : FRC.Shell (13 : Nat)) = (-2 : FRC.Shell (13 : Nat)) ∧ (-1 : FRC.Shell (173 : Nat)) * (170 : FRC.Shell (173 : Nat)) = (1 : FRC.Shell (173 : Nat)) + (2 : FRC.Shell (173 : Nat)) ∧ (-1 : FRC.Shell (173 : Nat)) * (2 : FRC.Shell (173 : Nat)) = (-2 : FRC.Shell (173 : Nat))) ∧ FRC.Dirac.hasOrderThree (173 : Nat) (2 : FRC.Shell (173 : Nat)) = true ∧ FRC.Dirac.hasOrderThree (13 : Nat) (2 : FRC.Shell (13 : Nat)) = false :=50 And.intro @FRC.Dirac.spin_conjugation_values (And.intro @FRC.Dirac.torus_counts (And.intro @FRC.Dirac.shell173_values (@FRC.Dirac.triality_values)))51/-- p08052 — 8:F2. The latitude identities: the energy index $\kap+1$ is the first rung past the midpoint of the ladder; the shift by $\kap$ is multiplication by $g^{\kap}$ on the meridians and carries the first latitude to the energy latitude; $\kap=-4^{-1}$, so the energy radius is $3\cdot4^{-1}$ and $\pi=2\kap=-2^{-1}$; the unit-norm circle has $\p-1$ points. On $\F_{13}$ and $\F_{173}$. -/52theorem p08052 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → κ + (1 : Nat) ≤ (2 : Nat) * κ) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {q : FRC.Shell p}, (4 : FRC.Shell p) * q = (1 : FRC.Shell p) → (4 : FRC.Shell p) * FRC.Shell.ofNat κ = (-1 : FRC.Shell p) ∧ FRC.Shell.ofNat κ = -q ∧ (1 : FRC.Shell p) + FRC.Shell.ofNat κ = (3 : FRC.Shell p) * q) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {h : FRC.Shell p}, (2 : FRC.Shell p) * h = (1 : FRC.Shell p) → FRC.Shell.ofNat ((2 : Nat) * κ) = -h) ∧ FRC.Dirac.normOneCount (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (14 : Nat) ∧ FRC.Dirac.normOneCount (173 : Nat) (2 : FRC.Shell (173 : Nat)) = (174 : Nat) ∧ FRC.Dirac.unitCircleCount (13 : Nat) = (12 : Nat) ∧ FRC.Dirac.unitCircleCount (173 : Nat) = (172 : Nat) :=53 And.intro @FRC.Dirac.ladder (And.intro @FRC.Dirac.four_kappa (And.intro @FRC.Dirac.terminal_latitude (@FRC.Dirac.torus_counts)))54/-- p08053 — 8:X1. Two cycles for one unit circle: the continuum's single phase group appears on the shell as the drive cycle, carrying the free evolution, and the norm-one cycle, carrying the Cayley phases and the boosts, and the two meet in $\{\pm1\}$. -/55theorem p08053 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {y : FRC.Shell p}, g * y = (1 : FRC.Shell p) → y.IsPrimitive (p - (1 : Nat)) ∧ ∀ (u : FRC.Shell p), u * u = (1 : FRC.Shell p) → u = (1 : FRC.Shell p) ∨ u = (-1 : FRC.Shell p) :=56 @FRC.Dirac.sector_separation57/-- p08054 — 8:X2. The one-way speed is gauge: the temporal coefficient is an odd drive step, registered transport is even, and the reframing flip reverses the one-way direction while preserving the parity class. -/58theorem p08054 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {h : FRC.Shell p}, (2 : FRC.Shell p) * h = (1 : FRC.Shell p) → h * ((2 : FRC.Shell p) * g) = g ∧ ((∃ y, y * y = (2 : FRC.Shell p) * g) ↔ κ % (2 : Nat) = (1 : Nat))) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (m : Nat), (∃ y, y * y = g ^ m) ↔ m % (2 : Nat) = (0 : Nat) :=59 And.intro @FRC.Dirac.nu_factorisation (@FRC.Shell.Frame.parity_iff)60/-- p08056 — 8:X4. The spinor form is forced: the continuum's $\gamma^0$-twist fails because Frobenius fixes the internal quarter-turn, and the arithmetic forces the twist onto the odd product omitting $\gamma^2$. -/61theorem p08056 : FRC.Dirac.spinorForm (2 : FRC.Shell (13 : Nat)) (5 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.spinorForm (2 : FRC.Shell (173 : Nat)) (93 : FRC.Shell (173 : Nat)) = true ∧ FRC.Dirac.spinorForm (2 : FRC.Shell (1549 : Nat)) (1461 : FRC.Shell (1549 : Nat)) = true :=62 @FRC.Dirac.spinor_form_values63/-- p08069 — 8:D16. The explicit transported form: the transported Dirac operator is the Dirac operator of the transported frame with the transported gamma matrices, the spin conjugates of the standard ones. -/64theorem p08069 : FRC.Dirac.spinConj (2 : FRC.Shell (13 : Nat)) (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (12 : FRC.Shell (13 : Nat)) (10 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.spinConj (2 : FRC.Shell (173 : Nat)) (93 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat)) (172 : FRC.Shell (173 : Nat)) (170 : FRC.Shell (173 : Nat)) (2 : FRC.Shell (173 : Nat)) = true ∧ FRC.Dirac.spinConj (2 : FRC.Shell (1549 : Nat)) (1461 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat)) (1548 : FRC.Shell (1549 : Nat)) (1546 : FRC.Shell (1549 : Nat)) (2 : FRC.Shell (1549 : Nat)) = true :=65 @FRC.Dirac.spin_conjugation_values66/-- p08072 — 8:D19. The worked shell $\F_{173}$, the second laboratory Subject, with the drive $2$ and $\im=93$: the boost at $x=y=1$ with $A=170$, $B=2$, the transported gamma matrices, the order $174$ of the boost cycle and its triality element; the named residues are nonsquares. -/67theorem p08072 : (((2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ (5 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (5 : Nat) = (6 : FRC.Shell (13 : Nat)) ∧ ∀ (r : FRC.Shell (13 : Nat)), r * r ≠ (2 : FRC.Shell (13 : Nat)) ∧ r * r ≠ (7 : FRC.Shell (13 : Nat)) ∧ r * r ≠ (5 : FRC.Shell (13 : Nat)) ∧ r * r ≠ (6 : FRC.Shell (13 : Nat))) ∧ ((2 : FRC.Shell (173 : Nat)) * (87 : FRC.Shell (173 : Nat)) = (1 : FRC.Shell (173 : Nat)) ∧ (93 : FRC.Shell (173 : Nat)) * (93 : FRC.Shell (173 : Nat)) = (-1 : FRC.Shell (173 : Nat)) ∧ (2 : FRC.Shell (173 : Nat)) ^ (93 : Nat) = (45 : FRC.Shell (173 : Nat)) ∧ (86 : FRC.Shell (173 : Nat)) = (2 : FRC.Shell (173 : Nat)) * (43 : FRC.Shell (173 : Nat)) ∧ ∀ (r : FRC.Shell (173 : Nat)), r * r ≠ (2 : FRC.Shell (173 : Nat)) ∧ r * r ≠ (87 : FRC.Shell (173 : Nat)) ∧ r * r ≠ (93 : FRC.Shell (173 : Nat)) ∧ r * r ≠ (45 : FRC.Shell (173 : Nat)) ∧ r * r ≠ (86 : FRC.Shell (173 : Nat))) ∧ (-1 : FRC.Shell (13 : Nat)) * (10 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) + (2 : FRC.Shell (13 : Nat)) ∧ (-1 : FRC.Shell (13 : Nat)) * (2 : FRC.Shell (13 : Nat)) = (-2 : FRC.Shell (13 : Nat)) ∧ (-1 : FRC.Shell (173 : Nat)) * (170 : FRC.Shell (173 : Nat)) = (1 : FRC.Shell (173 : Nat)) + (2 : FRC.Shell (173 : Nat)) ∧ (-1 : FRC.Shell (173 : Nat)) * (2 : FRC.Shell (173 : Nat)) = (-2 : FRC.Shell (173 : Nat))) ∧ (FRC.Dirac.normOneCount (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (14 : Nat) ∧ FRC.Dirac.normOneCount (173 : Nat) (2 : FRC.Shell (173 : Nat)) = (174 : Nat) ∧ FRC.Dirac.unitCircleCount (13 : Nat) = (12 : Nat) ∧ FRC.Dirac.unitCircleCount (173 : Nat) = (172 : Nat)) ∧ FRC.Dirac.hasOrderThree (173 : Nat) (2 : FRC.Shell (173 : Nat)) = true ∧ FRC.Dirac.hasOrderThree (13 : Nat) (2 : FRC.Shell (13 : Nat)) = false :=68 And.intro @FRC.Dirac.shell173_values (And.intro @FRC.Dirac.torus_counts (@FRC.Dirac.triality_values))69/-- p08073 — 8:E5. The power map on the phase cycle has image count $(\p-1)/\gcd(\varepsilon,\p-1)$ and loss factor $\gcd(\varepsilon,\p-1)$, every nonempty fibre of that size. -/70theorem p08073 : FRC.Dirac.powerImage (13 : Nat) (1 : Nat) = (12 : Nat) ∧ FRC.Dirac.powerImage (13 : Nat) (2 : Nat) = (6 : Nat) ∧ FRC.Dirac.powerImage (13 : Nat) (3 : Nat) = (4 : Nat) ∧ FRC.Dirac.powerImage (13 : Nat) (4 : Nat) = (3 : Nat) ∧ FRC.Dirac.powerImage (13 : Nat) (6 : Nat) = (2 : Nat) ∧ FRC.Dirac.powerImage (13 : Nat) (12 : Nat) = (1 : Nat) :=71 @FRC.Dirac.power_map1372-- end keys7374end FRC.Ledger75