IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodExistence

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/PeriodExistence.lean
   3
   4  Every unit residue has a period. This is Euler/Fermat transported into the
   5  δ residue layer: for `a` coprime to `N`, `a^(totient N) ≡ 1 (mod N)`, so a
   6  certified `PeriodWitness` exists. It makes the period spectrum non-vacuous: the
   7  object a period-finder searches for always exists.
   8
   9  This is existence, not cost. It says nothing about how cheaply the least period
  10  can be found; that is the open performance lane.
  11-/
  12
  13import Mathlib
  14import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodSpectrum
  15
  16namespace IndisputableMonolith
  17namespace Foundation
  18namespace PrimitiveRecognitionCalculus
  19namespace Factorization
  20
  21open DistinctionNat
  22
  23/-- The Euler exponent of `N` as an orbit position: the totient of the display. -/
  24def periodExponent (N : DistinctionNat) : DistinctionNat :=
  25  ofNat (Nat.totient N.toNat)
  26
  27theorem periodExponent_ne_zero {N : DistinctionNat} (hN2 : 2 ≤ N.toNat) :
  28    periodExponent N ≠ zero := by
  29  intro h
  30  have hh := congrArg DistinctionNat.toNat h
  31  rw [periodExponent, toNat_ofNat, toNat_zero] at hh
  32  have hpos : 0 < Nat.totient N.toNat := Nat.totient_pos.mpr (by omega)
  33  omega
  34
  35/-- Euler's theorem in the δ residue layer: a unit residue raised to the Euler
  36exponent returns to the identity residue. -/
  37theorem eulerPeriod_returns_one {N a : DistinctionNat} (hN : N ≠ zero)
  38    (ha : unitResidue N a) :
  39    sameResidue N hN (orbitPow a (periodExponent N)) one := by
  40  rw [sameResidue_iff_mod_eq, orbitPow_toNat, periodExponent, toNat_ofNat,
  41    one_toNat]
  42  have hcop : Nat.Coprime a.toNat N.toNat :=
  43    (unitResidue_iff_nat_coprime N a).mp ha
  44  exact Nat.ModEq.pow_totient hcop
  45
  46/-- Period existence: every unit residue modulo `N ≥ 2` has a certified period
  47witness, with period equal to the Euler exponent. -/
  48theorem period_exists_for_unitResidue {N a : DistinctionNat} (hN : N ≠ zero)
  49    (hN2 : 2 ≤ N.toNat) (ha : unitResidue N a) :
  50    PeriodWitness N hN a (periodExponent N) where
  51  exponent_nonzero := periodExponent_ne_zero hN2
  52  base_unit := ha
  53  returns_one := eulerPeriod_returns_one hN ha
  54
  55theorem periodWitness_nonempty_of_unitResidue {N a : DistinctionNat}
  56    (hN : N ≠ zero) (hN2 : 2 ≤ N.toNat) (ha : unitResidue N a) :
  57    Nonempty (PeriodWitness N hN a (periodExponent N)) :=
  58  ⟨period_exists_for_unitResidue hN hN2 ha⟩
  59
  60/-- Certificate for the period-existence surface. -/
  61structure PeriodExistenceCertificate : Prop where
  62  euler_period_returns_one :
  63    ∀ {N a : DistinctionNat} (hN : N ≠ zero),
  64      unitResidue N a →
  65        sameResidue N hN (orbitPow a (periodExponent N)) one
  66  period_exists :
  67    ∀ {N a : DistinctionNat} (hN : N ≠ zero), 2 ≤ N.toNat →
  68      unitResidue N a →
  69        Nonempty (PeriodWitness N hN a (periodExponent N))
  70
  71theorem period_existence_certificate : PeriodExistenceCertificate where
  72  euler_period_returns_one := by
  73    intro N a hN ha
  74    exact eulerPeriod_returns_one hN ha
  75  period_exists := by
  76    intro N a hN hN2 ha
  77    exact periodWitness_nonempty_of_unitResidue hN hN2 ha
  78
  79end Factorization
  80end PrimitiveRecognitionCalculus
  81end Foundation
  82end IndisputableMonolith
  83