Theme/Hermitian.lean — FrcCore

1import FrcCore.Cycle2import FrcCore.Theme.Dirac34/-!5# The Hermitian layer of 8-dirac — sums in the extension, the form, the translations, the Laplacian, no axioms67The third file of the dirac theme (5 November 2026, the core-proof programme): the Hermitian form on fields of the8register with values in the coefficient field `K = 𝔽_p(√ν)`, on every shell. A field is a function `Nat → Ext p ν`9read on the register `[0, p)`; a sum of field values is the pair of the base theme's `sumRange` sums of the components10(`esum`), so every identity of sums reduces to the base theme's (`sum_add`, `sum_neg`, `sum_mul_left`, `sum_eq_single`,11and the cycle's `sum_shift`). The form `⟨ψ, φ⟩ = Σ_x ψ̄(x) φ(x)` is Hermitian, `conj ⟨ψ, φ⟩ = ⟨φ, ψ⟩`, sesquilinear, and12nondegenerate — a field orthogonal to every field vanishes at every register site, by the delta fields (C2). The13translation `(T_s ψ)(x) = ψ(x + s)` preserves the form, and its adjoint is the opposite translation (C8, by the shift14invariance of the cycle sum); the Laplacian `Δψ = T_1 ψ + T_{p−1} ψ − 2ψ` is self-adjoint (C9); a finite Hamiltonian15`H = −ϰΔ + V` with `ϰ` and `V` Frobenius-fixed is self-adjoint (C11). Frame covariance: an additive bijection of the16coordinate points (the boost) pulls fields back, and the pullback intertwines the translations and the differences of17the two frames (C13, D7). Nothing here needs function extensionality: equalities of fields are stated at every site. No18axioms.19-/2021namespace FRC.Dirac.Hermitian2223open FRC FRC.Shell FRC.Extension2425variable {p : Nat} [Pos p] {ν : Shell p}2627/-! ## The ring identities of the extension on components -/28section ext29open FRC.Extension.Ext (conj ofShell)3031theorem add_re (z z' : Ext p ν) : (z + z').re = z.re + z'.re := rfl32theorem add_im (z z' : Ext p ν) : (z + z').im = z.im + z'.im := rfl33theorem neg_re (z : Ext p ν) : (-z).re = -z.re := rfl34theorem neg_im (z : Ext p ν) : (-z).im = -z.im := rfl35theorem zero_re : (0 : Ext p ν).re = 0 := rfl36theorem zero_im : (0 : Ext p ν).im = 0 := rfl37theorem one_re : (1 : Ext p ν).re = 1 := rfl38theorem one_im : (1 : Ext p ν).im = 0 := rfl3940theorem add_comm (z z' : Ext p ν) : z + z' = z' + z := FRC.Extension.Ext.ext (Shell.add_comm _ _) (Shell.add_comm _ _)41theorem add_assoc (a b c : Ext p ν) : a + b + c = a + (b + c) := FRC.Extension.Ext.ext (Shell.add_assoc _ _ _) (Shell.add_assoc _ _ _)42theorem zero_add (z : Ext p ν) : 0 + z = z := FRC.Extension.Ext.ext (Shell.zero_add _) (Shell.zero_add _)43theorem add_zero (z : Ext p ν) : z + 0 = z := FRC.Extension.Ext.ext (Shell.add_zero _) (Shell.add_zero _)44theorem add_neg (z : Ext p ν) : z + -z = 0 := FRC.Extension.Ext.ext (Shell.add_neg _) (Shell.add_neg _)45theorem neg_add (z : Ext p ν) : -z + z = 0 := FRC.Extension.Ext.ext (Shell.neg_add _) (Shell.neg_add _)46theorem neg_neg (z : Ext p ν) : - -z = z := FRC.Extension.Ext.ext (Shell.neg_neg _) (Shell.neg_neg _)47theorem neg_add_rev (z z' : Ext p ν) : -(z + z') = -z + -z' := FRC.Extension.Ext.ext (Shell.neg_add_rev _ _) (Shell.neg_add_rev _ _)48theorem zero_mul (z : Ext p ν) : (0 : Ext p ν) * z = 0 := by49  apply FRC.Extension.Ext.ext50  · show 0 * z.re + ν * (0 * z.im) = 051    rw [Shell.zero_mul, Shell.zero_mul, Shell.mul_zero, Shell.add_zero]52  · show 0 * z.im + 0 * z.re = 053    rw [Shell.zero_mul, Shell.zero_mul, Shell.add_zero]54theorem mul_zero (z : Ext p ν) : z * 0 = 0 := by rw [FRC.Extension.Ext.mul_comm]; exact zero_mul z55theorem mul_add (a b c : Ext p ν) : a * (b + c) = a * b + a * c := by56  apply FRC.Extension.Ext.ext57  · show a.re * (b.re + c.re) + ν * (a.im * (b.im + c.im)) = a.re * b.re + ν * (a.im * b.im) + (a.re * c.re + ν * (a.im * c.im))58    rw [Shell.left_distrib, Shell.left_distrib, Shell.left_distrib, Shell.add_add_add_comm]59  · show a.re * (b.im + c.im) + a.im * (b.re + c.re) = a.re * b.im + a.im * b.re + (a.re * c.im + a.im * c.re)60    rw [Shell.left_distrib, Shell.left_distrib, Shell.add_add_add_comm]61theorem add_mul (a b c : Ext p ν) : (a + b) * c = a * c + b * c := by62  rw [FRC.Extension.Ext.mul_comm, mul_add, FRC.Extension.Ext.mul_comm c a, FRC.Extension.Ext.mul_comm c b]63theorem neg_mul (a b : Ext p ν) : -(a * b) = -a * b := by64  apply FRC.Extension.Ext.ext65  · show -(a.re * b.re + ν * (a.im * b.im)) = -a.re * b.re + ν * (-a.im * b.im)66    rw [Shell.neg_add_rev, Shell.neg_mul, ← Shell.neg_mul, Shell.mul_neg ν, Shell.neg_mul a.im]67  · show -(a.re * b.im + a.im * b.re) = -a.re * b.im + -a.im * b.re68    rw [Shell.neg_add_rev, Shell.neg_mul, Shell.neg_mul]69theorem mul_neg (a b : Ext p ν) : -(a * b) = a * -b := by rw [FRC.Extension.Ext.mul_comm, neg_mul, FRC.Extension.Ext.mul_comm]70theorem conj_add (z z' : Ext p ν) : conj (z + z') = conj z + conj z' := FRC.Extension.Ext.ext rfl (Shell.neg_add_rev _ _)71theorem conj_neg (z : Ext p ν) : conj (-z) = -conj z := FRC.Extension.Ext.ext rfl rfl72theorem conj_zero : conj (0 : Ext p ν) = 0 := FRC.Extension.Ext.ext rfl Shell.neg_zero73theorem conj_one : conj (1 : Ext p ν) = 1 := FRC.Extension.Ext.ext rfl Shell.neg_zero74theorem conj_ofShell (c : Shell p) : conj (ofShell c : Ext p ν) = ofShell c := FRC.Extension.Ext.ext rfl Shell.neg_zero75/-- `(a + b) + (c + d) = (a + c) + (b + d)` in the extension. -/76theorem add_add_add_comm (a b c d : Ext p ν) : a + b + (c + d) = a + c + (b + d) :=77  FRC.Extension.Ext.ext (Shell.add_add_add_comm _ _ _ _) (Shell.add_add_add_comm _ _ _ _)78end ext7980/-! ## Sums in the extension, on components -/81section sums8283/-- `Σ_{j<n} f j` in the extension: the pair of the component sums. -/84def esum (f : Nat → Ext p ν) (n : Nat) : Ext p ν :=85  ⟨sumRange (fun j => (f j).re) n, sumRange (fun j => (f j).im) n⟩8687theorem esum_re (f : Nat → Ext p ν) (n : Nat) : (esum f n).re = sumRange (fun j => (f j).re) n := rfl88theorem esum_im (f : Nat → Ext p ν) (n : Nat) : (esum f n).im = sumRange (fun j => (f j).im) n := rfl89theorem esum_zero (f : Nat → Ext p ν) : esum f 0 = 0 := rfl90theorem esum_succ (f : Nat → Ext p ν) (n : Nat) : esum f (n + 1) = esum f n + f n := rfl9192theorem esum_congr {f h : Nat → Ext p ν} (n : Nat) (e : ∀ j, j < n → f j = h j) : esum f n = esum h n :=93  FRC.Extension.Ext.ext (sum_congr n fun j hj => FRC.Extension.Ext.re_congr (e j hj)) (sum_congr n fun j hj => FRC.Extension.Ext.im_congr (e j hj))9495theorem esum_add (f h : Nat → Ext p ν) (n : Nat) : esum (fun j => f j + h j) n = esum f n + esum h n :=96  FRC.Extension.Ext.ext (sum_add _ _ n) (sum_add _ _ n)9798theorem esum_neg (f : Nat → Ext p ν) (n : Nat) : esum (fun j => -(f j)) n = -(esum f n) :=99  FRC.Extension.Ext.ext (sum_neg _ n) (sum_neg _ n)100101theorem esum_conj (f : Nat → Ext p ν) (n : Nat) : FRC.Extension.Ext.conj (esum f n) = esum (fun j => FRC.Extension.Ext.conj (f j)) n :=102  FRC.Extension.Ext.ext rfl (by show -(sumRange (fun j => (f j).im) n) = sumRange (fun j => -(f j).im) n; rw [sum_neg])103104theorem esum_zero_of (f : Nat → Ext p ν) (n : Nat) (h : ∀ j, j < n → f j = 0) : esum f n = 0 :=105  FRC.Extension.Ext.ext (sum_zero n fun j hj => FRC.Extension.Ext.re_congr (h j hj)) (sum_zero n fun j hj => FRC.Extension.Ext.im_congr (h j hj))106107/-- A sum with one term: `Σ_{j<n} f j = f j₀` when every other term vanishes. -/108theorem esum_eq_single (f : Nat → Ext p ν) {j₀ n : Nat} (hj : j₀ < n) (h : ∀ j, j < n → j ≠ j₀ → f j = 0) :109    esum f n = f j₀ :=110  FRC.Extension.Ext.ext (sum_eq_single hj fun j hjn hne => FRC.Extension.Ext.re_congr (h j hjn hne))111    (sum_eq_single hj fun j hjn hne => FRC.Extension.Ext.im_congr (h j hjn hne))112113/-- A scalar pulls out of the sum on the left. -/114theorem esum_mul_left (c : Ext p ν) (f : Nat → Ext p ν) (n : Nat) : c * esum f n = esum (fun j => c * f j) n := by115  apply FRC.Extension.Ext.ext116  · show c.re * sumRange (fun j => (f j).re) n + ν * (c.im * sumRange (fun j => (f j).im) n) =117      sumRange (fun j => c.re * (f j).re + ν * (c.im * (f j).im)) n118    rw [sum_add, ← sum_mul_left, ← sum_mul_left, ← sum_mul_left]119  · show c.re * sumRange (fun j => (f j).im) n + c.im * sumRange (fun j => (f j).re) n =120      sumRange (fun j => c.re * (f j).im + c.im * (f j).re) n121    rw [sum_add, ← sum_mul_left, ← sum_mul_left]122123theorem esum_mul_right (c : Ext p ν) (f : Nat → Ext p ν) (n : Nat) : esum f n * c = esum (fun j => f j * c) n := by124  rw [FRC.Extension.Ext.mul_comm, esum_mul_left]; exact esum_congr n fun j _ => FRC.Extension.Ext.mul_comm _ _125126/-- The sum over the register is invariant under the shift of its index (the cycle's `sum_shift`). -/127theorem esum_shift (f : Nat → Ext p ν) (s : Nat) : esum (fun j => f ((j + s) % p)) p = esum f p :=128  FRC.Extension.Ext.ext (Cycle.sum_shift p (Pos.pos : 0 < p) (fun j => (f j).re) s) (Cycle.sum_shift p (Pos.pos : 0 < p) (fun j => (f j).im) s)129130end sums131132/-! ## The Hermitian form (8:C2) -/133section form134135/-- A field on the register with values in `K`, read on `[0, p)`. -/136abbrev Fld (p : Nat) [Pos p] (ν : Shell p) := Nat → Ext p ν137138/-- The Hermitian form `⟨ψ, φ⟩ = Σ_{x<p} ψ̄(x) φ(x)`, antilinear in the first slot. -/139def herm (ψ φ : Fld p ν) : Ext p ν := esum (fun j => FRC.Extension.Ext.conj (ψ j) * φ j) p140141/-- 8:C2 — the form is Hermitian: `conj ⟨ψ, φ⟩ = ⟨φ, ψ⟩`. -/142theorem herm_star (ψ φ : Fld p ν) : FRC.Extension.Ext.conj (herm ψ φ) = herm φ ψ := by143  unfold herm; rw [esum_conj]144  exact esum_congr p fun j _ => by rw [FRC.Extension.Ext.conj_mul, FRC.Extension.Ext.conj_conj, FRC.Extension.Ext.mul_comm]145146theorem herm_add_right (ψ φ φ' : Fld p ν) : herm ψ (fun j => φ j + φ' j) = herm ψ φ + herm ψ φ' := by147  unfold herm; rw [← esum_add]; exact esum_congr p fun j _ => mul_add _ _ _148149theorem herm_add_left (ψ ψ' φ : Fld p ν) : herm (fun j => ψ j + ψ' j) φ = herm ψ φ + herm ψ' φ := by150  unfold herm; rw [← esum_add]151  exact esum_congr p fun j _ => by152    show FRC.Extension.Ext.conj (ψ j + ψ' j) * φ j = _153    rw [conj_add, add_mul]154155theorem herm_neg_right (ψ φ : Fld p ν) : herm ψ (fun j => -(φ j)) = -(herm ψ φ) := by156  unfold herm; rw [← esum_neg]; exact esum_congr p fun j _ => (mul_neg _ _).symm157158theorem herm_neg_left (ψ φ : Fld p ν) : herm (fun j => -(ψ j)) φ = -(herm ψ φ) := by159  unfold herm; rw [← esum_neg]160  exact esum_congr p fun j _ => by161    show FRC.Extension.Ext.conj (-(ψ j)) * φ j = _162    rw [conj_neg, ← neg_mul]163164theorem herm_smul_right (c : Ext p ν) (ψ φ : Fld p ν) : herm ψ (fun j => c * φ j) = c * herm ψ φ := by165  unfold herm; rw [esum_mul_left]166  exact esum_congr p fun j _ => by167    show FRC.Extension.Ext.conj (ψ j) * (c * φ j) = c * (FRC.Extension.Ext.conj (ψ j) * φ j)168    rw [← FRC.Extension.Ext.mul_assoc, FRC.Extension.Ext.mul_comm (FRC.Extension.Ext.conj (ψ j)) c,169      FRC.Extension.Ext.mul_assoc]170171theorem herm_smul_left (c : Ext p ν) (ψ φ : Fld p ν) : herm (fun j => c * ψ j) φ = FRC.Extension.Ext.conj c * herm ψ φ := by172  unfold herm; rw [esum_mul_left]173  exact esum_congr p fun j _ => by174    show FRC.Extension.Ext.conj (c * ψ j) * φ j = _175    rw [FRC.Extension.Ext.conj_mul, FRC.Extension.Ext.mul_assoc]176177/-- The delta field at the site `x`. -/178def delta (x : Nat) : Fld p ν := fun j => if j = x then 1 else 0179180theorem herm_delta (ψ : Fld p ν) {x : Nat} (hx : x < p) : herm ψ (delta x) = FRC.Extension.Ext.conj (ψ x) := by181  unfold herm182  rw [esum_eq_single (fun j => FRC.Extension.Ext.conj (ψ j) * delta x j) hx]183  · show FRC.Extension.Ext.conj (ψ x) * (if x = x then 1 else 0) = FRC.Extension.Ext.conj (ψ x)184    rw [ite_eq_left rfl]; exact FRC.Extension.Ext.mul_one _185  · intro j _ hne186    show FRC.Extension.Ext.conj (ψ j) * (if j = x then 1 else 0) = 0187    rw [ite_eq_right hne]; exact mul_zero _188189/-- 8:C2 — the form is nondegenerate: a field orthogonal to every field vanishes at every site of the register190(its conjugate against the delta field is the site's value). -/191theorem herm_nondegenerate (ψ : Fld p ν) (h : ∀ φ : Fld p ν, herm ψ φ = 0) : ∀ x, x < p → ψ x = 0 := by192  intro x hx193  have e := h (delta x)194  rw [herm_delta ψ hx] at e195  rw [← FRC.Extension.Ext.conj_conj (ψ x), e, conj_zero]196197end form198199/-! ## Translations, the Laplacian and the Hamiltonians (8:C8, C9, C11) -/200section translations201202/-- The translation `(T_s ψ)(x) = ψ(x + s)` on the register. -/203def translate (s : Nat) (ψ : Fld p ν) : Fld p ν := fun j => ψ ((j + s) % p)204205/-- 8:C8 — translations are unitary: `⟨T_s ψ, T_s φ⟩ = ⟨ψ, φ⟩`. -/206theorem herm_translate (s : Nat) (ψ φ : Fld p ν) : herm (translate s ψ) (translate s φ) = herm ψ φ :=207  esum_shift (fun j => FRC.Extension.Ext.conj (ψ j) * φ j) s208209/-- `((j + s) % p + (p − s)) % p = j` for `j < p` and `s < p`: the shift and its opposite cancel on the register. -/210theorem shift_cancel {s j : Nat} (hs : s < p) (hj : j < p) : ((j + s) % p + (p - s)) % p = j := by211  have h := FRC.Nat.add_mul_mod_self_left j 1 p (Pos.pos : 0 < p)212  rw [Nat.mul_one] at h213  rw [FRC.Nat.mod_add_mod _ _ _ (Pos.pos : 0 < p), Nat.add_assoc, FRC.Nat.add_sub_of_le (Nat.le_of_lt hs), Nat.add_comm j p,214    h, FRC.Nat.mod_eq_of_lt hj]215216/-- 8:C8 — the adjoint of a translation is the opposite translation: `⟨T_s ψ, φ⟩ = ⟨ψ, T_{p−s} φ⟩` for `s < p`. -/217theorem herm_translate_adjoint {s : Nat} (hs : s < p) (ψ φ : Fld p ν) :218    herm (translate s ψ) φ = herm ψ (translate (p - s) φ) := by219  unfold herm translate220  rw [← esum_shift (fun j => FRC.Extension.Ext.conj (ψ j) * φ ((j + (p - s)) % p)) s]221  apply esum_congr p222  intro j hj223  show FRC.Extension.Ext.conj (ψ ((j + s) % p)) * φ j = FRC.Extension.Ext.conj (ψ ((j + s) % p)) * φ (((j + s) % p + (p - s)) % p)224  rw [shift_cancel hs hj]225226/-- The Laplacian `Δψ = T_1 ψ + T_{p−1} ψ − 2ψ` (the second difference on the cycle). -/227def laplacian (ψ : Fld p ν) : Fld p ν := fun j => translate 1 ψ j + translate (p - 1) ψ j + -(ψ j + ψ j)228229theorem sub_one_lt : p - 1 < p := Nat.sub_lt (Pos.pos : 0 < p) Nat.one_pos230231omit [Pos p] in232/-- `p − (p − 1) = 1` on a register of more than one site. -/233theorem sub_sub_one (h2 : 1 < p) : p - (p - 1) = 1 := by234  have h1 : p - 1 + 1 = p := FRC.Nat.sub_add_cancel (Nat.le_of_lt h2)235  calc p - (p - 1) = p - 1 + 1 - (p - 1) := by rw [h1]236    _ = 1 := FRC.Nat.add_sub_cancel_left _ _237238/-- 8:C9 — the Laplacian is self-adjoint, each of its summands being self-adjoint: `T_1` and `T_{p−1}` are239adjoint to each other and the diagonal term is real. -/240theorem herm_laplacian (h2 : 1 < p) (ψ φ : Fld p ν) : herm (laplacian ψ) φ = herm ψ (laplacian φ) := by241  unfold laplacian242  rw [herm_add_left, herm_add_left, herm_neg_left, herm_add_left, herm_add_right, herm_add_right, herm_neg_right,243    herm_add_right, herm_translate_adjoint h2, herm_translate_adjoint sub_one_lt,244    sub_sub_one h2, add_comm (herm ψ (translate (p - 1) φ))]245246/-- The finite Hamiltonian `Hψ = −ϰ Δψ + V ψ` of stiffness `ϰ` and potential `V`. -/247def hamiltonian (ϰ : Ext p ν) (V : Fld p ν) (ψ : Fld p ν) : Fld p ν :=248  fun j => -(ϰ * laplacian ψ j) + V j * ψ j249250/-- A real potential is symmetric for the form: `⟨Vψ, φ⟩ = ⟨ψ, Vφ⟩` when `conj (V x) = V x` at every site. -/251theorem herm_potential (V : Fld p ν) (hV : ∀ j, FRC.Extension.Ext.conj (V j) = V j) (ψ φ : Fld p ν) :252    herm (fun j => V j * ψ j) φ = herm ψ (fun j => V j * φ j) := by253  unfold herm254  apply esum_congr p255  intro j _256  show FRC.Extension.Ext.conj (V j * ψ j) * φ j = FRC.Extension.Ext.conj (ψ j) * (V j * φ j)257  rw [FRC.Extension.Ext.conj_mul, hV j, FRC.Extension.Ext.mul_assoc, ← FRC.Extension.Ext.mul_assoc,258    FRC.Extension.Ext.mul_comm (V j) (FRC.Extension.Ext.conj (ψ j)), FRC.Extension.Ext.mul_assoc]259260/-- 8:C11 — every finite Hamiltonian is self-adjoint: the Laplacian is, the potential is real, and the stiffness261is Frobenius-fixed. -/262theorem herm_hamiltonian (h2 : 1 < p) (ϰ : Ext p ν) (hϰ : FRC.Extension.Ext.conj ϰ = ϰ) (V : Fld p ν) (hV : ∀ j, FRC.Extension.Ext.conj (V j) = V j)263    (ψ φ : Fld p ν) : herm (hamiltonian ϰ V ψ) φ = herm ψ (hamiltonian ϰ V φ) := by264  unfold hamiltonian265  rw [herm_add_left, herm_add_right, herm_neg_left, herm_neg_right, herm_smul_left, herm_smul_right, hϰ,266    herm_laplacian h2, herm_potential V hV]267268end translations269270/-! ## Frame covariance: the pullback intertwines the translations and the differences (8:C13, D7) -/271section covariance272273/-- A point of the coordinate shell `𝔽_p⁴`. -/274structure Pt (p : Nat) [Pos p] where275  t : Shell p276  x : Shell p277  y : Shell p278  z : Shell p279280theorem Pt.ext {a b : Pt p} (ht : a.t = b.t) (hx : a.x = b.x) (hy : a.y = b.y) (hz : a.z = b.z) : a = b := by281  cases a; cases b; cases ht; cases hx; cases hy; cases hz; rfl282283instance : Add (Pt p) := ⟨fun a b => ⟨a.t + b.t, a.x + b.x, a.y + b.y, a.z + b.z⟩⟩284instance : Neg (Pt p) := ⟨fun a => ⟨-a.t, -a.x, -a.y, -a.z⟩⟩285instance : OfNat (Pt p) 0 := ⟨⟨0, 0, 0, 0⟩⟩286287theorem Pt.zero_add (a : Pt p) : (0 : Pt p) + a = a :=288  Pt.ext (Shell.zero_add _) (Shell.zero_add _) (Shell.zero_add _) (Shell.zero_add _)289theorem Pt.add_neg (a : Pt p) : a + -a = 0 :=290  Pt.ext (Shell.add_neg _) (Shell.add_neg _) (Shell.add_neg _) (Shell.add_neg _)291theorem Pt.add_right_cancel {a b c : Pt p} (h : a + c = b + c) : a = b :=292  Pt.ext (Shell.add_right_cancel (congrArg Pt.t h)) (Shell.add_right_cancel (congrArg Pt.x h))293    (Shell.add_right_cancel (congrArg Pt.y h)) (Shell.add_right_cancel (congrArg Pt.z h))294theorem Pt.neg_eq_of_add_eq_zero {a b : Pt p} (h : a + b = 0) : -a = b :=295  Pt.ext (Shell.neg_eq_of_add_eq_zero (congrArg Pt.t h)) (Shell.neg_eq_of_add_eq_zero (congrArg Pt.x h))296    (Shell.neg_eq_of_add_eq_zero (congrArg Pt.y h)) (Shell.neg_eq_of_add_eq_zero (congrArg Pt.z h))297298/-- A spinor-free field on the coordinate shell. -/299abbrev Fld4 (p : Nat) [Pos p] (ν : Shell p) := Pt p → Ext p ν300301/-- A change of frame: an additive bijection `A` of the points, given with its inverse (the boosts of `Plane`,302read on the coordinates, are such changes). -/303structure Change (p : Nat) [Pos p] where304  A : Pt p → Pt p305  Ainv : Pt p → Pt p306  inv_left : ∀ q, Ainv (A q) = q307  inv_right : ∀ q, A (Ainv q) = q308  add : ∀ q r, A (q + r) = A q + A r309310theorem Change.map_zero (C : Change p) : C.A 0 = 0 := by311  have h := C.add 0 0312  rw [Pt.zero_add] at h313  exact (Pt.add_right_cancel ((Pt.zero_add (C.A 0)).trans h)).symm314315theorem Change.map_neg (C : Change p) (e : Pt p) : C.A (-e) = -(C.A e) := by316  have h := C.add e (-e)317  rw [Pt.add_neg, C.map_zero] at h318  exact (Pt.neg_eq_of_add_eq_zero h.symm).symm319320/-- The inverse of a change is additive against the image: `A⁻¹(q + A e) = A⁻¹ q + e`. -/321theorem Change.inv_add (C : Change p) (q e : Pt p) : C.Ainv (q + C.A e) = C.Ainv q + e := by322  have h : q + C.A e = C.A (C.Ainv q + e) := by rw [C.add, C.inv_right]323  rw [h, C.inv_left]324325/-- The pullback `(A_* ψ)(q) = ψ(A⁻¹ q)` of a field under the change of frame. -/326def pullback (C : Change p) (ψ : Fld4 p ν) : Fld4 p ν := fun q => ψ (C.Ainv q)327328/-- The translation `(T_e ψ)(q) = ψ(q + e)` on the coordinate shell. -/329def translate4 (e : Pt p) (ψ : Fld4 p ν) : Fld4 p ν := fun q => ψ (q + e)330331/-- The forward difference `(∂_e ψ)(q) = ψ(q + e) − ψ(q)`. -/332def fwdDiff (e : Pt p) (ψ : Fld4 p ν) : Fld4 p ν := fun q => translate4 e ψ q + -(ψ q)333334/-- The symmetric difference `(∂^s_e ψ)(q) = ψ(q + e) − ψ(q − e)`. -/335def symDiff (e : Pt p) (ψ : Fld4 p ν) : Fld4 p ν := fun q => translate4 e ψ q + -(translate4 (-e) ψ q)336337/-- 8:C13, 8:D7 — the pullback intertwines the translations: `T_{Ae} (A_* ψ) = A_* (T_e ψ)` at every point. -/338theorem pullback_translate (C : Change p) (e : Pt p) (ψ : Fld4 p ν) (q : Pt p) :339    translate4 (C.A e) (pullback C ψ) q = pullback C (translate4 e ψ) q := by340  show ψ (C.Ainv (q + C.A e)) = ψ (C.Ainv q + e)341  rw [C.inv_add]342343/-- 8:C13, 8:D7 — the pullback intertwines the forward differences: `∂_{Ae} (A_* ψ) = A_* (∂_e ψ)` at every344point, so the transported difference operator is the difference along the transported direction. -/345theorem pullback_fwdDiff (C : Change p) (e : Pt p) (ψ : Fld4 p ν) (q : Pt p) :346    fwdDiff (C.A e) (pullback C ψ) q = pullback C (fwdDiff e ψ) q := by347  show translate4 (C.A e) (pullback C ψ) q + -(pullback C ψ q) = translate4 e ψ (C.Ainv q) + -(ψ (C.Ainv q))348  rw [pullback_translate]; rfl349350/-- 8:C13, 8:D7, 8:D8 — the pullback intertwines the symmetric differences: `∂^s_{Ae} (A_* ψ) = A_* (∂^s_e ψ)` at351every point (the change is additive, so it sends `−e` to `−Ae`). -/352theorem pullback_symDiff (C : Change p) (e : Pt p) (ψ : Fld4 p ν) (q : Pt p) :353    symDiff (C.A e) (pullback C ψ) q = pullback C (symDiff e ψ) q := by354  show translate4 (C.A e) (pullback C ψ) q + -(translate4 (-(C.A e)) (pullback C ψ) q) =355    translate4 e ψ (C.Ainv q) + -(translate4 (-e) ψ (C.Ainv q))356  rw [← C.map_neg, pullback_translate, pullback_translate]; rfl357358end covariance359360end FRC.Dirac.Hermitian361