The core module lean/FrcCore/Keys/Operator.lean — the substrate from first principles, no Mathlib, no axioms; one of the core's 137 modules (the index); it rests on 27 modules: Nat, Pigeonhole, Shell, Series, Cycle, Ring, FrameCore, Frame, Parity, Transform, Orbit, Sum, Theme/Quadratic, Theme/Extension, Poly, Instances, Theme/Dirac, Theme/Packed, Theme/Plane, Theme/Hermitian, Theme/Operator, Theme/Unipotent, Theme/Spinor, Theme/Loss, Theme/Det, Theme/Elim, Theme/Cayley: 28 theorems (0 definitions): 28 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.Extension2import FrcCore.Theme.Dirac3import FrcCore.Theme.Plane4import FrcCore.Theme.Hermitian5import FrcCore.Theme.Operator6import FrcCore.Theme.Unipotent7import FrcCore.Theme.Spinor8import FrcCore.Theme.Loss9import FrcCore.Theme.Cayley1011/-!12# FrcCore.Keys.Operator — the keyed theorems of the operator theme (ledger migration, task LM19)1314One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem15that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration16`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).17-/1819namespace FRC.Ledger2021-- Keys of the operator theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)22/-- p08008 — 8:B2. The class is the datum: the nonsquares form one square class, and the Lorentzian form depends on its coefficient through that class alone. -/23
theorem p08008 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {a b : FRC.Shell p}, a ≠ (0 : FRC.Shell p) → b ≠ (0 : FRC.Shell p) → ¬FRC.Shell.Frame.IsSquare a → ¬FRC.Shell.Frame.IsSquare b → FRC.Shell.Frame.IsSquare (a * b)) ∧ ∀ {p : Nat} [FRC.Pos p] (ν m x₀ x₁ x₂ x₃ : FRC.Shell p), -(m * m * ν) * (x₀ * x₀) + x₁ * x₁ + x₂ * x₂ + x₃ * x₃ = -ν * (m * x₀ * (m * x₀)) + x₁ * x₁ + x₂ * x₂ + x₃ * x₃ :=24 And.intro @FRC.Dirac.Plane.class_datum (@FRC.Dirac.Plane.form_class)25/-- p08016 — 8:C2. The form is Hermitian and nondegenerate. -/26theorem p08016 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (ψ φ : FRC.Dirac.Hermitian.Fld p ν), FRC.Extension.Ext.conj (FRC.Dirac.Hermitian.herm ψ φ) = FRC.Dirac.Hermitian.herm φ ψ) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (ψ : FRC.Dirac.Hermitian.Fld p ν), (∀ (φ : FRC.Dirac.Hermitian.Fld p ν), FRC.Dirac.Hermitian.herm ψ φ = (0 : FRC.Dirac.Ext p ν)) → ∀ (x : Nat), x < p → ψ x = (0 : FRC.Dirac.Ext p ν) :=27 And.intro @FRC.Dirac.Hermitian.herm_star (@FRC.Dirac.Hermitian.herm_nondegenerate)28set_option linter.defProp false in29/-- p08018 — 8:C4. Exact Hermitian preservation: for a self-adjoint Hamiltonian and an admissible parameter the Cayley step is unitary. -/30def p08018 := And.intro @FRC.Dirac.Operator.cayley_unitary (And.intro @FRC.Dirac.Spinor.MatE.adjoint_dagger (And.intro @FRC.Dirac.Spinor.cayley_values173 (And.intro @FRC.Dirac.Spinor.cayley_nilpotent1549 (And.intro @FRC.Dirac.Spinor.cayley_step1549 (@FRC.Dirac.Spinor.cayley_unitary1549)))))31/-- p08020 — 8:C6. The $\F_{13}$ Schr\"odinger example: the kinetic Hamiltonian is nilpotent, every trace-zero parameter is admissible, and every nonzero parameter gives a unitary step of order $13$. -/32theorem p08020 : (FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (1 : FRC.Shell (13 : Nat)) } = true ∧ FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = true ∧ { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } * { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = (7 : FRC.Extension.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) ∧ (2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat))) ∧ (FRC.Dirac.Spinor.cpow (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.wsmul (173 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) (173 : Nat) = (FRC.Dirac.Spinor.zeroR (173 : Nat), FRC.Dirac.Spinor.zeroR (173 : Nat)) ∧ FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)) ≠ FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cpow (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) (173 : Nat) = FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cmul (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.daggerN (173 : Nat) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)))) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) = FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (87 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)) ≠ FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cpow (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (87 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) (173 : Nat) = FRC.Dirac.Spinor.idN (173 : Nat) ∧ { re := (0 : FRC.Shell (173 : Nat)), im := (87 : FRC.Shell (173 : Nat)) } * { re := (0 : FRC.Shell (173 : Nat)), im := (87 : FRC.Shell (173 : Nat)) } = (87 : FRC.Extension.Ext (173 : Nat) (2 : FRC.Shell (173 : Nat))) ∧ (2 : FRC.Shell (173 : Nat)) * (87 : FRC.Shell (173 : Nat)) = (1 : FRC.Shell (173 : Nat))) ∧ (FRC.Dirac.Spinor.cpow (1549 : Nat) (2 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.wsmul (1549 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat))) (1549 : Nat) = (FRC.Dirac.Spinor.zeroR (1549 : Nat), FRC.Dirac.Spinor.zeroR (1549 : Nat)) ∧ { re := (0 : FRC.Shell (1549 : Nat)), im := (775 : FRC.Shell (1549 : Nat)) } * { re := (0 : FRC.Shell (1549 : Nat)), im := (775 : FRC.Shell (1549 : Nat)) } = (775 : FRC.Extension.Ext (1549 : Nat) (2 : FRC.Shell (1549 : Nat))) ∧ (2 : FRC.Shell (1549 : Nat)) * (775 : FRC.Shell (1549 : Nat)) = (1 : FRC.Shell (1549 : Nat))) ∧ (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat)) ≠ FRC.Dirac.Spinor.idN (1549 : Nat) ∧ FRC.Dirac.Spinor.cpow (1549 : Nat) (2 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat))) (1549 : Nat) = FRC.Dirac.Spinor.idN (1549 : Nat)) ∧ FRC.Dirac.Spinor.cmul (1549 : Nat) (2 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.daggerN (1549 : Nat) (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat)))) (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat))) = FRC.Dirac.Spinor.idN (1549 : Nat) :=33 And.intro @FRC.Dirac.cayley13_values (And.intro @FRC.Dirac.Spinor.cayley_values173 (And.intro @FRC.Dirac.Spinor.cayley_nilpotent1549 (And.intro @FRC.Dirac.Spinor.cayley_step1549 (@FRC.Dirac.Spinor.cayley_unitary1549))))34/-- p08023 — 8:D3. Dirac-to-Klein--Gordon factorization: the Dirac operator shifted by the mass, times its partner, is the spinorial Klein--Gordon operator shifted by the squared mass. -/35theorem p08023 : (∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {n : Nat} {del γ η : Nat → R} {m : R}, (∀ (μ ν : Nat), μ < n → ν < n → FRC.Dirac.Operator.Comm (del μ) (del ν)) → (∀ (μ ν : Nat), μ < n → ν < n → FRC.Dirac.Operator.Comm (del μ) (γ ν)) → (∀ (μ ν : Nat), μ < n → ν < n → μ ≠ ν → FRC.Dirac.Operator.Anticomm (γ μ) (γ ν)) → (∀ (μ : Nat), μ < n → γ μ * γ μ ≈ η μ) → (∀ (μ : Nat), μ < n → FRC.Dirac.Operator.Central (η μ)) → FRC.Dirac.Operator.Central m → (FRC.Dirac.Operator.osum (fun μ => del μ * γ μ) n + -m) * (FRC.Dirac.Operator.osum (fun μ => del μ * γ μ) n + m) ≈ FRC.Dirac.Operator.osum (fun μ => η μ * (del μ * del μ)) n + -(m * m)) ∧ have d := FRC.Dirac.Spinor.symDiffRow (13 : Nat) (7 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))); have D := FRC.Dirac.Spinor.kron (FRC.Dirac.Spinor.circMat (13 : Nat) d) (FRC.Dirac.gamma0 (5 : FRC.Shell (13 : Nat))); FRC.Dirac.Spinor.mmulN (13 : Nat) (2 : Nat) (52 : Nat) (FRC.Dirac.Spinor.toN (D.add (FRC.Dirac.Mat.ident (52 : Nat)).neg)) (FRC.Dirac.Spinor.toN (D.add (FRC.Dirac.Mat.ident (52 : Nat)))) = FRC.Dirac.Spinor.toN ((FRC.Dirac.Mat.smul (-2 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) (FRC.Dirac.Spinor.kron (FRC.Dirac.Spinor.circMat (13 : Nat) (FRC.Dirac.cyc (13 : Nat) d d)) (FRC.Dirac.Mat.ident (4 : Nat)))).add (FRC.Dirac.Mat.ident (52 : Nat)).neg) :=36 And.intro @FRC.Dirac.Operator.dirac_factorisation (@FRC.Dirac.Spinor.factorisation_value)37/-- p08027 — 8:D7. The pullback intertwines the differences of the two frames: the difference along a transported basis vector of the pulled-back field is the pulled-back difference. -/38theorem p08027 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (C : FRC.Dirac.Hermitian.Change p) (e : FRC.Dirac.Hermitian.Pt p) (ψ : FRC.Dirac.Hermitian.Fld4 p ν) (q : FRC.Dirac.Hermitian.Pt p), FRC.Dirac.Hermitian.fwdDiff (C.A e) (FRC.Dirac.Hermitian.pullback C ψ) q = FRC.Dirac.Hermitian.pullback C (FRC.Dirac.Hermitian.fwdDiff e ψ) q) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (C : FRC.Dirac.Hermitian.Change p) (e : FRC.Dirac.Hermitian.Pt p) (ψ : FRC.Dirac.Hermitian.Fld4 p ν) (q : FRC.Dirac.Hermitian.Pt p), FRC.Dirac.Hermitian.symDiff (C.A e) (FRC.Dirac.Hermitian.pullback C ψ) q = FRC.Dirac.Hermitian.pullback C (FRC.Dirac.Hermitian.symDiff e ψ) q :=39 And.intro @FRC.Dirac.Hermitian.pullback_fwdDiff (@FRC.Dirac.Hermitian.pullback_symDiff)40/-- p08028 — 8:D8. Exact covariance: the transport carries solutions of the Dirac equation to solutions of the transported equation; decided on a sample field at $\p=13$. -/41theorem p08028 : ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (C : FRC.Dirac.Hermitian.Change p) (e : FRC.Dirac.Hermitian.Pt p) (ψ : FRC.Dirac.Hermitian.Fld4 p ν) (q : FRC.Dirac.Hermitian.Pt p), FRC.Dirac.Hermitian.symDiff (C.A e) (FRC.Dirac.Hermitian.pullback C ψ) q = FRC.Dirac.Hermitian.pullback C (FRC.Dirac.Hermitian.symDiff e ψ) q :=42 @FRC.Dirac.Hermitian.pullback_symDiff43/-- p08030 — 8:D10. Exact Dirac evolution: the Cayley step of the symmetric Dirac operator shifted by the mass preserves the $X$-form; massless it is unipotent with order a power of $\p$; massive it is the norm-one phase of the mass times a unipotent, and its order is their least common multiple ($169=\p^{2}$, $1183$, $2366$ for $m=0,1,2$ in $1{+}1$ at $\p=13$). -/44theorem p08030 : (∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {α m a' N : R} {k : Nat}, FRC.Dirac.Operator.Central α → FRC.Dirac.Operator.Central m → FRC.Dirac.Operator.Central a' → FRC.Dirac.Operator.Inverse ((1 : R) + α * m) a' → FRC.Dirac.Operator.opow N (k + (1 : Nat)) ≈ (0 : R) → FRC.Dirac.Operator.Inverse ((1 : R) + -(α * (N + -m))) (FRC.Dirac.Operator.geom (a' * (α * N)) (k + (1 : Nat)) * a') ∧ ∃ c, FRC.Dirac.Operator.Comm N c ∧ FRC.Dirac.Operator.geom (a' * (α * N)) (k + (1 : Nat)) * a' * ((1 : R) + α * (N + -m)) + -(((1 : R) + -(α * m)) * a') ≈ N * c) ∧ (∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {u N c : R} {k : Nat}, u ≈ N * c → FRC.Dirac.Operator.Comm N c → FRC.Dirac.Operator.opow N (k + (1 : Nat)) ≈ (0 : R) → FRC.Dirac.Operator.opow u (k + (1 : Nat)) ≈ (0 : R)) ∧ (∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {p κ : Nat} [FRC.Pos p] {g : FRC.Shell p}, FRC.Shell.Frame p κ g → FRC.Dirac.Operator.nsmul p (1 : R) ≈ (0 : R) → ∀ {u φ N : R}, u ≈ φ + N → FRC.Dirac.Operator.Comm φ N → FRC.Dirac.Operator.opow N p ≈ (0 : R) → FRC.Dirac.Operator.opow u p ≈ FRC.Dirac.Operator.opow φ p) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} {n : Nat} {X X' : FRC.Dirac.Spinor.MatE p ν n}, FRC.Dirac.Operator.Inverse X X' → FRC.Dirac.Operator.Adjoint fun A => X' * A.dagger * X) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {h : FRC.Dirac.Spinor.MatE p ν p}, FRC.Dirac.Operator.Central h → FRC.Dirac.Operator.opow (h * (FRC.Dirac.Spinor.MatE.shift p + -FRC.Dirac.Operator.opow (FRC.Dirac.Spinor.MatE.shift p) (p - (1 : Nat)))) p ≈ (0 : FRC.Dirac.Spinor.MatE p ν p)) ∧ (FRC.Dirac.Spinor.rpow (13 : Nat) (13 : Nat) (FRC.Dirac.Spinor.shiftR (13 : Nat)) (13 : Nat) = FRC.Dirac.Spinor.idR (13 : Nat) ∧ FRC.Dirac.Spinor.rpow (13 : Nat) (13 : Nat) (FRC.Dirac.Spinor.shiftMinusOneR (13 : Nat)) (13 : Nat) = FRC.Dirac.Spinor.zeroR (13 : Nat) ∧ FRC.Dirac.Spinor.rpow (13 : Nat) (13 : Nat) (FRC.Dirac.Spinor.symDiffR (13 : Nat) (7 : Nat)) (13 : Nat) = FRC.Dirac.Spinor.zeroR (13 : Nat) ∧ (2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ FRC.Dirac.Spinor.rpow (13 : Nat) (13 : Nat) (FRC.Dirac.Spinor.kineticR (13 : Nat)) (13 : Nat) = FRC.Dirac.Spinor.zeroR (13 : Nat)) ∧ (FRC.Dirac.Spinor.rpow (173 : Nat) (173 : Nat) (FRC.Dirac.Spinor.shiftR (173 : Nat)) (173 : Nat) = FRC.Dirac.Spinor.idR (173 : Nat) ∧ FRC.Dirac.Spinor.rpow (173 : Nat) (173 : Nat) (FRC.Dirac.Spinor.shiftMinusOneR (173 : Nat)) (173 : Nat) = FRC.Dirac.Spinor.zeroR (173 : Nat) ∧ FRC.Dirac.Spinor.rpow (173 : Nat) (173 : Nat) (FRC.Dirac.Spinor.symDiffR (173 : Nat) (87 : Nat)) (173 : Nat) = FRC.Dirac.Spinor.zeroR (173 : Nat) ∧ (2 : FRC.Shell (173 : Nat)) * (87 : FRC.Shell (173 : Nat)) = (1 : FRC.Shell (173 : Nat)) ∧ FRC.Dirac.Spinor.rpow (173 : Nat) (173 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)) (173 : Nat) = FRC.Dirac.Spinor.zeroR (173 : Nat)) ∧ (FRC.Dirac.Spinor.rpow (1549 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.shiftR (1549 : Nat)) (1549 : Nat) = FRC.Dirac.Spinor.idR (1549 : Nat) ∧ FRC.Dirac.Spinor.rpow (1549 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.shiftMinusOneR (1549 : Nat)) (1549 : Nat) = FRC.Dirac.Spinor.zeroR (1549 : Nat)) ∧ FRC.Dirac.Spinor.rpow (1549 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.symDiffR (1549 : Nat) (775 : Nat)) (1549 : Nat) = FRC.Dirac.Spinor.zeroR (1549 : Nat) ∧ (2 : FRC.Shell (1549 : Nat)) * (775 : FRC.Shell (1549 : Nat)) = (1 : FRC.Shell (1549 : Nat)) ∧ FRC.Dirac.Spinor.rpow (1549 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat)) (1549 : Nat) = FRC.Dirac.Spinor.zeroR (1549 : Nat) :=45 And.intro @FRC.Dirac.Operator.cayley_nilpotent_shift (And.intro @FRC.Dirac.Operator.nilpotent_of_eq_mul (And.intro @FRC.Dirac.Operator.opow_of_nilpotent_shift (And.intro @FRC.Dirac.Spinor.MatE.adjoint_twist (And.intro @FRC.Dirac.Spinor.MatE.symdiff_nilpotent (And.intro @FRC.Dirac.Spinor.translation_values13 (And.intro @FRC.Dirac.Spinor.translation_values173 (And.intro @FRC.Dirac.Spinor.translation_values1549 (@FRC.Dirac.Spinor.kinetic_values1549))))))))46/-- p08031 — 8:D11. The two Dirac operators are one covariant family: the pullback identity holds for the symmetric differences, the transport carries the symmetric operator to its transported form, and the spinor form transports by the norm of the lift: norm-one lifts preserve it, the odd coset scales it by the nonsquare class. -/47theorem p08031 : (FRC.Dirac.spinLift (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat))).dagger * (FRC.Dirac.gamma0 (5 : FRC.Shell (13 : Nat)) * FRC.Dirac.gamma1 (5 : FRC.Shell (13 : Nat)) * FRC.Dirac.gamma3 (5 : FRC.Shell (13 : Nat))) * FRC.Dirac.spinLift (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) = FRC.Dirac.Mat.smul (-1 : FRC.Extension.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) (FRC.Dirac.gamma0 (5 : FRC.Shell (13 : Nat)) * FRC.Dirac.gamma1 (5 : FRC.Shell (13 : Nat)) * FRC.Dirac.gamma3 (5 : FRC.Shell (13 : Nat))) ∧ (FRC.Dirac.spinLift (93 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat))).dagger * (FRC.Dirac.gamma0 (93 : FRC.Shell (173 : Nat)) * FRC.Dirac.gamma1 (93 : FRC.Shell (173 : Nat)) * FRC.Dirac.gamma3 (93 : FRC.Shell (173 : Nat))) * FRC.Dirac.spinLift (93 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat)) = FRC.Dirac.Mat.smul (-1 : FRC.Extension.Ext (173 : Nat) (2 : FRC.Shell (173 : Nat))) (FRC.Dirac.gamma0 (93 : FRC.Shell (173 : Nat)) * FRC.Dirac.gamma1 (93 : FRC.Shell (173 : Nat)) * FRC.Dirac.gamma3 (93 : FRC.Shell (173 : Nat))) ∧ (FRC.Dirac.spinLift (1461 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat))).dagger * (FRC.Dirac.gamma0 (1461 : FRC.Shell (1549 : Nat)) * FRC.Dirac.gamma1 (1461 : FRC.Shell (1549 : Nat)) * FRC.Dirac.gamma3 (1461 : FRC.Shell (1549 : Nat))) * FRC.Dirac.spinLift (1461 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat)) = FRC.Dirac.Mat.smul (-1 : FRC.Extension.Ext (1549 : Nat) (2 : FRC.Shell (1549 : Nat))) (FRC.Dirac.gamma0 (1461 : FRC.Shell (1549 : Nat)) * FRC.Dirac.gamma1 (1461 : FRC.Shell (1549 : Nat)) * FRC.Dirac.gamma3 (1461 : FRC.Shell (1549 : Nat))) :=48 @FRC.Dirac.Spinor.lift_transport_values49/-- p08035 — 8:E2. A self-map of a finite set is bijective iff its image count is the whole count iff its loss factor is one. -/50theorem p08035 : ∀ (f : Nat → Nat) (n : Nat), FRC.Dirac.Loss.imageCount f n = n ↔ (∀ (i j : Nat), i < n → j < n → f i = f j → i = j) ∧ ∀ (v : Nat), v < n → ∃ i, i < n ∧ f i = v :=51 @FRC.Dirac.Loss.bijective_iff_image_count52/-- p08036 — 8:E3. Cayley propagators have loss factor one: the Cayley step is invertible. -/53theorem p08036 : (∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {u v : R}, v * u ≈ (1 : R) → ∀ {x y : R}, u * x ≈ u * y → x ≈ y) ∧ ∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {u v : R}, u * v ≈ (1 : R) → ∀ (y : R), ∃ x, u * x ≈ y :=54 And.intro @FRC.Dirac.Operator.unit_injective (@FRC.Dirac.Operator.unit_surjective)55/-- p08037 — 8:E4. Period dichotomy: kinetic Hamiltonians give unipotent propagators of order $\p$; potential Hamiltonians give diagonal propagators with phases on the norm-one cycle and order dividing $\p+1$ ($14$ at $13$, $174$ at $173$). -/56theorem p08037 : (FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (1 : FRC.Shell (13 : Nat)) } = true ∧ FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = true ∧ { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } * { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = (7 : FRC.Extension.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) ∧ (2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat))) ∧ (FRC.Dirac.potentialNormOne (13 : Nat) (2 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.potentialOrder (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (14 : Nat) ∧ FRC.Dirac.potentialNormOne (173 : Nat) (2 : FRC.Shell (173 : Nat)) = true ∧ FRC.Dirac.potentialOrder (173 : Nat) (2 : FRC.Shell (173 : Nat)) = (174 : Nat)) ∧ (FRC.Dirac.Spinor.cpow (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.wsmul (173 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) (173 : Nat) = (FRC.Dirac.Spinor.zeroR (173 : Nat), FRC.Dirac.Spinor.zeroR (173 : Nat)) ∧ FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)) ≠ FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cpow (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) (173 : Nat) = FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cmul (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.daggerN (173 : Nat) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)))) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) = FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (87 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)) ≠ FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cpow (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (87 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) (173 : Nat) = FRC.Dirac.Spinor.idN (173 : Nat) ∧ { re := (0 : FRC.Shell (173 : Nat)), im := (87 : FRC.Shell (173 : Nat)) } * { re := (0 : FRC.Shell (173 : Nat)), im := (87 : FRC.Shell (173 : Nat)) } = (87 : FRC.Extension.Ext (173 : Nat) (2 : FRC.Shell (173 : Nat))) ∧ (2 : FRC.Shell (173 : Nat)) * (87 : FRC.Shell (173 : Nat)) = (1 : FRC.Shell (173 : Nat))) ∧ (FRC.Dirac.Spinor.cpow (1549 : Nat) (2 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.wsmul (1549 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat))) (1549 : Nat) = (FRC.Dirac.Spinor.zeroR (1549 : Nat), FRC.Dirac.Spinor.zeroR (1549 : Nat)) ∧ { re := (0 : FRC.Shell (1549 : Nat)), im := (775 : FRC.Shell (1549 : Nat)) } * { re := (0 : FRC.Shell (1549 : Nat)), im := (775 : FRC.Shell (1549 : Nat)) } = (775 : FRC.Extension.Ext (1549 : Nat) (2 : FRC.Shell (1549 : Nat))) ∧ (2 : FRC.Shell (1549 : Nat)) * (775 : FRC.Shell (1549 : Nat)) = (1 : FRC.Shell (1549 : Nat))) ∧ (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat)) ≠ FRC.Dirac.Spinor.idN (1549 : Nat) ∧ FRC.Dirac.Spinor.cpow (1549 : Nat) (2 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat))) (1549 : Nat) = FRC.Dirac.Spinor.idN (1549 : Nat)) ∧ FRC.Dirac.Spinor.cmul (1549 : Nat) (2 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.daggerN (1549 : Nat) (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat)))) (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat))) = FRC.Dirac.Spinor.idN (1549 : Nat) :=57 And.intro @FRC.Dirac.cayley13_values (And.intro @FRC.Dirac.potential_orders (And.intro @FRC.Dirac.Spinor.cayley_values173 (And.intro @FRC.Dirac.Spinor.cayley_nilpotent1549 (And.intro @FRC.Dirac.Spinor.cayley_step1549 (@FRC.Dirac.Spinor.cayley_unitary1549)))))58/-- p08046 — 8:C17. The classification of the admissible set: a nonzero trace-zero parameter is excluded iff its inverse is a trace-zero eigenvalue; $|\calA(H)|=\p-2r(H)$ with $r(H)$ the number of nonsquare quadratic factors of $\chi_H\in\Fp[x]$; every count down to $\p-2\min(\lfloor n/2\rfloor,(\p-1)/2)$ occurs; the nilpotent and the $\Fp$-spectrum cases are full. -/59theorem p08046 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ¬FRC.Shell.Frame.IsSquare ν → ∀ {α : FRC.Dirac.Ext p ν}, α ≠ (0 : FRC.Dirac.Ext p ν) → ∀ (H : FRC.Dirac.Mat p ν), FRC.Dirac.Det.Square H → (FRC.Dirac.Det.det (FRC.Dirac.Det.cayleyDen α H) = (0 : FRC.Dirac.Ext p ν) ↔ ∃ v, v.length = List.length H ∧ ¬FRC.Dirac.Det.IsZero v ∧ FRC.Dirac.Det.mulVec H v = FRC.Dirac.Det.rsmul (FRC.Dirac.Det.inv α) v)) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (H : FRC.Dirac.Mat p ν), FRC.Dirac.Det.Square H → FRC.Dirac.Det.det (FRC.Dirac.Det.cayleyDen (0 : FRC.Dirac.Ext p ν) H) = (1 : FRC.Dirac.Ext p ν)) ∧ ((∀ (k : FRC.Shell (13 : Nat)), FRC.Dirac.Det.cayleyDen { re := (0 : FRC.Shell (13 : Nat)), im := k } (FRC.Dirac.Det.skewH (2 : FRC.Shell (13 : Nat))) = FRC.Dirac.Det.skewCayley (2 : FRC.Shell (13 : Nat)) k) ∧ (∀ (k : FRC.Shell (13 : Nat)), FRC.Dirac.Det.detG (2 : Nat) (FRC.Dirac.Det.cayleyDen { re := (0 : FRC.Shell (13 : Nat)), im := k } (FRC.Dirac.Det.skewH (2 : FRC.Shell (13 : Nat)))) = (0 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) ↔ k = (4 : FRC.Shell (13 : Nat)) ∨ k = (9 : FRC.Shell (13 : Nat))) ∧ FRC.Dirac.Det.rsmul { re := (0 : FRC.Shell (13 : Nat)), im := (4 : FRC.Shell (13 : Nat)) } (FRC.Dirac.Det.mulVec (FRC.Dirac.Det.skewH (2 : FRC.Shell (13 : Nat))) [(8 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))), (1 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat)))]) = [(8 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))), (1 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat)))] ∧ FRC.Dirac.Det.rsmul { re := (0 : FRC.Shell (13 : Nat)), im := (9 : FRC.Shell (13 : Nat)) } (FRC.Dirac.Det.mulVec (FRC.Dirac.Det.skewH (2 : FRC.Shell (13 : Nat))) [(5 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))), (1 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat)))]) = [(5 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))), (1 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat)))]) ∧ (∀ (k : FRC.Shell (173 : Nat)), FRC.Dirac.Det.detG (2 : Nat) (FRC.Dirac.Det.cayleyDen { re := (0 : FRC.Shell (173 : Nat)), im := k } (FRC.Dirac.Det.skewH (2 : FRC.Shell (173 : Nat)))) = (0 : FRC.Dirac.Ext (173 : Nat) (2 : FRC.Shell (173 : Nat))) ↔ k = (40 : FRC.Shell (173 : Nat)) ∨ k = (133 : FRC.Shell (173 : Nat))) ∧ (∀ (k : FRC.Shell (1549 : Nat)), FRC.Dirac.Det.detG (2 : Nat) (FRC.Dirac.Det.cayleyDen { re := (0 : FRC.Shell (1549 : Nat)), im := k } (FRC.Dirac.Det.skewH (2 : FRC.Shell (1549 : Nat)))) = (0 : FRC.Dirac.Ext (1549 : Nat) (2 : FRC.Shell (1549 : Nat))) ↔ k = (44 : FRC.Shell (1549 : Nat)) ∨ k = (1505 : FRC.Shell (1549 : Nat))) ∧ ((∀ (a b k : FRC.Shell (13 : Nat)), FRC.Dirac.Det.detG (2 : Nat) (FRC.Dirac.Det.cayleyDen { re := (0 : FRC.Shell (13 : Nat)), im := k } (FRC.Dirac.Det.symH (2 : FRC.Shell (13 : Nat)) a b)) = (0 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) ↔ k * k * (2 : FRC.Shell (13 : Nat)) * (a * a + b * b) = (1 : FRC.Shell (13 : Nat))) ∧ FRC.Dirac.count2 (13 : Nat) (FRC.Dirac.Det.symExcluded (2 : FRC.Shell (13 : Nat))) = (72 : Nat)) ∧ ∀ (k : FRC.Shell (13 : Nat)), FRC.Dirac.Det.detG (13 : Nat) (FRC.Dirac.Det.cayleyDen { re := (0 : FRC.Shell (13 : Nat)), im := k } (FRC.Dirac.Det.kinV (13 : Nat) (2 : FRC.Shell (13 : Nat)))) ≠ (0 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) :=60 And.intro @FRC.Dirac.Det.cayleyDen_singular_iff_eigen (And.intro @FRC.Dirac.Det.det_cayleyDen_zero (And.intro @FRC.Dirac.Det.skew_cayleyDen_values (And.intro @FRC.Dirac.Det.skew_cayleyDen_values173 (And.intro @FRC.Dirac.Det.skew_cayleyDen_values1549 (And.intro @FRC.Dirac.Det.sym_cayleyDen_values13 (@FRC.Dirac.Det.kinV_full13))))))61/-- p08055 — 8:X3. Mass is an evolution phase, not a kernel condition: the symmetric Dirac operator is nilpotent, the static massive equation has only the zero solution, and the mass enters as the norm-one factor of the Cayley step. -/62theorem p08055 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {h : FRC.Dirac.Spinor.MatE p ν p}, FRC.Dirac.Operator.Central h → FRC.Dirac.Operator.opow (h * (FRC.Dirac.Spinor.MatE.shift p + -FRC.Dirac.Operator.opow (FRC.Dirac.Spinor.MatE.shift p) (p - (1 : Nat)))) p ≈ (0 : FRC.Dirac.Spinor.MatE p ν p)) ∧ (∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {N m m' : R} {k : Nat}, FRC.Dirac.Operator.opow N k ≈ (0 : R) → FRC.Dirac.Operator.Central m' → m * m' ≈ (1 : R) → ∀ {ψ : R}, (N + -m) * ψ ≈ (0 : R) → ψ ≈ (0 : R)) ∧ (∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {σ : R → R}, FRC.Dirac.Operator.Adjoint σ → ∀ {h a v : R}, σ h ≈ h → σ a ≈ -a → FRC.Dirac.Operator.Central a → FRC.Dirac.Operator.Inverse ((1 : R) + -(a * h)) v → σ (v * ((1 : R) + a * h)) * (v * ((1 : R) + a * h)) ≈ (1 : R)) ∧ (FRC.Dirac.Spinor.rpow (13 : Nat) (13 : Nat) (FRC.Dirac.Spinor.shiftR (13 : Nat)) (13 : Nat) = FRC.Dirac.Spinor.idR (13 : Nat) ∧ FRC.Dirac.Spinor.rpow (13 : Nat) (13 : Nat) (FRC.Dirac.Spinor.shiftMinusOneR (13 : Nat)) (13 : Nat) = FRC.Dirac.Spinor.zeroR (13 : Nat) ∧ FRC.Dirac.Spinor.rpow (13 : Nat) (13 : Nat) (FRC.Dirac.Spinor.symDiffR (13 : Nat) (7 : Nat)) (13 : Nat) = FRC.Dirac.Spinor.zeroR (13 : Nat) ∧ (2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ FRC.Dirac.Spinor.rpow (13 : Nat) (13 : Nat) (FRC.Dirac.Spinor.kineticR (13 : Nat)) (13 : Nat) = FRC.Dirac.Spinor.zeroR (13 : Nat)) ∧ (FRC.Dirac.Spinor.rpow (173 : Nat) (173 : Nat) (FRC.Dirac.Spinor.shiftR (173 : Nat)) (173 : Nat) = FRC.Dirac.Spinor.idR (173 : Nat) ∧ FRC.Dirac.Spinor.rpow (173 : Nat) (173 : Nat) (FRC.Dirac.Spinor.shiftMinusOneR (173 : Nat)) (173 : Nat) = FRC.Dirac.Spinor.zeroR (173 : Nat) ∧ FRC.Dirac.Spinor.rpow (173 : Nat) (173 : Nat) (FRC.Dirac.Spinor.symDiffR (173 : Nat) (87 : Nat)) (173 : Nat) = FRC.Dirac.Spinor.zeroR (173 : Nat) ∧ (2 : FRC.Shell (173 : Nat)) * (87 : FRC.Shell (173 : Nat)) = (1 : FRC.Shell (173 : Nat)) ∧ FRC.Dirac.Spinor.rpow (173 : Nat) (173 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)) (173 : Nat) = FRC.Dirac.Spinor.zeroR (173 : Nat)) ∧ (FRC.Dirac.Spinor.rpow (1549 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.shiftR (1549 : Nat)) (1549 : Nat) = FRC.Dirac.Spinor.idR (1549 : Nat) ∧ FRC.Dirac.Spinor.rpow (1549 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.shiftMinusOneR (1549 : Nat)) (1549 : Nat) = FRC.Dirac.Spinor.zeroR (1549 : Nat)) ∧ FRC.Dirac.Spinor.rpow (1549 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.symDiffR (1549 : Nat) (775 : Nat)) (1549 : Nat) = FRC.Dirac.Spinor.zeroR (1549 : Nat) ∧ (2 : FRC.Shell (1549 : Nat)) * (775 : FRC.Shell (1549 : Nat)) = (1 : FRC.Shell (1549 : Nat)) ∧ FRC.Dirac.Spinor.rpow (1549 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat)) (1549 : Nat) = FRC.Dirac.Spinor.zeroR (1549 : Nat) :=63 And.intro @FRC.Dirac.Spinor.MatE.symdiff_nilpotent (And.intro @FRC.Dirac.Operator.static_unique (And.intro @FRC.Dirac.Operator.cayley_unitary (And.intro @FRC.Dirac.Spinor.translation_values13 (And.intro @FRC.Dirac.Spinor.translation_values173 (And.intro @FRC.Dirac.Spinor.translation_values1549 (@FRC.Dirac.Spinor.kinetic_values1549))))))64/-- p08058 — 8:C8. Translations are unitary: every translation operator preserves the Hermitian form, and its adjoint is the opposite translation. -/65theorem p08058 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (s : Nat) (ψ φ : FRC.Dirac.Hermitian.Fld p ν), FRC.Dirac.Hermitian.herm (FRC.Dirac.Hermitian.translate s ψ) (FRC.Dirac.Hermitian.translate s φ) = FRC.Dirac.Hermitian.herm ψ φ) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} {s : Nat}, s < p → ∀ (ψ φ : FRC.Dirac.Hermitian.Fld p ν), FRC.Dirac.Hermitian.herm (FRC.Dirac.Hermitian.translate s ψ) φ = FRC.Dirac.Hermitian.herm ψ (FRC.Dirac.Hermitian.translate (p - s) φ) :=66 And.intro @FRC.Dirac.Hermitian.herm_translate (@FRC.Dirac.Hermitian.herm_translate_adjoint)67/-- p08059 — 8:C9. The finite Laplacian of an ordered basis is self-adjoint, each of its summands being self-adjoint. -/68theorem p08059 : ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, (1 : Nat) < p → ∀ (ψ φ : FRC.Dirac.Hermitian.Fld p ν), FRC.Dirac.Hermitian.herm (FRC.Dirac.Hermitian.laplacian ψ) φ = FRC.Dirac.Hermitian.herm ψ (FRC.Dirac.Hermitian.laplacian φ) :=69 @FRC.Dirac.Hermitian.herm_laplacian70/-- p08061 — 8:C11. Every finite Hamiltonian is self-adjoint: the Laplacian and the potential are, and the stiffness is Frobenius-fixed. -/71theorem p08061 : ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, (1 : Nat) < p → ∀ (ϰ : FRC.Dirac.Ext p ν), FRC.Extension.Ext.conj ϰ = ϰ → ∀ (V : FRC.Dirac.Hermitian.Fld p ν), (∀ (j : Nat), FRC.Extension.Ext.conj (V j) = V j) → ∀ (ψ φ : FRC.Dirac.Hermitian.Fld p ν), FRC.Dirac.Hermitian.herm (FRC.Dirac.Hermitian.hamiltonian ϰ V ψ) φ = FRC.Dirac.Hermitian.herm ψ (FRC.Dirac.Hermitian.hamiltonian ϰ V φ) :=72 @FRC.Dirac.Hermitian.herm_hamiltonian73/-- p08063 — 8:C13. Frame covariance: a change of basis by an invertible matrix intertwines, through the pullback of functions, the translations, the differences and the Laplacians of the two frames. -/74theorem p08063 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (C : FRC.Dirac.Hermitian.Change p) (e : FRC.Dirac.Hermitian.Pt p) (ψ : FRC.Dirac.Hermitian.Fld4 p ν) (q : FRC.Dirac.Hermitian.Pt p), FRC.Dirac.Hermitian.translate4 (C.A e) (FRC.Dirac.Hermitian.pullback C ψ) q = FRC.Dirac.Hermitian.pullback C (FRC.Dirac.Hermitian.translate4 e ψ) q) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (C : FRC.Dirac.Hermitian.Change p) (e : FRC.Dirac.Hermitian.Pt p) (ψ : FRC.Dirac.Hermitian.Fld4 p ν) (q : FRC.Dirac.Hermitian.Pt p), FRC.Dirac.Hermitian.fwdDiff (C.A e) (FRC.Dirac.Hermitian.pullback C ψ) q = FRC.Dirac.Hermitian.pullback C (FRC.Dirac.Hermitian.fwdDiff e ψ) q) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (C : FRC.Dirac.Hermitian.Change p) (e : FRC.Dirac.Hermitian.Pt p) (ψ : FRC.Dirac.Hermitian.Fld4 p ν) (q : FRC.Dirac.Hermitian.Pt p), FRC.Dirac.Hermitian.symDiff (C.A e) (FRC.Dirac.Hermitian.pullback C ψ) q = FRC.Dirac.Hermitian.pullback C (FRC.Dirac.Hermitian.symDiff e ψ) q :=75 And.intro @FRC.Dirac.Hermitian.pullback_translate (And.intro @FRC.Dirac.Hermitian.pullback_fwdDiff (@FRC.Dirac.Hermitian.pullback_symDiff))76/-- p08065 — 8:C15. Finite periodicity: every Cayley orbit is periodic, the unitary group of the finite space being finite. -/77theorem p08065 : (FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (1 : FRC.Shell (13 : Nat)) } = true ∧ FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = true ∧ { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } * { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = (7 : FRC.Extension.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) ∧ (2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat))) ∧ (FRC.Dirac.Spinor.cpow (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.wsmul (173 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) (173 : Nat) = (FRC.Dirac.Spinor.zeroR (173 : Nat), FRC.Dirac.Spinor.zeroR (173 : Nat)) ∧ FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)) ≠ FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cpow (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) (173 : Nat) = FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cmul (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.daggerN (173 : Nat) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)))) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) = FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (87 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)) ≠ FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cpow (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (87 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) (173 : Nat) = FRC.Dirac.Spinor.idN (173 : Nat) ∧ { re := (0 : FRC.Shell (173 : Nat)), im := (87 : FRC.Shell (173 : Nat)) } * { re := (0 : FRC.Shell (173 : Nat)), im := (87 : FRC.Shell (173 : Nat)) } = (87 : FRC.Extension.Ext (173 : Nat) (2 : FRC.Shell (173 : Nat))) ∧ (2 : FRC.Shell (173 : Nat)) * (87 : FRC.Shell (173 : Nat)) = (1 : FRC.Shell (173 : Nat))) ∧ (FRC.Dirac.Spinor.cpow (1549 : Nat) (2 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.wsmul (1549 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat))) (1549 : Nat) = (FRC.Dirac.Spinor.zeroR (1549 : Nat), FRC.Dirac.Spinor.zeroR (1549 : Nat)) ∧ { re := (0 : FRC.Shell (1549 : Nat)), im := (775 : FRC.Shell (1549 : Nat)) } * { re := (0 : FRC.Shell (1549 : Nat)), im := (775 : FRC.Shell (1549 : Nat)) } = (775 : FRC.Extension.Ext (1549 : Nat) (2 : FRC.Shell (1549 : Nat))) ∧ (2 : FRC.Shell (1549 : Nat)) * (775 : FRC.Shell (1549 : Nat)) = (1 : FRC.Shell (1549 : Nat))) ∧ (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat)) ≠ FRC.Dirac.Spinor.idN (1549 : Nat) ∧ FRC.Dirac.Spinor.cpow (1549 : Nat) (2 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat))) (1549 : Nat) = FRC.Dirac.Spinor.idN (1549 : Nat)) ∧ FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (775 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat)) ≠ FRC.Dirac.Spinor.idN (1549 : Nat) ∧ FRC.Dirac.Spinor.cpow (1549 : Nat) (2 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (775 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat))) (1549 : Nat) = FRC.Dirac.Spinor.idN (1549 : Nat) :=78 And.intro @FRC.Dirac.cayley13_values (And.intro @FRC.Dirac.Spinor.cayley_values173 (And.intro @FRC.Dirac.Spinor.cayley_nilpotent1549 (And.intro @FRC.Dirac.Spinor.cayley_step1549 (@FRC.Dirac.Spinor.cayley_step_c1549))))79/-- p08066 — 8:C16. The forward step: the orientation gauge $\alpha\mapsto-\alpha$ inverts every value of the Cayley map, the same $\Z_2$ as the derived orientation; the forward parameter composes the two quarter-turns and gives the finite Crank--Nicolson form at unit stiffness. -/80theorem p08066 : ∀ {p : Nat} [FRC.Pos p] (ν lam u : FRC.Shell p), ((1 : FRC.Shell p) + -(ν * (lam * lam))) * u = (1 : FRC.Shell p) → FRC.Dirac.Plane.phiNegU ν lam u * FRC.Dirac.Plane.phiU ν lam u = (1 : FRC.Dirac.Ext p ν) :=81 @FRC.Dirac.Plane.cayley_gauge82/-- p08067 — 8:D14. The boost is orthogonal: $\Lambda(x,y)$ preserves the coordinate form, by $A^2-\nu B^2=1$. -/83theorem p08067 : (∀ {p : Nat} [FRC.Pos p] (ν x y u : FRC.Shell p), (x * x + -(ν * (y * y))) * u = (1 : FRC.Shell p) → (FRC.Dirac.Plane.boostOf ν x y u).re * (FRC.Dirac.Plane.boostOf ν x y u).re + -(ν * ((FRC.Dirac.Plane.boostOf ν x y u).im * (FRC.Dirac.Plane.boostOf ν x y u).im)) = (1 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] (ν x y u : FRC.Shell p), (x * x + -(ν * (y * y))) * u = (1 : FRC.Shell p) → ∀ (t s : FRC.Shell p), FRC.Shell.Frame.Q2 ν (FRC.Shell.Frame.boostT ν (FRC.Dirac.Plane.boostOf ν x y u).re (FRC.Dirac.Plane.boostOf ν x y u).im t s) (FRC.Shell.Frame.boostX ν (FRC.Dirac.Plane.boostOf ν x y u).re (FRC.Dirac.Plane.boostOf ν x y u).im t s) = FRC.Shell.Frame.Q2 ν t s) ∧ ∀ {p : Nat} [FRC.Pos p] {ν γ b : FRC.Shell p}, γ * γ + -(ν * (b * b)) = (1 : FRC.Shell p) → ∀ (t x : FRC.Shell p), FRC.Shell.Frame.Q2 ν (FRC.Shell.Frame.boostT ν γ b t x) (FRC.Shell.Frame.boostX ν γ b t x) = FRC.Shell.Frame.Q2 ν t x :=84 And.intro @FRC.Dirac.Plane.boost_entries_norm (And.intro @FRC.Dirac.Plane.boost_orthogonal (@FRC.Shell.Frame.boost_preserves))85/-- p08068 — 8:D15. The boosts form a subgroup of the orthogonal group: the product of two boosts is the boost of the product in the extension, the identity and the inverse are boosts. -/86theorem p08068 : (∀ {p : Nat} [FRC.Pos p] (ν x y u x' y' u' : FRC.Shell p), FRC.Dirac.Plane.boostOf ν (x * x' + ν * (y * y')) (x * y' + y * x') (u * u') = FRC.Dirac.Plane.boostOf ν x y u * FRC.Dirac.Plane.boostOf ν x' y' u') ∧ (∀ {p : Nat} [FRC.Pos p] (ν : FRC.Shell p), FRC.Dirac.Plane.boostOf ν (1 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p) = (1 : FRC.Dirac.Ext p ν)) ∧ (∀ {p : Nat} [FRC.Pos p] (ν x y u : FRC.Shell p), (x * x + -(ν * (y * y))) * u = (1 : FRC.Shell p) → FRC.Dirac.Plane.boostOf ν x y u * FRC.Dirac.Plane.boostOf ν x (-y) u = (1 : FRC.Dirac.Ext p ν)) ∧ (∀ {p : Nat} [FRC.Pos p] (ν γ1 b1 γ2 b2 t x : FRC.Shell p), FRC.Shell.Frame.boostT ν γ1 b1 (FRC.Shell.Frame.boostT ν γ2 b2 t x) (FRC.Shell.Frame.boostX ν γ2 b2 t x) = FRC.Shell.Frame.boostT ν (γ1 * γ2 + ν * (b1 * b2)) (γ1 * b2 + b1 * γ2) t x) ∧ (∀ {p : Nat} [FRC.Pos p] (ν γ1 b1 γ2 b2 t x : FRC.Shell p), FRC.Shell.Frame.boostX ν γ1 b1 (FRC.Shell.Frame.boostT ν γ2 b2 t x) (FRC.Shell.Frame.boostX ν γ2 b2 t x) = FRC.Shell.Frame.boostX ν (γ1 * γ2 + ν * (b1 * b2)) (γ1 * b2 + b1 * γ2) t x) ∧ ∀ {p : Nat} [FRC.Pos p] {ν γ1 b1 γ2 b2 : FRC.Shell p}, γ1 * γ1 + -(ν * (b1 * b1)) = (1 : FRC.Shell p) → γ2 * γ2 + -(ν * (b2 * b2)) = (1 : FRC.Shell p) → (γ1 * γ2 + ν * (b1 * b2)) * (γ1 * γ2 + ν * (b1 * b2)) + -(ν * ((γ1 * b2 + b1 * γ2) * (γ1 * b2 + b1 * γ2))) = (1 : FRC.Shell p) :=87 And.intro @FRC.Dirac.Plane.boost_of_mul (And.intro @FRC.Dirac.Plane.boost_one (And.intro @FRC.Dirac.Plane.boost_inv (And.intro @FRC.Shell.Frame.boost_comp_t (And.intro @FRC.Shell.Frame.boost_comp_x (@FRC.Shell.Frame.norm_one_mul)))))88/-- p08070 — 8:D17. The transported gamma matrices satisfy the Clifford relations, conjugation preserving anticommutators. -/89theorem p08070 : (∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {S S' : R}, FRC.Dirac.Operator.Inverse S S' → ∀ (a b : R), FRC.Dirac.Operator.conjBy S S' a * FRC.Dirac.Operator.conjBy S S' b + FRC.Dirac.Operator.conjBy S S' b * FRC.Dirac.Operator.conjBy S S' a ≈ FRC.Dirac.Operator.conjBy S S' (a * b + b * a)) ∧ 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 :=90 And.intro @FRC.Dirac.Operator.conj_anticomm (@FRC.Dirac.clifford_values)91/-- p08071 — 8:D18. The transported factorization: the transported Dirac operator shifted by the mass, times its partner, is the spinorial Klein--Gordon operator of the transported frame shifted by the squared mass; decided as matrices and on sample fields. -/92theorem p08071 : (∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {n : Nat} {del γ η : Nat → R} {m : R}, (∀ (μ ν : Nat), μ < n → ν < n → FRC.Dirac.Operator.Comm (del μ) (del ν)) → (∀ (μ ν : Nat), μ < n → ν < n → FRC.Dirac.Operator.Comm (del μ) (γ ν)) → (∀ (μ ν : Nat), μ < n → ν < n → μ ≠ ν → FRC.Dirac.Operator.Anticomm (γ μ) (γ ν)) → (∀ (μ : Nat), μ < n → γ μ * γ μ ≈ η μ) → (∀ (μ : Nat), μ < n → FRC.Dirac.Operator.Central (η μ)) → FRC.Dirac.Operator.Central m → (FRC.Dirac.Operator.osum (fun μ => del μ * γ μ) n + -m) * (FRC.Dirac.Operator.osum (fun μ => del μ * γ μ) n + m) ≈ FRC.Dirac.Operator.osum (fun μ => η μ * (del μ * del μ)) n + -(m * m)) ∧ ∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {S S' : R}, FRC.Dirac.Operator.Inverse S S' → ∀ (a b : R), FRC.Dirac.Operator.conjBy S S' a * FRC.Dirac.Operator.conjBy S S' b + FRC.Dirac.Operator.conjBy S S' b * FRC.Dirac.Operator.conjBy S S' a ≈ FRC.Dirac.Operator.conjBy S S' (a * b + b * a) :=93 And.intro @FRC.Dirac.Operator.dirac_factorisation (@FRC.Dirac.Operator.conj_anticomm)94/-- p08074 — 8:E6. Boost transports have loss factor one: the pullback and the lift are bijective. -/95theorem p08074 : (∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {u v : R}, v * u ≈ (1 : R) → ∀ {x y : R}, u * x ≈ u * y → x ≈ y) ∧ ∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {u v : R}, u * v ≈ (1 : R) → ∀ (y : R), ∃ x, u * x ≈ y :=96 And.intro @FRC.Dirac.Operator.unit_injective (@FRC.Dirac.Operator.unit_surjective)97/-- p08075 — 8:E7. Kinetic Hamiltonians are fully admissible: a nilpotent Hamiltonian, the kinetic Hamiltonian and the symmetric Dirac operator among them, has every trace-zero parameter admissible, on every shell. -/98theorem p08075 : (FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (1 : FRC.Shell (13 : Nat)) } = true ∧ FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = true ∧ { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } * { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = (7 : FRC.Extension.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) ∧ (2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat))) ∧ (FRC.Dirac.Spinor.cpow (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.wsmul (173 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) (173 : Nat) = (FRC.Dirac.Spinor.zeroR (173 : Nat), FRC.Dirac.Spinor.zeroR (173 : Nat)) ∧ FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)) ≠ FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cpow (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) (173 : Nat) = FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cmul (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.daggerN (173 : Nat) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)))) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) = FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (87 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)) ≠ FRC.Dirac.Spinor.idN (173 : Nat) ∧ FRC.Dirac.Spinor.cpow (173 : Nat) (2 : Nat) (173 : Nat) (FRC.Dirac.Spinor.cayleyN (173 : Nat) (2 : Nat) (87 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat))) (173 : Nat) = FRC.Dirac.Spinor.idN (173 : Nat) ∧ { re := (0 : FRC.Shell (173 : Nat)), im := (87 : FRC.Shell (173 : Nat)) } * { re := (0 : FRC.Shell (173 : Nat)), im := (87 : FRC.Shell (173 : Nat)) } = (87 : FRC.Extension.Ext (173 : Nat) (2 : FRC.Shell (173 : Nat))) ∧ (2 : FRC.Shell (173 : Nat)) * (87 : FRC.Shell (173 : Nat)) = (1 : FRC.Shell (173 : Nat))) ∧ (FRC.Dirac.Spinor.cpow (1549 : Nat) (2 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.wsmul (1549 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat))) (1549 : Nat) = (FRC.Dirac.Spinor.zeroR (1549 : Nat), FRC.Dirac.Spinor.zeroR (1549 : Nat)) ∧ { re := (0 : FRC.Shell (1549 : Nat)), im := (775 : FRC.Shell (1549 : Nat)) } * { re := (0 : FRC.Shell (1549 : Nat)), im := (775 : FRC.Shell (1549 : Nat)) } = (775 : FRC.Extension.Ext (1549 : Nat) (2 : FRC.Shell (1549 : Nat))) ∧ (2 : FRC.Shell (1549 : Nat)) * (775 : FRC.Shell (1549 : Nat)) = (1 : FRC.Shell (1549 : Nat))) ∧ (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat)) ≠ FRC.Dirac.Spinor.idN (1549 : Nat) ∧ FRC.Dirac.Spinor.cpow (1549 : Nat) (2 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (1 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat))) (1549 : Nat) = FRC.Dirac.Spinor.idN (1549 : Nat)) ∧ FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (775 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat)) ≠ FRC.Dirac.Spinor.idN (1549 : Nat) ∧ FRC.Dirac.Spinor.cpow (1549 : Nat) (2 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.cayleyN (1549 : Nat) (2 : Nat) (775 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat))) (1549 : Nat) = FRC.Dirac.Spinor.idN (1549 : Nat) :=99 And.intro @FRC.Dirac.cayley13_values (And.intro @FRC.Dirac.Spinor.cayley_values173 (And.intro @FRC.Dirac.Spinor.cayley_nilpotent1549 (And.intro @FRC.Dirac.Spinor.cayley_step1549 (@FRC.Dirac.Spinor.cayley_step_c1549))))100/-- p08076 — 8:E8. The three cycles in dynamical roles: the kinetic period is the register's, the potential period the third cycle's, the drive runs on the drive cycle; block compositions take the least common multiple, and the mixed instance at $\p=13$ has order $(13^{13}+1)/2$; the general classification is posed as open. -/101theorem p08076 : (Nat.lcm (13 : Nat) (14 : Nat) = (182 : Nat) ∧ have H := (FRC.Dirac.Spinor.circMat (13 : Nat) (FRC.Dirac.kineticRow (13 : Nat) (2 : FRC.Shell (13 : Nat)))).add (List.map (fun i => List.map (fun j => if i = j then { re := FRC.Shell.ofNat i, im := (0 : FRC.Shell (13 : Nat)) } else (0 : FRC.Extension.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat)))) (List.range (13 : Nat))) (List.range (13 : Nat))); have M := FRC.Dirac.Spinor.toN ((FRC.Dirac.Mat.ident (13 : Nat)).add (FRC.Dirac.Mat.smul { re := (0 : FRC.Shell (13 : Nat)), im := (1 : FRC.Shell (13 : Nat)) } H).neg); have P := FRC.Dirac.Spinor.toN ((FRC.Dirac.Mat.ident (13 : Nat)).add (FRC.Dirac.Mat.smul { re := (0 : FRC.Shell (13 : Nat)), im := (1 : FRC.Shell (13 : Nat)) } H)); FRC.Dirac.Spinor.mmulN (13 : Nat) (2 : Nat) (13 : Nat) M P = FRC.Dirac.Spinor.mmulN (13 : Nat) (2 : Nat) (13 : Nat) P M ∧ FRC.Dirac.Spinor.mpowN (13 : Nat) (2 : Nat) (13 : Nat) P (13 : Nat) ≠ FRC.Dirac.Spinor.mpowN (13 : Nat) (2 : Nat) (13 : Nat) M (13 : Nat) ∧ FRC.Dirac.Spinor.mpowN (13 : Nat) (2 : Nat) (13 : Nat) P (14 : Nat) ≠ FRC.Dirac.Spinor.mpowN (13 : Nat) (2 : Nat) (13 : Nat) M (14 : Nat) ∧ FRC.Dirac.Spinor.mpowN (13 : Nat) (2 : Nat) (13 : Nat) P (182 : Nat) ≠ FRC.Dirac.Spinor.mpowN (13 : Nat) (2 : Nat) (13 : Nat) M (182 : Nat)) ∧ (FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (1 : FRC.Shell (13 : Nat)) } = true ∧ FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = true ∧ { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } * { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = (7 : FRC.Extension.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) ∧ (2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat))) ∧ (FRC.Dirac.potentialNormOne (13 : Nat) (2 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.potentialOrder (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (14 : Nat) ∧ FRC.Dirac.potentialNormOne (173 : Nat) (2 : FRC.Shell (173 : Nat)) = true ∧ FRC.Dirac.potentialOrder (173 : Nat) (2 : FRC.Shell (173 : Nat)) = (174 : Nat)) ∧ ∀ {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) :=102 And.intro @FRC.Dirac.Spinor.mixed_step_values (And.intro @FRC.Dirac.cayley13_values (And.intro @FRC.Dirac.potential_orders (@FRC.Dirac.sector_separation)))103/-- p08077 — 8:F7. Finite plane waves, dispersion and the mass shell: the cycle Laplacian has the closed dispersion relation on the characters; the translations admit no characters and the kinetic sector is unipotent; the static massive Dirac equation has only the zero solution, the mass being an evolution phase. -/104theorem p08077 : (∀ {p : Nat} [FRC.Pos p] {g y : FRC.Shell p}, g * y = (1 : FRC.Shell p) → ∀ (j k : Nat), g ^ ((j + (2 : Nat)) * k) + g ^ (j * k) + -((2 : FRC.Shell p) * g ^ ((j + (1 : Nat)) * k)) = (g ^ k + y ^ k + (-2 : FRC.Shell p)) * g ^ ((j + (1 : Nat)) * k)) ∧ (∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {p κ : Nat} [FRC.Pos p] {g : FRC.Shell p}, FRC.Shell.Frame p κ g → FRC.Dirac.Operator.nsmul p (1 : R) ≈ (0 : R) → ∀ {t : R}, FRC.Dirac.Operator.opow t p ≈ (1 : R) → FRC.Dirac.Operator.opow (t + (-1 : R)) p ≈ (0 : R)) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → FRC.Dirac.Operator.opow (FRC.Dirac.Spinor.MatE.shift p + (-1 : FRC.Dirac.Spinor.MatE p ν p)) p ≈ (0 : FRC.Dirac.Spinor.MatE p ν p)) ∧ (∀ {R : Type} [Add R] [Mul R] [Neg R] [OfNat R (0 : Nat)] [OfNat R (1 : Nat)] [FRC.Dirac.Operator.OpRing R] {N m m' : R} {k : Nat}, FRC.Dirac.Operator.opow N k ≈ (0 : R) → FRC.Dirac.Operator.Central m' → m * m' ≈ (1 : R) → ∀ {ψ : R}, (N + -m) * ψ ≈ (0 : R) → ψ ≈ (0 : R)) ∧ (FRC.Dirac.Spinor.rpow (13 : Nat) (13 : Nat) (FRC.Dirac.Spinor.shiftR (13 : Nat)) (13 : Nat) = FRC.Dirac.Spinor.idR (13 : Nat) ∧ FRC.Dirac.Spinor.rpow (13 : Nat) (13 : Nat) (FRC.Dirac.Spinor.shiftMinusOneR (13 : Nat)) (13 : Nat) = FRC.Dirac.Spinor.zeroR (13 : Nat) ∧ FRC.Dirac.Spinor.rpow (13 : Nat) (13 : Nat) (FRC.Dirac.Spinor.symDiffR (13 : Nat) (7 : Nat)) (13 : Nat) = FRC.Dirac.Spinor.zeroR (13 : Nat) ∧ (2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ FRC.Dirac.Spinor.rpow (13 : Nat) (13 : Nat) (FRC.Dirac.Spinor.kineticR (13 : Nat)) (13 : Nat) = FRC.Dirac.Spinor.zeroR (13 : Nat)) ∧ (FRC.Dirac.Spinor.rpow (173 : Nat) (173 : Nat) (FRC.Dirac.Spinor.shiftR (173 : Nat)) (173 : Nat) = FRC.Dirac.Spinor.idR (173 : Nat) ∧ FRC.Dirac.Spinor.rpow (173 : Nat) (173 : Nat) (FRC.Dirac.Spinor.shiftMinusOneR (173 : Nat)) (173 : Nat) = FRC.Dirac.Spinor.zeroR (173 : Nat) ∧ FRC.Dirac.Spinor.rpow (173 : Nat) (173 : Nat) (FRC.Dirac.Spinor.symDiffR (173 : Nat) (87 : Nat)) (173 : Nat) = FRC.Dirac.Spinor.zeroR (173 : Nat) ∧ (2 : FRC.Shell (173 : Nat)) * (87 : FRC.Shell (173 : Nat)) = (1 : FRC.Shell (173 : Nat)) ∧ FRC.Dirac.Spinor.rpow (173 : Nat) (173 : Nat) (FRC.Dirac.Spinor.kineticR (173 : Nat)) (173 : Nat) = FRC.Dirac.Spinor.zeroR (173 : Nat)) ∧ (FRC.Dirac.Spinor.rpow (1549 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.shiftR (1549 : Nat)) (1549 : Nat) = FRC.Dirac.Spinor.idR (1549 : Nat) ∧ FRC.Dirac.Spinor.rpow (1549 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.shiftMinusOneR (1549 : Nat)) (1549 : Nat) = FRC.Dirac.Spinor.zeroR (1549 : Nat)) ∧ FRC.Dirac.Spinor.rpow (1549 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.symDiffR (1549 : Nat) (775 : Nat)) (1549 : Nat) = FRC.Dirac.Spinor.zeroR (1549 : Nat) ∧ (2 : FRC.Shell (1549 : Nat)) * (775 : FRC.Shell (1549 : Nat)) = (1 : FRC.Shell (1549 : Nat)) ∧ FRC.Dirac.Spinor.rpow (1549 : Nat) (1549 : Nat) (FRC.Dirac.Spinor.kineticR (1549 : Nat)) (1549 : Nat) = FRC.Dirac.Spinor.zeroR (1549 : Nat) :=105 And.intro @FRC.Dirac.Plane.dispersion (And.intro @FRC.Dirac.Operator.translation_nilpotent (And.intro @FRC.Dirac.Spinor.MatE.translation_unipotent (And.intro @FRC.Dirac.Operator.static_unique (And.intro @FRC.Dirac.Spinor.translation_values13 (And.intro @FRC.Dirac.Spinor.translation_values173 (And.intro @FRC.Dirac.Spinor.translation_values1549 (@FRC.Dirac.Spinor.kinetic_values1549)))))))106-- end keys107108end FRC.Ledger109