IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.FiniteMulCharacter

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/FiniteMulCharacter.lean
   3
   4  A first δ-native finite multiplicative character interface. This is not the
   5  older PRC cost-character/orientation surface; it is a residue-unit character
   6  surface meant for period and Dirichlet-style arithmetic.
   7-/
   8
   9import Mathlib
  10import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodSpectrum
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace PrimitiveRecognitionCalculus
  15namespace Factorization
  16
  17open DistinctionNat
  18
  19/-- A finite multiplicative character on unit residues modulo `N`, represented
  20as a complex-valued function on orbit representatives that respects the native
  21residue relation and multiplies on unit residues. -/
  22structure FiniteMulCharacter (N : DistinctionNat) where
  23  eval : DistinctionNat → ℂ
  24  respects_residue :
  25    ∀ {a b : DistinctionNat} {hN : N ≠ zero},
  26      sameResidue N hN a b → eval a = eval b
  27  map_one : eval one = 1
  28  map_mul_units :
  29    ∀ {a b : DistinctionNat},
  30      unitResidue N a → unitResidue N b →
  31        eval (a * b) = eval a * eval b
  32
  33namespace FiniteMulCharacter
  34
  35/-- The constant-one principal character on unit residues. -/
  36def principal (N : DistinctionNat) : FiniteMulCharacter N where
  37  eval := fun _ => 1
  38  respects_residue := by
  39    intro a b hN h
  40    rfl
  41  map_one := rfl
  42  map_mul_units := by
  43    intro a b ha hb
  44    norm_num
  45
  46@[simp] theorem principal_eval (N a : DistinctionNat) :
  47    (principal N).eval a = 1 := rfl
  48
  49theorem principal_map_mul_units (N a b : DistinctionNat)
  50    (ha : unitResidue N a) (hb : unitResidue N b) :
  51    (principal N).eval (a * b) =
  52      (principal N).eval a * (principal N).eval b := by
  53  exact (principal N).map_mul_units ha hb
  54
  55/-- Product of two finite multiplicative characters. -/
  56def mul {N : DistinctionNat}
  57    (χ ψ : FiniteMulCharacter N) : FiniteMulCharacter N where
  58  eval := fun a => χ.eval a * ψ.eval a
  59  respects_residue := by
  60    intro a b hN h
  61    rw [χ.respects_residue h, ψ.respects_residue h]
  62  map_one := by
  63    rw [χ.map_one, ψ.map_one]
  64    norm_num
  65  map_mul_units := by
  66    intro a b ha hb
  67    rw [χ.map_mul_units ha hb, ψ.map_mul_units ha hb]
  68    ring
  69
  70theorem mul_eval {N : DistinctionNat}
  71    (χ ψ : FiniteMulCharacter N) (a : DistinctionNat) :
  72    (mul χ ψ).eval a = χ.eval a * ψ.eval a := rfl
  73
  74/-- Sum of a character over a finite representative list after left
  75multiplication by a unit. -/
  76theorem scaled_list_eval_sum {N : DistinctionNat}
  77    (χ : FiniteMulCharacter N) (t : DistinctionNat)
  78    (L : List DistinctionNat)
  79    (ht : unitResidue N t)
  80    (hunits : ∀ a ∈ L, unitResidue N a) :
  81    (L.map (fun a => χ.eval (t * a))).sum =
  82      χ.eval t * (L.map χ.eval).sum := by
  83  induction L with
  84  | nil =>
  85      simp
  86  | cons a rest ih =>
  87      have ha : unitResidue N a := hunits a (by simp)
  88      have hrest : ∀ b ∈ rest, unitResidue N b := by
  89        intro b hb
  90        exact hunits b (by simp [hb])
  91      have ih' := ih hrest
  92      simp [χ.map_mul_units ht ha, ih', mul_add]
  93
  94/-- Finite-character orthogonality in the form needed by the δ residue layer.
  95If left multiplication by a unit `t` cycles the chosen representative list and
  96the character is nontrivial on `t`, then the character sum over that list is
  97zero. -/
  98theorem orthogonality_nonprincipal_sum_zero {N : DistinctionNat}
  99    (χ : FiniteMulCharacter N) (t : DistinctionNat)
 100    (L : List DistinctionNat)
 101    (ht : unitResidue N t)
 102    (hunits : ∀ a ∈ L, unitResidue N a)
 103    (hcycle : L.map (fun a => t * a) = L)
 104    (hnontrivial : χ.eval t ≠ 1) :
 105    (L.map χ.eval).sum = 0 := by
 106  let S : ℂ := (L.map χ.eval).sum
 107  have hscaled :
 108      (L.map (fun a => χ.eval (t * a))).sum = S := by
 109    have hcycleEval :=
 110      congrArg (fun M : List DistinctionNat => (M.map χ.eval).sum) hcycle
 111    simpa [List.map_map, S] using hcycleEval
 112  have hmul :
 113      (L.map (fun a => χ.eval (t * a))).sum = χ.eval t * S := by
 114    exact scaled_list_eval_sum χ t L ht hunits
 115  have hmulEq : χ.eval t * S = S := by
 116    rw [← hmul, hscaled]
 117  have hzero : (χ.eval t - 1) * S = 0 := by
 118    rw [sub_mul, one_mul, hmulEq, sub_self]
 119  rcases mul_eq_zero.mp hzero with hleft | hright
 120  · exfalso
 121    exact hnontrivial (sub_eq_zero.mp hleft)
 122  · exact hright
 123
 124end FiniteMulCharacter
 125
 126/-- Certificate for the finite character interface. -/
 127structure FiniteMulCharacterCertificate : Prop where
 128  principal_exists :
 129    ∀ N : DistinctionNat, (FiniteMulCharacter.principal N).eval one = 1
 130  principal_multiplicative :
 131    ∀ N a b : DistinctionNat,
 132      unitResidue N a → unitResidue N b →
 133        (FiniteMulCharacter.principal N).eval (a * b) =
 134          (FiniteMulCharacter.principal N).eval a *
 135            (FiniteMulCharacter.principal N).eval b
 136  character_product_eval :
 137    ∀ {N : DistinctionNat} (χ ψ : FiniteMulCharacter N) (a : DistinctionNat),
 138      (FiniteMulCharacter.mul χ ψ).eval a = χ.eval a * ψ.eval a
 139  scaled_list_eval_sum :
 140    ∀ {N : DistinctionNat} (χ : FiniteMulCharacter N)
 141      (t : DistinctionNat) (L : List DistinctionNat),
 142      unitResidue N t →
 143        (∀ a ∈ L, unitResidue N a) →
 144          (L.map (fun a => χ.eval (t * a))).sum =
 145            χ.eval t * (L.map χ.eval).sum
 146  orthogonality_nonprincipal_sum_zero :
 147    ∀ {N : DistinctionNat} (χ : FiniteMulCharacter N)
 148      (t : DistinctionNat) (L : List DistinctionNat),
 149      unitResidue N t →
 150        (∀ a ∈ L, unitResidue N a) →
 151          L.map (fun a => t * a) = L →
 152            χ.eval t ≠ 1 →
 153              (L.map χ.eval).sum = 0
 154
 155theorem finite_mul_character_certificate : FiniteMulCharacterCertificate where
 156  principal_exists := by
 157    intro N
 158    exact (FiniteMulCharacter.principal N).map_one
 159  principal_multiplicative := by
 160    intro N a b ha hb
 161    exact FiniteMulCharacter.principal_map_mul_units N a b ha hb
 162  character_product_eval := by
 163    intro N χ ψ a
 164    exact FiniteMulCharacter.mul_eval χ ψ a
 165  scaled_list_eval_sum := by
 166    intro N χ t L ht hunits
 167    exact FiniteMulCharacter.scaled_list_eval_sum χ t L ht hunits
 168  orthogonality_nonprincipal_sum_zero := by
 169    intro N χ t L ht hunits hcycle hnontrivial
 170    exact FiniteMulCharacter.orthogonality_nonprincipal_sum_zero
 171      χ t L ht hunits hcycle hnontrivial
 172
 173end Factorization
 174end PrimitiveRecognitionCalculus
 175end Foundation
 176end IndisputableMonolith
 177