IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PrimeCoordinateTransform

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/PrimeCoordinateTransform.lean
   3
   4  Final-goal interface for δ-native prime-coordinate data. This module proves
   5  that once such coordinates are supplied, factor recovery is a projection from
   6  the data. It does not claim that the transform is already δ-derived.
   7-/
   8
   9import Mathlib
  10import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PhysicalPeriodReadout
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace PrimitiveRecognitionCalculus
  15namespace Factorization
  16
  17open DistinctionNat
  18
  19/-- One prime coordinate: a prime orbit base and a nonzero exponent. -/
  20structure PrimePowerCoordinate : Type where
  21  base : DistinctionNat
  22  exponent : DistinctionNat
  23  base_prime : primeOrbit base
  24  exponent_nonzero : exponent ≠ zero
  25
  26/-- The orbit value of one prime-power coordinate. -/
  27def primePowerValue (c : PrimePowerCoordinate) : DistinctionNat :=
  28  orbitPow c.base c.exponent
  29
  30/-- Product of a list of prime-power coordinates. -/
  31def primeCoordinateProduct : List PrimePowerCoordinate → DistinctionNat
  32  | [] => one
  33  | c :: rest => primePowerValue c * primeCoordinateProduct rest
  34
  35theorem primeCoordinateProduct_nil :
  36    primeCoordinateProduct [] = one := rfl
  37
  38theorem primeCoordinateProduct_cons (c : PrimePowerCoordinate)
  39    (rest : List PrimePowerCoordinate) :
  40    primeCoordinateProduct (c :: rest) =
  41      primePowerValue c * primeCoordinateProduct rest := rfl
  42
  43/-- Prime-coordinate data for an orbit number `N`. -/
  44structure PrimeCoordinateData (N : DistinctionNat) : Type where
  45  coordinates : List PrimePowerCoordinate
  46  reconstructs : primeCoordinateProduct coordinates = N
  47
  48theorem primeCoordinateData_reconstructs {N : DistinctionNat}
  49    (data : PrimeCoordinateData N) :
  50    primeCoordinateProduct data.coordinates = N :=
  51  data.reconstructs
  52
  53theorem primeCoordinateProduct_append
  54    (xs ys : List PrimePowerCoordinate) :
  55    primeCoordinateProduct (xs ++ ys) =
  56      primeCoordinateProduct xs * primeCoordinateProduct ys := by
  57  induction xs with
  58  | nil =>
  59      simp [primeCoordinateProduct, one_mul_eq]
  60  | cons c rest ih =>
  61      simp [primeCoordinateProduct, ih]
  62      rw [mul_assoc]
  63
  64def singlePrimeCoordinateData {N : DistinctionNat}
  65    (hp : primeOrbit N) : PrimeCoordinateData N where
  66  coordinates := [{
  67    base := N
  68    exponent := one
  69    base_prime := hp
  70    exponent_nonzero := one_ne_zero
  71  }]
  72  reconstructs := by
  73    apply toNat_inj
  74    simp [primeCoordinateProduct, primePowerValue, orbitPow_toNat,
  75      one_toNat, toNat_mul]
  76
  77theorem nontrivialFactorization_of_not_primeOrbit
  78    {N : DistinctionNat}
  79    (hN0 : N ≠ zero) (hNunit : ¬ unit N)
  80    (hnot : ¬ primeOrbit N) :
  81    nontrivialFactorization N := by
  82  by_contra hfac
  83  exact hnot ⟨hN0, hNunit, hfac⟩
  84
  85theorem toNat_pos_of_ne_zero {N : DistinctionNat} (hN : N ≠ zero) :
  86    0 < N.toNat := by
  87  have hne : N.toNat ≠ 0 := by
  88    intro h
  89    apply hN
  90    apply toNat_inj
  91    rw [h, toNat_zero]
  92  omega
  93
  94theorem toNat_ne_one_of_not_unit {N : DistinctionNat}
  95    (hNunit : ¬ unit N) :
  96    N.toNat ≠ 1 := by
  97  intro h
  98  apply hNunit
  99  rw [unit_iff_toNat_eq_one]
 100  exact h
 101
 102theorem factor_left_toNat_lt_product {a b N : DistinctionNat}
 103    (ha0 : a ≠ zero) (hb0 : b ≠ zero)
 104    (hbunit : ¬ unit b) (hmul : a * b = N) :
 105    a.toNat < N.toNat := by
 106  have hapos : 0 < a.toNat := toNat_pos_of_ne_zero ha0
 107  have hbpos : 0 < b.toNat := toNat_pos_of_ne_zero hb0
 108  have hbne1 : b.toNat ≠ 1 := toNat_ne_one_of_not_unit hbunit
 109  have hbge2 : 2 ≤ b.toNat := by omega
 110  have hmulNat : a.toNat * b.toNat = N.toNat := by
 111    have h := congrArg DistinctionNat.toNat hmul
 112    simpa [toNat_mul] using h
 113  nlinarith
 114
 115theorem factor_right_toNat_lt_product {a b N : DistinctionNat}
 116    (ha0 : a ≠ zero) (hb0 : b ≠ zero)
 117    (haunit : ¬ unit a) (hmul : a * b = N) :
 118    b.toNat < N.toNat := by
 119  rw [mul_comm] at hmul
 120  exact factor_left_toNat_lt_product hb0 ha0 haunit hmul
 121
 122/-- A claimed δ-prime-coordinate transform. This is the bold goal object. -/
 123def DeltaPrimeCoordinateTransform : Type :=
 124  ∀ N : DistinctionNat, N ≠ zero → ¬ unit N → PrimeCoordinateData N
 125
 126/-- A weaker transform that is allowed to rely on a named external readout. -/
 127structure AssistedPrimeCoordinateTransform : Type where
 128  commitmentName : String
 129  transform :
 130    ∀ N : DistinctionNat, N ≠ zero → ¬ unit N → PrimeCoordinateData N
 131
 132/-! ## Classical factorization transport back into δ -/
 133
 134theorem primeOrbit_ofNat_of_natPrime {p : Nat} (hp : Nat.Prime p) :
 135    primeOrbit (ofNat p) := by
 136  rw [primeOrbit_iff_toNat_no_nontrivial_factor, toNat_ofNat]
 137  refine ⟨hp.ne_zero, hp.ne_one, ?_⟩
 138  rintro ⟨a, b, ha0, _hb0, ha1, hb1, hmul⟩
 139  have hadvd : a ∣ p := ⟨b, hmul.symm⟩
 140  rcases hp.eq_one_or_self_of_dvd a hadvd with haeq | haeq
 141  · exact ha1 haeq
 142  · have hb : b = 1 := by
 143      rw [haeq] at hmul
 144      nlinarith [hmul, hp.pos]
 145    exact hb1 hb
 146
 147def primePowerCoordinateOfNatPrime (p : Nat) (hp : Nat.Prime p) :
 148    PrimePowerCoordinate where
 149  base := ofNat p
 150  exponent := one
 151  base_prime := primeOrbit_ofNat_of_natPrime hp
 152  exponent_nonzero := one_ne_zero
 153
 154theorem primePowerValue_of_natPrime_toNat (p : Nat) (hp : Nat.Prime p) :
 155    (primePowerValue (primePowerCoordinateOfNatPrime p hp)).toNat = p := by
 156  simp [primePowerValue, primePowerCoordinateOfNatPrime, orbitPow_toNat,
 157    one_toNat, toNat_ofNat]
 158
 159def primeCoordinatesFromNatList :
 160    (L : List Nat) → (∀ p ∈ L, Nat.Prime p) → List PrimePowerCoordinate
 161  | [], _ => []
 162  | p :: rest, hprime =>
 163      primePowerCoordinateOfNatPrime p (hprime p (by simp)) ::
 164        primeCoordinatesFromNatList rest (by
 165          intro q hq
 166          exact hprime q (by simp [hq]))
 167
 168theorem primeCoordinateProduct_fromNatList_toNat
 169    (L : List Nat) (hprime : ∀ p ∈ L, Nat.Prime p) :
 170    (primeCoordinateProduct (primeCoordinatesFromNatList L hprime)).toNat =
 171      L.prod := by
 172  induction L with
 173  | nil =>
 174      simp [primeCoordinatesFromNatList, primeCoordinateProduct, one_toNat]
 175  | cons p rest ih =>
 176      simp [primeCoordinatesFromNatList, primeCoordinateProduct,
 177        primePowerValue_of_natPrime_toNat, toNat_mul, ih]
 178
 179def natPrimeFactorCoordinates (n : Nat) : List PrimePowerCoordinate :=
 180  primeCoordinatesFromNatList n.primeFactorsList (by
 181    intro p hp
 182    exact Nat.prime_of_mem_primeFactorsList hp)
 183
 184theorem primeCoordinateProduct_natPrimeFactorCoordinates_toNat (n : Nat) :
 185    (primeCoordinateProduct (natPrimeFactorCoordinates n)).toNat =
 186      n.primeFactorsList.prod := by
 187  unfold natPrimeFactorCoordinates
 188  exact primeCoordinateProduct_fromNatList_toNat n.primeFactorsList (by
 189    intro p hp
 190    exact Nat.prime_of_mem_primeFactorsList hp)
 191
 192private theorem toNat_ne_zero_of_ne_zero {N : DistinctionNat} (hN : N ≠ zero) :
 193    N.toNat ≠ 0 := by
 194  intro h
 195  apply hN
 196  apply toNat_inj
 197  rw [h, toNat_zero]
 198
 199/-- A theorem-level δ prime-coordinate transform obtained by transporting
 200Mathlib's canonical `Nat.primeFactorsList` through the established δ/Nat
 201display equivalence. This closes the transform as a classical transport
 202theorem; it is not a new fast factoring algorithm. -/
 203def deltaPrimeCoordinateTransform_classicalTransport :
 204    DeltaPrimeCoordinateTransform := by
 205  intro N hN0 _hNunit
 206  refine {
 207    coordinates := natPrimeFactorCoordinates N.toNat
 208    reconstructs := ?_
 209  }
 210  apply toNat_inj
 211  rw [primeCoordinateProduct_natPrimeFactorCoordinates_toNat]
 212  exact Nat.prod_primeFactorsList (toNat_ne_zero_of_ne_zero hN0)
 213
 214theorem deltaPrimeCoordinateTransform_exists :
 215    Nonempty DeltaPrimeCoordinateTransform :=
 216  ⟨deltaPrimeCoordinateTransform_classicalTransport⟩
 217
 218/-! ## Native-choice δ transform by prime/factorization descent -/
 219
 220theorem nativePrimeCoordinateData_exists :
 221    ∀ N : DistinctionNat, N ≠ zero → ¬ unit N →
 222      Nonempty (PrimeCoordinateData N) := by
 223  have hmain :
 224      ∀ n : Nat, ∀ N : DistinctionNat,
 225        N.toNat = n → N ≠ zero → ¬ unit N →
 226          Nonempty (PrimeCoordinateData N) := by
 227    intro n
 228    induction n using Nat.strong_induction_on with
 229    | h n ih =>
 230        intro N hNnat hN0 hNunit
 231        by_cases hp : primeOrbit N
 232        · exact ⟨singlePrimeCoordinateData hp⟩
 233        · have hfac := nontrivialFactorization_of_not_primeOrbit
 234            hN0 hNunit hp
 235          rcases hfac with ⟨a, b, ha0, hb0, haunit, hbunit, hmul⟩
 236          have ha_lt_n : a.toNat < n := by
 237            rw [← hNnat]
 238            exact factor_left_toNat_lt_product ha0 hb0 hbunit hmul
 239          have hb_lt_n : b.toNat < n := by
 240            rw [← hNnat]
 241            exact factor_right_toNat_lt_product ha0 hb0 haunit hmul
 242          rcases ih a.toNat ha_lt_n a rfl ha0 haunit with ⟨adata⟩
 243          rcases ih b.toNat hb_lt_n b rfl hb0 hbunit with ⟨bdata⟩
 244          refine ⟨{
 245            coordinates := adata.coordinates ++ bdata.coordinates
 246            reconstructs := ?_
 247          }⟩
 248          rw [primeCoordinateProduct_append, adata.reconstructs,
 249            bdata.reconstructs, hmul]
 250  intro N hN0 hNunit
 251  exact hmain N.toNat N rfl hN0 hNunit
 252
 253/-- Noncomputable native-choice transform: it uses the δ-native
 254`primeOrbit/nontrivialFactorization` split and well-founded descent. -/
 255noncomputable def deltaPrimeCoordinateTransform_nativeChoice :
 256    DeltaPrimeCoordinateTransform := by
 257  intro N hN0 hNunit
 258  exact Classical.choice (nativePrimeCoordinateData_exists N hN0 hNunit)
 259
 260theorem deltaPrimeCoordinateTransform_nativeChoice_exists :
 261    Nonempty DeltaPrimeCoordinateTransform :=
 262  ⟨deltaPrimeCoordinateTransform_nativeChoice⟩
 263
 264theorem primeCoordinateData_nonempty_of_nonunit {N : DistinctionNat}
 265    (data : PrimeCoordinateData N) (hNunit : ¬ unit N) :
 266    data.coordinates ≠ [] := by
 267  intro hnil
 268  have hN : one = N := by
 269    simpa [primeCoordinateProduct, hnil] using data.reconstructs
 270  apply hNunit
 271  unfold unit
 272  exact hN.symm
 273
 274theorem base_divides_orbitPow_of_exponent_nonzero
 275    (p e : DistinctionNat) (he : e ≠ zero) :
 276    divides p (orbitPow p e) := by
 277  cases e with
 278  | zero =>
 279      exact False.elim (he rfl)
 280  | succ k =>
 281      refine ⟨orbitPow p k, ?_⟩
 282      rw [orbitPow_succ, mul_comm]
 283
 284/-- The first coordinate in a coordinate list gives a prime divisor of the
 285reconstructed number. This is the formal version of "factor recovery is a
 286coordinate projection." -/
 287theorem first_coordinate_prime_divisor {N : DistinctionNat}
 288    (c : PrimePowerCoordinate) (rest : List PrimePowerCoordinate)
 289    (data : PrimeCoordinateData N)
 290    (hcoords : data.coordinates = c :: rest) :
 291    primeOrbit c.base ∧ divides c.base N := by
 292  constructor
 293  · exact c.base_prime
 294  · have hpow : divides c.base (primePowerValue c) :=
 295      base_divides_orbitPow_of_exponent_nonzero c.base c.exponent
 296        c.exponent_nonzero
 297    have hprod : divides (primePowerValue c)
 298        (primePowerValue c * primeCoordinateProduct rest) :=
 299      divides_mul_right (primePowerValue c) (primeCoordinateProduct rest)
 300    have hdivProduct : divides c.base
 301        (primePowerValue c * primeCoordinateProduct rest) :=
 302      divides_trans hpow hprod
 303    rcases hdivProduct with ⟨k, hk⟩
 304    refine ⟨k, ?_⟩
 305    rw [hk]
 306    rw [← primeCoordinateProduct_cons]
 307    rw [← hcoords]
 308    exact data.reconstructs
 309
 310/-- A δ-prime-coordinate transform makes factor recovery immediate for every
 311nonzero nonunit orbit number. -/
 312theorem deltaPrimeCoordinateTransform_recovers_prime_divisor
 313    (T : DeltaPrimeCoordinateTransform) :
 314    ∀ N : DistinctionNat, N ≠ zero → ¬ unit N →
 315      ∃ p : DistinctionNat, primeOrbit p ∧ divides p N := by
 316  intro N hN0 hNunit
 317  let data := T N hN0 hNunit
 318  have hnonempty := primeCoordinateData_nonempty_of_nonunit data hNunit
 319  cases hcoords : data.coordinates with
 320  | nil =>
 321      exact False.elim (hnonempty hcoords)
 322  | cons c rest =>
 323      exact ⟨c.base, first_coordinate_prime_divisor c rest data hcoords⟩
 324
 325/-- Certificate for the prime-coordinate transform interface. -/
 326structure PrimeCoordinateTransformCertificate : Prop where
 327  data_reconstructs :
 328    ∀ {N : DistinctionNat} (data : PrimeCoordinateData N),
 329      primeCoordinateProduct data.coordinates = N
 330  classical_transport_exists :
 331    Nonempty DeltaPrimeCoordinateTransform
 332  native_choice_exists :
 333    Nonempty DeltaPrimeCoordinateTransform
 334  nonunit_data_nonempty :
 335    ∀ {N : DistinctionNat} (data : PrimeCoordinateData N),
 336      ¬ unit N → data.coordinates ≠ []
 337  delta_transform_recovers_prime_divisor :
 338    DeltaPrimeCoordinateTransform →
 339      ∀ N : DistinctionNat, N ≠ zero → ¬ unit N →
 340        ∃ p : DistinctionNat, primeOrbit p ∧ divides p N
 341
 342theorem prime_coordinate_transform_certificate :
 343    PrimeCoordinateTransformCertificate where
 344  data_reconstructs := by
 345    intro N data
 346    exact primeCoordinateData_reconstructs data
 347  classical_transport_exists := deltaPrimeCoordinateTransform_exists
 348  native_choice_exists := deltaPrimeCoordinateTransform_nativeChoice_exists
 349  nonunit_data_nonempty := by
 350    intro N data hNunit
 351    exact primeCoordinateData_nonempty_of_nonunit data hNunit
 352  delta_transform_recovers_prime_divisor := by
 353    intro T N hN0 hNunit
 354    exact deltaPrimeCoordinateTransform_recovers_prime_divisor T N hN0 hNunit
 355
 356end Factorization
 357end PrimitiveRecognitionCalculus
 358end Foundation
 359end IndisputableMonolith
 360