IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.CoordinateUniqueness

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/CoordinateUniqueness.lean
   3
   4  Fundamental theorem of arithmetic in δ prime coordinates. This module proves
   5  that the prime-coordinate readout of an orbit number is unique (any two
   6  reconstructions induce the same Nat factorization), that every coordinate base
   7  is a genuine prime divisor, and that every prime divisor appears as a
   8  coordinate base. Together these say factor recovery is list membership on the
   9  readout, not a search.
  10
  11  This is theorem content about the structure of the readout. It makes no claim
  12  about the cost of producing the readout; both transforms in
  13  `PrimeCoordinateTransform` remain search-grade.
  14-/
  15
  16import Mathlib
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PrimeCoordinateTransform
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace PrimitiveRecognitionCalculus
  22namespace Factorization
  23
  24open DistinctionNat
  25
  26/-! ## A prime orbit displays as a Nat prime -/
  27
  28/-- The δ-native `primeOrbit` predicate forces the orbit display to be a genuine
  29Nat prime. This is the bridge that lets the readout inherit `Nat.factorization`
  30structure. -/
  31theorem natPrime_toNat_of_primeOrbit {p : DistinctionNat} (hp : primeOrbit p) :
  32    Nat.Prime p.toNat := by
  33  rw [primeOrbit_iff_toNat_no_nontrivial_factor] at hp
  34  obtain ⟨h0, h1, hnf⟩ := hp
  35  rw [Nat.prime_def_lt]
  36  refine ⟨by omega, ?_⟩
  37  intro m hmlt hmdvd
  38  rcases hmdvd with ⟨k, hk⟩
  39  by_contra hm1
  40  apply hnf
  41  refine ⟨m, k, ?_, ?_, hm1, ?_, hk.symm⟩
  42  · intro hm0
  43    rw [hm0, Nat.zero_mul] at hk
  44    exact h0 hk
  45  · intro hk0
  46    rw [hk0, Nat.mul_zero] at hk
  47    exact h0 hk
  48  · intro hk1
  49    rw [hk1, Nat.mul_one] at hk
  50    omega
  51
  52/-- The converse bridge: a Nat prime display lifts back to a δ prime orbit. -/
  53theorem primeOrbit_of_natPrime_toNat {p : DistinctionNat}
  54    (h : Nat.Prime p.toNat) : primeOrbit p := by
  55  have hp := primeOrbit_ofNat_of_natPrime h
  56  rwa [ofNat_toNat] at hp
  57
  58/-- δ primality is exactly Nat primality of the display. -/
  59theorem primeOrbit_iff_natPrime_toNat (p : DistinctionNat) :
  60    primeOrbit p ↔ Nat.Prime p.toNat :=
  61  ⟨natPrime_toNat_of_primeOrbit, primeOrbit_of_natPrime_toNat⟩
  62
  63/-- Consequently `primeOrbit` is decidable: δ primality is machine-checkable. -/
  64instance : DecidablePred (primeOrbit : DistinctionNat → Prop) := fun p =>
  65  decidable_of_iff (Nat.Prime p.toNat) (primeOrbit_iff_natPrime_toNat p).symm
  66
  67/-! ## The induced Nat factorization of a coordinate list -/
  68
  69/-- The Nat factorization read off a coordinate list: each prime-power
  70coordinate `base^exponent` contributes `exponent` to the prime `base`. -/
  71noncomputable def coordinateFactorization
  72    (coords : List PrimePowerCoordinate) : Nat →₀ Nat :=
  73  (coords.map fun c => Finsupp.single c.base.toNat c.exponent.toNat).sum
  74
  75theorem coordinateFactorization_nil :
  76    coordinateFactorization [] = 0 := by
  77  simp [coordinateFactorization]
  78
  79theorem coordinateFactorization_cons (c : PrimePowerCoordinate)
  80    (rest : List PrimePowerCoordinate) :
  81    coordinateFactorization (c :: rest) =
  82      Finsupp.single c.base.toNat c.exponent.toNat +
  83        coordinateFactorization rest := by
  84  simp [coordinateFactorization, List.map_cons, List.sum_cons]
  85
  86theorem primeCoordinateProduct_toNat_ne_zero
  87    (coords : List PrimePowerCoordinate) :
  88    (primeCoordinateProduct coords).toNat ≠ 0 := by
  89  induction coords with
  90  | nil => simp [primeCoordinateProduct, one_toNat]
  91  | cons c rest ih =>
  92      rw [primeCoordinateProduct_cons, toNat_mul]
  93      have hbpos : 0 < c.base.toNat := (natPrime_toNat_of_primeOrbit c.base_prime).pos
  94      have hc : (primePowerValue c).toNat ≠ 0 := by
  95        rw [primePowerValue, orbitPow_toNat]
  96        exact pow_ne_zero _ hbpos.ne'
  97      exact Nat.mul_ne_zero hc ih
  98
  99/-- The factorization read off a coordinate list equals the canonical Nat
 100factorization of the reconstructed product. -/
 101theorem coordinateFactorization_eq_factorization_product
 102    (coords : List PrimePowerCoordinate) :
 103    coordinateFactorization coords =
 104      Nat.factorization (primeCoordinateProduct coords).toNat := by
 105  induction coords with
 106  | nil =>
 107      rw [coordinateFactorization_nil, primeCoordinateProduct_nil, one_toNat,
 108        Nat.factorization_one]
 109  | cons c rest ih =>
 110      have hbpos : 0 < c.base.toNat :=
 111        (natPrime_toNat_of_primeOrbit c.base_prime).pos
 112      have hc : (primePowerValue c).toNat ≠ 0 := by
 113        rw [primePowerValue, orbitPow_toNat]
 114        exact pow_ne_zero _ hbpos.ne'
 115      have hr : (primeCoordinateProduct rest).toNat ≠ 0 :=
 116        primeCoordinateProduct_toNat_ne_zero rest
 117      have hpf : Nat.factorization (primePowerValue c).toNat
 118          = Finsupp.single c.base.toNat c.exponent.toNat := by
 119        rw [primePowerValue, orbitPow_toNat, Nat.factorization_pow,
 120          (natPrime_toNat_of_primeOrbit c.base_prime).factorization,
 121          Finsupp.smul_single, smul_eq_mul, mul_one]
 122      rw [coordinateFactorization_cons, ih, primeCoordinateProduct_cons,
 123        toNat_mul, Nat.factorization_mul hc hr, hpf]
 124
 125/-- Specialized to reconstruction data: the readout of `N` is exactly the
 126canonical factorization of `N`'s display. -/
 127theorem coordinateFactorization_eq_factorization_of_data {N : DistinctionNat}
 128    (data : PrimeCoordinateData N) :
 129    coordinateFactorization data.coordinates = Nat.factorization N.toNat := by
 130  rw [coordinateFactorization_eq_factorization_product, data.reconstructs]
 131
 132/-- Fundamental theorem of arithmetic in δ coordinates: any two prime-coordinate
 133reconstructions of the same orbit number induce the same prime factorization.
 134The readout is unique as a multiset of prime powers. -/
 135theorem primeCoordinateData_factorization_unique {N : DistinctionNat}
 136    (d₁ d₂ : PrimeCoordinateData N) :
 137    coordinateFactorization d₁.coordinates =
 138      coordinateFactorization d₂.coordinates := by
 139  rw [coordinateFactorization_eq_factorization_of_data,
 140    coordinateFactorization_eq_factorization_of_data]
 141
 142/-! ## Soundness: every coordinate base is a prime divisor -/
 143
 144theorem mem_coordinate_divides_product (c : PrimePowerCoordinate) :
 145    ∀ (coords : List PrimePowerCoordinate), c ∈ coords →
 146      divides (primePowerValue c) (primeCoordinateProduct coords) := by
 147  intro coords
 148  induction coords with
 149  | nil =>
 150      intro hmem
 151      simp at hmem
 152  | cons d rest ih =>
 153      intro hmem
 154      rw [primeCoordinateProduct_cons]
 155      rcases List.mem_cons.mp hmem with h | h
 156      · subst h
 157        exact divides_mul_right _ _
 158      · exact divides_trans (ih h) (divides_mul_left _ _)
 159
 160/-- Every coordinate base is a prime orbit that divides `N`. Reading a base off
 161the list is a sound factor projection. -/
 162theorem coordinate_base_is_prime_divisor {N : DistinctionNat}
 163    (data : PrimeCoordinateData N) (c : PrimePowerCoordinate)
 164    (hmem : c ∈ data.coordinates) :
 165    primeOrbit c.base ∧ divides c.base N := by
 166  refine ⟨c.base_prime, ?_⟩
 167  have h1 : divides c.base (primePowerValue c) :=
 168    base_divides_orbitPow_of_exponent_nonzero c.base c.exponent c.exponent_nonzero
 169  have h2 : divides (primePowerValue c) (primeCoordinateProduct data.coordinates) :=
 170    mem_coordinate_divides_product c data.coordinates hmem
 171  rw [← data.reconstructs]
 172  exact divides_trans h1 h2
 173
 174/-! ## Completeness: every prime divisor appears as a coordinate base -/
 175
 176theorem mem_support_coordinateFactorization :
 177    ∀ (coords : List PrimePowerCoordinate) {x : Nat},
 178      x ∈ (coordinateFactorization coords).support →
 179        ∃ c ∈ coords, c.base.toNat = x := by
 180  intro coords
 181  induction coords with
 182  | nil =>
 183      intro x hx
 184      rw [coordinateFactorization_nil] at hx
 185      simp at hx
 186  | cons c rest ih =>
 187      intro x hx
 188      rw [coordinateFactorization_cons] at hx
 189      have hsub := Finsupp.support_add hx
 190      rw [Finset.mem_union] at hsub
 191      rcases hsub with h | h
 192      · have hx1 := Finsupp.support_single_subset h
 193        rw [Finset.mem_singleton] at hx1
 194        exact ⟨c, List.mem_cons.mpr (Or.inl rfl), hx1.symm⟩
 195      · rcases ih h with ⟨d, hd, hdx⟩
 196        exact ⟨d, List.mem_cons.mpr (Or.inr hd), hdx⟩
 197
 198/-- Every prime orbit dividing `N` appears as a coordinate base. The readout is
 199a complete factor oracle. -/
 200theorem prime_divisor_is_coordinate_base {N : DistinctionNat}
 201    (data : PrimeCoordinateData N) (hN0 : N ≠ zero)
 202    {q : DistinctionNat} (hq : primeOrbit q) (hdvd : divides q N) :
 203    ∃ c ∈ data.coordinates, c.base = q := by
 204  have hqp : Nat.Prime q.toNat := natPrime_toNat_of_primeOrbit hq
 205  have hdvdNat : q.toNat ∣ N.toNat := (divides_iff_toNat_dvd q N).mp hdvd
 206  have hN0Nat : N.toNat ≠ 0 := by
 207    intro h
 208    apply hN0
 209    apply toNat_inj
 210    rw [h, toNat_zero]
 211  have hmemPF : q.toNat ∈ N.toNat.primeFactors := by
 212    rw [Nat.mem_primeFactors]
 213    exact ⟨hqp, hdvdNat, hN0Nat⟩
 214  have hsupp : q.toNat ∈ (Nat.factorization N.toNat).support := by
 215    rwa [Nat.support_factorization]
 216  rw [← coordinateFactorization_eq_factorization_of_data data] at hsupp
 217  rcases mem_support_coordinateFactorization data.coordinates hsupp with ⟨c, hc, hcq⟩
 218  exact ⟨c, hc, toNat_inj hcq⟩
 219
 220/-- The headline readout equivalence: for a prime orbit `q`, deciding whether
 221`q` divides `N` is exactly checking whether `q` is one of the coordinate bases.
 222Factor recovery is list membership on the readout, not a search. -/
 223theorem primeOrbit_divides_iff_mem_coordinate_bases {N : DistinctionNat}
 224    (data : PrimeCoordinateData N) (hN0 : N ≠ zero)
 225    {q : DistinctionNat} (hq : primeOrbit q) :
 226    divides q N ↔ ∃ c ∈ data.coordinates, c.base = q := by
 227  constructor
 228  · intro hdvd
 229    exact prime_divisor_is_coordinate_base data hN0 hq hdvd
 230  · rintro ⟨c, hc, hcq⟩
 231    rw [← hcq]
 232    exact (coordinate_base_is_prime_divisor data c hc).2
 233
 234/-! ## The computable transport readout is the canonical factorization -/
 235
 236/-- The computable classical-transport transform produces, for every nonzero
 237nonunit orbit number, a readout whose induced factorization is the canonical
 238`Nat.factorization`. Combined with uniqueness, this is a computable δ transform
 239whose output is the canonical prime decomposition. -/
 240theorem classicalTransport_readout_is_canonical
 241    (N : DistinctionNat) (hN0 : N ≠ zero) (hNunit : ¬ unit N) :
 242    coordinateFactorization
 243        (deltaPrimeCoordinateTransform_classicalTransport N hN0 hNunit).coordinates
 244      = Nat.factorization N.toNat :=
 245  coordinateFactorization_eq_factorization_of_data _
 246
 247/-- Certificate for the coordinate-uniqueness layer. -/
 248structure CoordinateUniquenessCertificate : Prop where
 249  prime_orbit_displays_natPrime :
 250    ∀ {p : DistinctionNat}, primeOrbit p → Nat.Prime p.toNat
 251  prime_orbit_iff_natPrime :
 252    ∀ p : DistinctionNat, primeOrbit p ↔ Nat.Prime p.toNat
 253  factorization_of_data :
 254    ∀ {N : DistinctionNat} (data : PrimeCoordinateData N),
 255      coordinateFactorization data.coordinates = Nat.factorization N.toNat
 256  factorization_unique :
 257    ∀ {N : DistinctionNat} (d₁ d₂ : PrimeCoordinateData N),
 258      coordinateFactorization d₁.coordinates =
 259        coordinateFactorization d₂.coordinates
 260  coordinate_base_sound :
 261    ∀ {N : DistinctionNat} (data : PrimeCoordinateData N)
 262      (c : PrimePowerCoordinate),
 263      c ∈ data.coordinates → primeOrbit c.base ∧ divides c.base N
 264  readout_complete :
 265    ∀ {N : DistinctionNat} (data : PrimeCoordinateData N), N ≠ zero →
 266      ∀ {q : DistinctionNat}, primeOrbit q →
 267        (divides q N ↔ ∃ c ∈ data.coordinates, c.base = q)
 268
 269theorem coordinate_uniqueness_certificate : CoordinateUniquenessCertificate where
 270  prime_orbit_displays_natPrime := by
 271    intro p hp
 272    exact natPrime_toNat_of_primeOrbit hp
 273  prime_orbit_iff_natPrime := primeOrbit_iff_natPrime_toNat
 274  factorization_of_data := by
 275    intro N data
 276    exact coordinateFactorization_eq_factorization_of_data data
 277  factorization_unique := by
 278    intro N d₁ d₂
 279    exact primeCoordinateData_factorization_unique d₁ d₂
 280  coordinate_base_sound := by
 281    intro N data c hmem
 282    exact coordinate_base_is_prime_divisor data c hmem
 283  readout_complete := by
 284    intro N data hN0 q hq
 285    exact primeOrbit_divides_iff_mem_coordinate_bases data hN0 hq
 286
 287end Factorization
 288end PrimitiveRecognitionCalculus
 289end Foundation
 290end IndisputableMonolith
 291