IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.UnitGroup

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/UnitGroup.lean
   3
   4  Unit residues modulo an orbit modulus. This is the first finite
   5  multiplicative surface needed for Dirichlet-style characters and period
   6  readout.
   7-/
   8
   9import Mathlib
  10import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.ResidueOrbit
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace PrimitiveRecognitionCalculus
  15namespace Factorization
  16
  17open DistinctionNat
  18
  19/-- A residue representative is a unit modulo `N` when it is δ-coprime to `N`. -/
  20def unitResidue (N a : DistinctionNat) : Prop :=
  21  coprime a N
  22
  23theorem unitResidue_iff_nat_coprime (N a : DistinctionNat) :
  24    unitResidue N a ↔ Nat.Coprime a.toNat N.toNat := by
  25  unfold unitResidue
  26  exact coprime_iff_nat_coprime a N
  27
  28theorem unitResidue_one (N : DistinctionNat) :
  29    unitResidue N one := by
  30  rw [unitResidue_iff_nat_coprime, one_toNat]
  31  exact Nat.coprime_one_left N.toNat
  32
  33theorem unitResidue_mul_closed {N a b : DistinctionNat}
  34    (ha : unitResidue N a) (hb : unitResidue N b) :
  35    unitResidue N (a * b) := by
  36  rw [unitResidue_iff_nat_coprime] at ha hb ⊢
  37  rw [toNat_mul]
  38  exact Nat.Coprime.mul_left ha hb
  39
  40theorem unitResidue_pow_closed {N a : DistinctionNat}
  41    (ha : unitResidue N a) (k : Nat) :
  42    Nat.Coprime (a.toNat ^ k) N.toNat := by
  43  rw [unitResidue_iff_nat_coprime] at ha
  44  exact Nat.Coprime.pow_left k ha
  45
  46/-- Unit residues form the carrier for finite multiplicative character theory. -/
  47structure UnitResidue (N : DistinctionNat) : Type where
  48  val : DistinctionNat
  49  isUnit : unitResidue N val
  50
  51namespace UnitResidue
  52
  53variable {N : DistinctionNat}
  54
  55/-- The identity unit residue. -/
  56def one (N : DistinctionNat) : UnitResidue N where
  57  val := DistinctionNat.one
  58  isUnit := unitResidue_one N
  59
  60/-- Multiplication of unit residues. -/
  61def mul (u v : UnitResidue N) : UnitResidue N where
  62  val := u.val * v.val
  63  isUnit := unitResidue_mul_closed u.isUnit v.isUnit
  64
  65theorem mul_val (u v : UnitResidue N) :
  66    (mul u v).val = u.val * v.val := rfl
  67
  68theorem one_val (N : DistinctionNat) :
  69    (one N).val = DistinctionNat.one := rfl
  70
  71end UnitResidue
  72
  73/-- Certificate for the unit-residue surface. -/
  74structure UnitGroupCertificate : Prop where
  75  unit_display :
  76    ∀ N a : DistinctionNat,
  77      unitResidue N a ↔ Nat.Coprime a.toNat N.toNat
  78  one_is_unit :
  79    ∀ N : DistinctionNat, unitResidue N one
  80  mul_closed :
  81    ∀ {N a b : DistinctionNat},
  82      unitResidue N a → unitResidue N b → unitResidue N (a * b)
  83  pow_closed_display :
  84    ∀ {N a : DistinctionNat},
  85      unitResidue N a → ∀ k : Nat, Nat.Coprime (a.toNat ^ k) N.toNat
  86
  87theorem unit_group_certificate : UnitGroupCertificate where
  88  unit_display := unitResidue_iff_nat_coprime
  89  one_is_unit := unitResidue_one
  90  mul_closed := by
  91    intro N a b ha hb
  92    exact unitResidue_mul_closed ha hb
  93  pow_closed_display := by
  94    intro N a ha k
  95    exact unitResidue_pow_closed ha k
  96
  97end Factorization
  98end PrimitiveRecognitionCalculus
  99end Foundation
 100end IndisputableMonolith
 101