IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitDivisibility

   1/-
   2  PrimitiveRecognitionCalculus/OrbitDivisibility.lean
   3
   4  Round-trip sources:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6    δ/PRC_Structural_Brainstorm_20260527.html
   7
   8  Spec anchors:
   9    Build Order step 2: divisibility, units, factorization, and primality on
  10    orbit positions.
  11
  12  Strength: δ-only for definitions. Nat divisibility and Nat arithmetic appear
  13  only in verifier transport theorems.
  14-/
  15
  16import Mathlib
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitArithmetic
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace PrimitiveRecognitionCalculus
  22namespace DistinctionNat
  23
  24/-! ## Native divisibility on finite δ-orbit positions -/
  25
  26/-- The multiplicative unit orbit position. -/
  27def one : DistinctionNat :=
  28  succ zero
  29
  30@[simp] theorem one_toNat :
  31    one.toNat = 1 := by
  32  rfl
  33
  34theorem one_ne_zero :
  35    one ≠ zero := by
  36  intro h
  37  exact zero_ne_succ zero h.symm
  38
  39theorem mul_one_eq (a : DistinctionNat) :
  40    a * one = a := by
  41  unfold one
  42  rw [mul_succ_eq, mul_zero_eq, zero_add_eq]
  43
  44theorem one_mul_eq (a : DistinctionNat) :
  45    one * a = a := by
  46  rw [mul_comm, mul_one_eq]
  47
  48theorem mul_assoc (a b c : DistinctionNat) :
  49    (a * b) * c = a * (b * c) := by
  50  apply toNat_inj
  51  rw [toNat_mul, toNat_mul, toNat_mul, toNat_mul]
  52  exact Nat.mul_assoc a.toNat b.toNat c.toNat
  53
  54/-- Native orbit divisibility: `a` divides `b` when multiplying `a` by another
  55orbit position yields `b`. -/
  56def divides (a b : DistinctionNat) : Prop :=
  57  ∃ k : DistinctionNat, a * k = b
  58
  59/-- Native unit predicate. In the finite δ-orbit, the only multiplicative unit
  60is the one-step orbit. -/
  61def unit (a : DistinctionNat) : Prop :=
  62  a = one
  63
  64/-- Native nontrivial factorization. Both factors must be nonzero and non-unit. -/
  65def nontrivialFactorization (n : DistinctionNat) : Prop :=
  66  ∃ a b : DistinctionNat,
  67    a ≠ zero ∧ b ≠ zero ∧ ¬ unit a ∧ ¬ unit b ∧ a * b = n
  68
  69/-- Native prime orbit position: nonzero, non-unit, and with no nontrivial
  70factorization. -/
  71def primeOrbit (p : DistinctionNat) : Prop :=
  72  p ≠ zero ∧ ¬ unit p ∧ ¬ nontrivialFactorization p
  73
  74theorem divides_refl (a : DistinctionNat) :
  75    divides a a := by
  76  exact ⟨one, mul_one_eq a⟩
  77
  78theorem divides_zero (a : DistinctionNat) :
  79    divides a zero := by
  80  exact ⟨zero, mul_zero_eq a⟩
  81
  82theorem one_divides (a : DistinctionNat) :
  83    divides one a := by
  84  exact ⟨a, one_mul_eq a⟩
  85
  86theorem divides_trans {a b c : DistinctionNat}
  87    (hab : divides a b) (hbc : divides b c) :
  88    divides a c := by
  89  rcases hab with ⟨m, hm⟩
  90  rcases hbc with ⟨n, hn⟩
  91  refine ⟨m * n, ?_⟩
  92  rw [← mul_assoc, hm, hn]
  93
  94theorem divides_mul_right (a b : DistinctionNat) :
  95    divides a (a * b) := by
  96  exact ⟨b, rfl⟩
  97
  98theorem divides_mul_left (a b : DistinctionNat) :
  99    divides b (a * b) := by
 100  refine ⟨a, ?_⟩
 101  rw [mul_comm]
 102
 103theorem zero_divides_iff_eq_zero (a : DistinctionNat) :
 104    divides zero a ↔ a = zero := by
 105  constructor
 106  · intro h
 107    rcases h with ⟨k, hk⟩
 108    rw [zero_mul_eq] at hk
 109    exact hk.symm
 110  · intro h
 111    rw [h]
 112    exact divides_zero zero
 113
 114/-- Divisibility is native, but it displays as Nat divisibility. -/
 115theorem divides_iff_toNat_dvd (a b : DistinctionNat) :
 116    divides a b ↔ a.toNat ∣ b.toNat := by
 117  constructor
 118  · intro h
 119    rcases h with ⟨k, hk⟩
 120    refine ⟨k.toNat, ?_⟩
 121    have hnat := congrArg DistinctionNat.toNat hk
 122    rw [toNat_mul] at hnat
 123    exact hnat.symm
 124  · intro h
 125    rcases h with ⟨k, hk⟩
 126    refine ⟨ofNat k, ?_⟩
 127    apply toNat_inj
 128    rw [toNat_mul, toNat_ofNat]
 129    exact hk.symm
 130
 131theorem unit_iff_toNat_eq_one (a : DistinctionNat) :
 132    unit a ↔ a.toNat = 1 := by
 133  constructor
 134  · intro h
 135    unfold unit at h
 136    rw [h, one_toNat]
 137  · intro h
 138    unfold unit
 139    apply toNat_inj
 140    rw [h, one_toNat]
 141
 142theorem divides_one_iff_unit (a : DistinctionNat) :
 143    divides a one ↔ unit a := by
 144  rw [divides_iff_toNat_dvd, unit_iff_toNat_eq_one, one_toNat]
 145  exact Nat.dvd_one
 146
 147theorem unit_of_divides_unit {a b : DistinctionNat}
 148    (hb : unit b) (hdiv : divides a b) :
 149    unit a := by
 150  rw [unit_iff_toNat_eq_one] at hb ⊢
 151  have hnat := (divides_iff_toNat_dvd a b).mp hdiv
 152  rw [hb] at hnat
 153  exact Nat.dvd_one.mp hnat
 154
 155theorem divides_antisymm {a b : DistinctionNat}
 156    (hab : divides a b) (hba : divides b a) :
 157    a = b := by
 158  apply toNat_inj
 159  exact Nat.dvd_antisymm
 160    ((divides_iff_toNat_dvd a b).mp hab)
 161    ((divides_iff_toNat_dvd b a).mp hba)
 162
 163private theorem ofNat_ne_zero_of_ne_zero {n : Nat} (h : n ≠ 0) :
 164    ofNat n ≠ zero := by
 165  intro hz
 166  have hnat := congrArg DistinctionNat.toNat hz
 167  rw [toNat_ofNat, toNat_zero] at hnat
 168  exact h hnat
 169
 170private theorem not_unit_ofNat_of_ne_one {n : Nat} (h : n ≠ 1) :
 171    ¬ unit (ofNat n) := by
 172  intro hu
 173  rw [unit_iff_toNat_eq_one] at hu
 174  rw [toNat_ofNat] at hu
 175  exact h hu
 176
 177/-- Native nontrivial factorization displays as ordinary Nat nontrivial
 178factorization. -/
 179theorem nontrivialFactorization_iff_toNat (n : DistinctionNat) :
 180    nontrivialFactorization n ↔
 181      ∃ a b : Nat,
 182        a ≠ 0 ∧ b ≠ 0 ∧ a ≠ 1 ∧ b ≠ 1 ∧ a * b = n.toNat := by
 183  constructor
 184  · intro h
 185    rcases h with ⟨a, b, ha0, hb0, ha1, hb1, hmul⟩
 186    refine ⟨a.toNat, b.toNat, ?_, ?_, ?_, ?_, ?_⟩
 187    · intro hz
 188      have : a = zero := by
 189        apply toNat_inj
 190        rw [hz, toNat_zero]
 191      exact ha0 this
 192    · intro hz
 193      have : b = zero := by
 194        apply toNat_inj
 195        rw [hz, toNat_zero]
 196      exact hb0 this
 197    · intro h1
 198      apply ha1
 199      rw [unit_iff_toNat_eq_one]
 200      exact h1
 201    · intro h1
 202      apply hb1
 203      rw [unit_iff_toNat_eq_one]
 204      exact h1
 205    · have hnat := congrArg DistinctionNat.toNat hmul
 206      rw [toNat_mul] at hnat
 207      exact hnat
 208  · intro h
 209    rcases h with ⟨a, b, ha0, hb0, ha1, hb1, hmul⟩
 210    refine ⟨ofNat a, ofNat b, ?_, ?_, ?_, ?_, ?_⟩
 211    · exact ofNat_ne_zero_of_ne_zero ha0
 212    · exact ofNat_ne_zero_of_ne_zero hb0
 213    · exact not_unit_ofNat_of_ne_one ha1
 214    · exact not_unit_ofNat_of_ne_one hb1
 215    · apply toNat_inj
 216      rw [toNat_mul, toNat_ofNat, toNat_ofNat, hmul]
 217
 218/-- Native prime-orbit predicate displays as the Nat no-nontrivial-factor
 219predicate, without defining primality by importing Nat prime theory. -/
 220theorem primeOrbit_iff_toNat_no_nontrivial_factor (p : DistinctionNat) :
 221    primeOrbit p ↔
 222      p.toNat ≠ 0 ∧ p.toNat ≠ 1 ∧
 223        ¬ ∃ a b : Nat,
 224          a ≠ 0 ∧ b ≠ 0 ∧ a ≠ 1 ∧ b ≠ 1 ∧ a * b = p.toNat := by
 225  unfold primeOrbit
 226  rw [unit_iff_toNat_eq_one, nontrivialFactorization_iff_toNat]
 227  constructor
 228  · intro h
 229    rcases h with ⟨hp0, hp1, hfac⟩
 230    refine ⟨?_, hp1, hfac⟩
 231    intro hz
 232    have : p = zero := by
 233      apply toNat_inj
 234      rw [hz, toNat_zero]
 235    exact hp0 this
 236  · intro h
 237    rcases h with ⟨hp0, hp1, hfac⟩
 238    refine ⟨?_, hp1, hfac⟩
 239    intro hz
 240    exact hp0 (by rw [hz, toNat_zero])
 241
 242/-- If an orbit is prime, every native factorization has a unit factor. -/
 243theorem unit_or_unit_of_mul_eq_prime {a b p : DistinctionNat}
 244    (hp : primeOrbit p) (hmul : a * b = p) :
 245    unit a ∨ unit b := by
 246  by_cases ha0 : a = zero
 247  · exfalso
 248    rcases hp with ⟨hp0, _, _⟩
 249    apply hp0
 250    rw [← hmul, ha0, zero_mul_eq]
 251  · by_cases hb0 : b = zero
 252    · exfalso
 253      rcases hp with ⟨hp0, _, _⟩
 254      apply hp0
 255      rw [← hmul, hb0, mul_zero_eq]
 256    · by_cases ha1 : unit a
 257      · exact Or.inl ha1
 258      · by_cases hb1 : unit b
 259        · exact Or.inr hb1
 260        · exfalso
 261          rcases hp with ⟨_, _, hnf⟩
 262          exact hnf ⟨a, b, ha0, hb0, ha1, hb1, hmul⟩
 263
 264/-- Converse native factor theorem: if a nonzero non-unit orbit position has
 265only unit factors, then it is a prime orbit. -/
 266theorem primeOrbit_of_unit_or_unit
 267    {p : DistinctionNat}
 268    (hp0 : p ≠ zero)
 269    (hp1 : ¬ unit p)
 270    (hfac : ∀ a b : DistinctionNat, a * b = p → unit a ∨ unit b) :
 271    primeOrbit p := by
 272  refine ⟨hp0, hp1, ?_⟩
 273  intro hnon
 274  rcases hnon with ⟨a, b, _ha0, _hb0, ha1, hb1, hmul⟩
 275  rcases hfac a b hmul with ha | hb
 276  · exact ha1 ha
 277  · exact hb1 hb
 278
 279theorem unit_or_eq_of_divides_prime {a p : DistinctionNat}
 280    (hp : primeOrbit p) (hdiv : divides a p) :
 281    unit a ∨ a = p := by
 282  rcases hdiv with ⟨k, hk⟩
 283  rcases unit_or_unit_of_mul_eq_prime hp hk with ha | hkunit
 284  · exact Or.inl ha
 285  · right
 286    unfold unit at hkunit
 287    rw [hkunit, mul_one_eq] at hk
 288    exact hk
 289
 290/-- Bundling certificate for the native divisibility surface. -/
 291structure OrbitDivisibilityCertificate : Prop where
 292  divides_display :
 293    ∀ a b : DistinctionNat, divides a b ↔ a.toNat ∣ b.toNat
 294  divides_reflexive :
 295    ∀ a : DistinctionNat, divides a a
 296  divides_transitive :
 297    ∀ {a b c : DistinctionNat}, divides a b → divides b c → divides a c
 298  divides_mul_right_factor :
 299    ∀ a b : DistinctionNat, divides a (a * b)
 300  divides_mul_left_factor :
 301    ∀ a b : DistinctionNat, divides b (a * b)
 302  one_divides_all :
 303    ∀ a : DistinctionNat, divides one a
 304  zero_divides_only_zero :
 305    ∀ a : DistinctionNat, divides zero a ↔ a = zero
 306  unit_display :
 307    ∀ a : DistinctionNat, unit a ↔ a.toNat = 1
 308  divides_one_exactly_units :
 309    ∀ a : DistinctionNat, divides a one ↔ unit a
 310  divisor_of_unit_is_unit :
 311    ∀ {a b : DistinctionNat}, unit b → divides a b → unit a
 312  divides_antisymmetric :
 313    ∀ {a b : DistinctionNat}, divides a b → divides b a → a = b
 314  nontrivial_factorization_display :
 315    ∀ n : DistinctionNat,
 316      nontrivialFactorization n ↔
 317        ∃ a b : Nat,
 318          a ≠ 0 ∧ b ≠ 0 ∧ a ≠ 1 ∧ b ≠ 1 ∧ a * b = n.toNat
 319  prime_orbit_display :
 320    ∀ p : DistinctionNat,
 321      primeOrbit p ↔
 322        p.toNat ≠ 0 ∧ p.toNat ≠ 1 ∧
 323          ¬ ∃ a b : Nat,
 324            a ≠ 0 ∧ b ≠ 0 ∧ a ≠ 1 ∧ b ≠ 1 ∧ a * b = p.toNat
 325  prime_factor_property :
 326    ∀ {a b p : DistinctionNat},
 327      primeOrbit p → a * b = p → unit a ∨ unit b
 328  prime_divisor_property :
 329    ∀ {a p : DistinctionNat}, primeOrbit p → divides a p → unit a ∨ a = p
 330
 331/-- The native orbit divisibility surface is closed. -/
 332theorem orbit_divisibility_certificate : OrbitDivisibilityCertificate where
 333  divides_display := divides_iff_toNat_dvd
 334  divides_reflexive := divides_refl
 335  divides_transitive := by
 336    intro a b c hab hbc
 337    exact divides_trans hab hbc
 338  divides_mul_right_factor := divides_mul_right
 339  divides_mul_left_factor := divides_mul_left
 340  one_divides_all := one_divides
 341  zero_divides_only_zero := zero_divides_iff_eq_zero
 342  unit_display := unit_iff_toNat_eq_one
 343  divides_one_exactly_units := divides_one_iff_unit
 344  divisor_of_unit_is_unit := by
 345    intro a b hb hdiv
 346    exact unit_of_divides_unit hb hdiv
 347  divides_antisymmetric := by
 348    intro a b hab hba
 349    exact divides_antisymm hab hba
 350  nontrivial_factorization_display := nontrivialFactorization_iff_toNat
 351  prime_orbit_display := primeOrbit_iff_toNat_no_nontrivial_factor
 352  prime_factor_property := by
 353    intro a b p hp hmul
 354    exact unit_or_unit_of_mul_eq_prime hp hmul
 355  prime_divisor_property := by
 356    intro a p hp hdiv
 357    exact unit_or_eq_of_divides_prime hp hdiv
 358
 359end DistinctionNat
 360end PrimitiveRecognitionCalculus
 361end Foundation
 362end IndisputableMonolith
 363