IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.ResidueOrbit

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/ResidueOrbit.lean
   3
   4  δ-native residues modulo an orbit position, defined by the existing native
   5  remainder operation. Nat modular arithmetic appears only as a verifier
   6  display surface.
   7-/
   8
   9import Mathlib
  10import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.ChartTransition
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace PrimitiveRecognitionCalculus
  15namespace Factorization
  16
  17open DistinctionNat
  18
  19/-- The native residue of `a` modulo a nonzero orbit modulus `N`. -/
  20def residue (N : DistinctionNat) (hN : N ≠ zero) (a : DistinctionNat) :
  21    DistinctionNat :=
  22  remainder a N hN
  23
  24/-- Native equality of residues modulo `N`. -/
  25def sameResidue (N : DistinctionNat) (hN : N ≠ zero)
  26    (a b : DistinctionNat) : Prop :=
  27  residue N hN a = residue N hN b
  28
  29theorem residue_toNat (N : DistinctionNat) (hN : N ≠ zero)
  30    (a : DistinctionNat) :
  31    (residue N hN a).toNat = a.toNat % N.toNat := by
  32  unfold residue
  33  exact remainder_toNat a N hN
  34
  35theorem sameResidue_iff_mod_eq (N : DistinctionNat) (hN : N ≠ zero)
  36    (a b : DistinctionNat) :
  37    sameResidue N hN a b ↔ a.toNat % N.toNat = b.toNat % N.toNat := by
  38  constructor
  39  · intro h
  40    have hnat := congrArg DistinctionNat.toNat h
  41    simpa [sameResidue, residue_toNat] using hnat
  42  · intro h
  43    unfold sameResidue
  44    apply toNat_inj
  45    simpa [residue_toNat] using h
  46
  47theorem sameResidue_refl (N : DistinctionNat) (hN : N ≠ zero)
  48    (a : DistinctionNat) :
  49    sameResidue N hN a a := by
  50  unfold sameResidue
  51  rfl
  52
  53theorem sameResidue_symm {N a b : DistinctionNat} {hN : N ≠ zero}
  54    (h : sameResidue N hN a b) :
  55    sameResidue N hN b a := by
  56  unfold sameResidue at h ⊢
  57  exact h.symm
  58
  59theorem sameResidue_trans {N a b c : DistinctionNat} {hN : N ≠ zero}
  60    (hab : sameResidue N hN a b) (hbc : sameResidue N hN b c) :
  61    sameResidue N hN a c := by
  62  unfold sameResidue at hab hbc ⊢
  63  exact hab.trans hbc
  64
  65theorem sameResidue_add {N a b c d : DistinctionNat} {hN : N ≠ zero}
  66    (hab : sameResidue N hN a b) (hcd : sameResidue N hN c d) :
  67    sameResidue N hN (a + c) (b + d) := by
  68  rw [sameResidue_iff_mod_eq] at hab hcd ⊢
  69  rw [toNat_add, toNat_add]
  70  calc
  71    (a.toNat + c.toNat) % N.toNat
  72        = (a.toNat % N.toNat + c.toNat % N.toNat) % N.toNat := by
  73          exact Nat.add_mod a.toNat c.toNat N.toNat
  74    _ = (b.toNat % N.toNat + d.toNat % N.toNat) % N.toNat := by
  75          rw [hab, hcd]
  76    _ = (b.toNat + d.toNat) % N.toNat := by
  77          exact (Nat.add_mod b.toNat d.toNat N.toNat).symm
  78
  79theorem sameResidue_mul {N a b c d : DistinctionNat} {hN : N ≠ zero}
  80    (hab : sameResidue N hN a b) (hcd : sameResidue N hN c d) :
  81    sameResidue N hN (a * c) (b * d) := by
  82  rw [sameResidue_iff_mod_eq] at hab hcd ⊢
  83  rw [toNat_mul, toNat_mul]
  84  calc
  85    (a.toNat * c.toNat) % N.toNat
  86        = (a.toNat % N.toNat * (c.toNat % N.toNat)) % N.toNat := by
  87          exact Nat.mul_mod a.toNat c.toNat N.toNat
  88    _ = (b.toNat % N.toNat * (d.toNat % N.toNat)) % N.toNat := by
  89          rw [hab, hcd]
  90    _ = (b.toNat * d.toNat) % N.toNat := by
  91          exact (Nat.mul_mod b.toNat d.toNat N.toNat).symm
  92
  93/-- Residue-level addition represented back on orbit positions. -/
  94def residueAdd (N : DistinctionNat) (hN : N ≠ zero)
  95    (a b : DistinctionNat) : DistinctionNat :=
  96  residue N hN (a + b)
  97
  98/-- Residue-level multiplication represented back on orbit positions. -/
  99def residueMul (N : DistinctionNat) (hN : N ≠ zero)
 100    (a b : DistinctionNat) : DistinctionNat :=
 101  residue N hN (a * b)
 102
 103theorem residueAdd_toNat_mod (N : DistinctionNat) (hN : N ≠ zero)
 104    (a b : DistinctionNat) :
 105    (residueAdd N hN a b).toNat =
 106      (a.toNat + b.toNat) % N.toNat := by
 107  unfold residueAdd
 108  rw [residue_toNat, toNat_add]
 109
 110theorem residueMul_toNat_mod (N : DistinctionNat) (hN : N ≠ zero)
 111    (a b : DistinctionNat) :
 112    (residueMul N hN a b).toNat =
 113      (a.toNat * b.toNat) % N.toNat := by
 114  unfold residueMul
 115  rw [residue_toNat, toNat_mul]
 116
 117/-- Certificate for the residue orbit layer. -/
 118structure ResidueOrbitCertificate : Prop where
 119  residue_display :
 120    ∀ (N : DistinctionNat) (hN : N ≠ zero) (a : DistinctionNat),
 121      (residue N hN a).toNat = a.toNat % N.toNat
 122  same_residue_display :
 123    ∀ (N : DistinctionNat) (hN : N ≠ zero) (a b : DistinctionNat),
 124      sameResidue N hN a b ↔ a.toNat % N.toNat = b.toNat % N.toNat
 125  same_residue_refl :
 126    ∀ (N : DistinctionNat) (hN : N ≠ zero) (a : DistinctionNat),
 127      sameResidue N hN a a
 128  same_residue_symm :
 129    ∀ {N a b : DistinctionNat} {hN : N ≠ zero},
 130      sameResidue N hN a b → sameResidue N hN b a
 131  same_residue_trans :
 132    ∀ {N a b c : DistinctionNat} {hN : N ≠ zero},
 133      sameResidue N hN a b → sameResidue N hN b c →
 134        sameResidue N hN a c
 135  same_residue_add :
 136    ∀ {N a b c d : DistinctionNat} {hN : N ≠ zero},
 137      sameResidue N hN a b → sameResidue N hN c d →
 138        sameResidue N hN (a + c) (b + d)
 139  same_residue_mul :
 140    ∀ {N a b c d : DistinctionNat} {hN : N ≠ zero},
 141      sameResidue N hN a b → sameResidue N hN c d →
 142        sameResidue N hN (a * c) (b * d)
 143  residue_add_display :
 144    ∀ (N : DistinctionNat) (hN : N ≠ zero) (a b : DistinctionNat),
 145      (residueAdd N hN a b).toNat = (a.toNat + b.toNat) % N.toNat
 146  residue_mul_display :
 147    ∀ (N : DistinctionNat) (hN : N ≠ zero) (a b : DistinctionNat),
 148      (residueMul N hN a b).toNat = (a.toNat * b.toNat) % N.toNat
 149
 150theorem residue_orbit_certificate : ResidueOrbitCertificate where
 151  residue_display := residue_toNat
 152  same_residue_display := sameResidue_iff_mod_eq
 153  same_residue_refl := sameResidue_refl
 154  same_residue_symm := by
 155    intro N a b hN h
 156    exact sameResidue_symm h
 157  same_residue_trans := by
 158    intro N a b c hN hab hbc
 159    exact sameResidue_trans hab hbc
 160  same_residue_add := by
 161    intro N a b c d hN hab hcd
 162    exact sameResidue_add hab hcd
 163  same_residue_mul := by
 164    intro N a b c d hN hab hcd
 165    exact sameResidue_mul hab hcd
 166  residue_add_display := residueAdd_toNat_mod
 167  residue_mul_display := residueMul_toNat_mod
 168
 169end Factorization
 170end PrimitiveRecognitionCalculus
 171end Foundation
 172end IndisputableMonolith
 173