IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodSpectrum

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/PeriodSpectrum.lean
   3
   4  Multiplicative powers and certified period witnesses for unit residues.
   5  This file does not assert a fast period-finder. It only defines the witness
   6  object that any classical, quantum, or physical readout must return.
   7-/
   8
   9import Mathlib
  10import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.UnitGroup
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace PrimitiveRecognitionCalculus
  15namespace Factorization
  16
  17open DistinctionNat
  18
  19/-- δ-native exponentiation by an orbit exponent. -/
  20def orbitPow (a : DistinctionNat) : DistinctionNat → DistinctionNat
  21  | zero => one
  22  | succ k => orbitPow a k * a
  23
  24theorem orbitPow_zero (a : DistinctionNat) :
  25    orbitPow a zero = one := rfl
  26
  27theorem orbitPow_succ (a k : DistinctionNat) :
  28    orbitPow a (succ k) = orbitPow a k * a := rfl
  29
  30theorem orbitPow_toNat (a k : DistinctionNat) :
  31    (orbitPow a k).toNat = a.toNat ^ k.toNat := by
  32  induction k with
  33  | zero =>
  34      simp [orbitPow, one_toNat]
  35  | succ k ih =>
  36      rw [orbitPow_succ, toNat_mul, ih, toNat_succ]
  37      exact Nat.pow_succ a.toNat k.toNat
  38
  39theorem orbitPow_unitResidue {N a : DistinctionNat}
  40    (ha : unitResidue N a) (k : DistinctionNat) :
  41    unitResidue N (orbitPow a k) := by
  42  rw [unitResidue_iff_nat_coprime]
  43  rw [orbitPow_toNat]
  44  exact unitResidue_pow_closed ha k.toNat
  45
  46/-- A certified period witness. Minimality is optional at the interface; the
  47essential output is a nonzero exponent that returns the unit residue to `1`. -/
  48structure PeriodWitness (N : DistinctionNat) (hN : N ≠ zero)
  49    (a r : DistinctionNat) : Prop where
  50  exponent_nonzero : r ≠ zero
  51  base_unit : unitResidue N a
  52  returns_one : sameResidue N hN (orbitPow a r) one
  53
  54/-- A period witness plus a proper divisor it exposes. The divisor may come
  55from the usual `gcd(a^(r/2)-1,N)` route, but this structure deliberately stores
  56the certificate rather than pretending the readout itself is already derived. -/
  57structure ProperDivisorFromPeriod (N : DistinctionNat) (hN : N ≠ zero)
  58    (a r : DistinctionNat) : Type where
  59  period : PeriodWitness N hN a r
  60  divisor : DistinctionNat
  61  divisor_nonzero : divisor ≠ zero
  62  divisor_nonunit : ¬ unit divisor
  63  divisor_not_modulus : divisor ≠ N
  64  divisor_divides : divides divisor N
  65
  66/-- Once a period readout has supplied a proper divisor certificate, the
  67δ-native divisibility layer gives a nontrivial factorization. -/
  68theorem period_divisor_to_nontrivialFactorization {N a r : DistinctionNat}
  69    {hN : N ≠ zero}
  70    (w : ProperDivisorFromPeriod N hN a r) :
  71    nontrivialFactorization N := by
  72  exact nontrivialFactorization_of_proper_divisor hN
  73    w.divisor_nonzero w.divisor_nonunit w.divisor_not_modulus
  74    w.divisor_divides
  75
  76/-- Certificate for the period-spectrum interface. -/
  77structure PeriodSpectrumCertificate : Prop where
  78  pow_display :
  79    ∀ a k : DistinctionNat, (orbitPow a k).toNat = a.toNat ^ k.toNat
  80  pow_preserves_unit :
  81    ∀ {N a : DistinctionNat},
  82      unitResidue N a → ∀ k : DistinctionNat, unitResidue N (orbitPow a k)
  83  period_divisor_extracts_factorization :
  84    ∀ {N a r : DistinctionNat} {hN : N ≠ zero},
  85      ProperDivisorFromPeriod N hN a r → nontrivialFactorization N
  86
  87theorem period_spectrum_certificate : PeriodSpectrumCertificate where
  88  pow_display := orbitPow_toNat
  89  pow_preserves_unit := by
  90    intro N a ha k
  91    exact orbitPow_unitResidue ha k
  92  period_divisor_extracts_factorization := by
  93    intro N a r hN w
  94    exact period_divisor_to_nontrivialFactorization w
  95
  96end Factorization
  97end PrimitiveRecognitionCalculus
  98end Foundation
  99end IndisputableMonolith
 100