IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.ChartTransition

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/ChartTransition.lean
   3
   4  δ-native factoring starts as a chart-transition problem. The positional
   5  orbit chart gives a product/magnitude. The multiplicative chart asks for
   6  factor coordinates. This file proves the small finite statements that keep
   7  those two surfaces separate.
   8
   9  Strength: δ-native statements with verifier Nat display lemmas. No project
  10  axioms and no computational oracle for factoring.
  11-/
  12
  13import Mathlib
  14import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitEuclidean
  15
  16namespace IndisputableMonolith
  17namespace Foundation
  18namespace PrimitiveRecognitionCalculus
  19namespace Factorization
  20
  21open DistinctionNat
  22
  23/-- A native factor pair for an orbit position `n`. -/
  24structure FactorPair (n : DistinctionNat) : Type where
  25  left : DistinctionNat
  26  right : DistinctionNat
  27  product_eq : left * right = n
  28
  29/-- The positional chart sees only the product of a pair. -/
  30def factorPairProduct (a b : DistinctionNat) : DistinctionNat :=
  31  a * b
  32
  33/-- The Archimedean magnitude displayed by an orbit position. -/
  34def archimedeanMagnitude (n : DistinctionNat) : Nat :=
  35  n.toNat
  36
  37theorem factorPairProduct_toNat (a b : DistinctionNat) :
  38    (factorPairProduct a b).toNat = a.toNat * b.toNat := by
  39  unfold factorPairProduct
  40  exact toNat_mul a b
  41
  42/-- Same product means same displayed magnitude. This is the cheap chart. -/
  43theorem same_product_same_magnitude {a b c d : DistinctionNat}
  44    (h : factorPairProduct a b = factorPairProduct c d) :
  45    archimedeanMagnitude (factorPairProduct a b) =
  46      archimedeanMagnitude (factorPairProduct c d) := by
  47  unfold archimedeanMagnitude
  48  rw [h]
  49
  50/-- Concrete ambiguity: `2 * 6` and `3 * 4` are different factor pairs with
  51the same product. This is the finite obstruction behind "magnitude is not a
  52factor oracle." -/
  53theorem two_six_product_eq_three_four :
  54    factorPairProduct (ofNat 2) (ofNat 6) =
  55      factorPairProduct (ofNat 3) (ofNat 4) := by
  56  apply toNat_inj
  57  simp [factorPairProduct, toNat_mul]
  58
  59theorem two_ne_three : ofNat 2 ≠ ofNat 3 := by
  60  intro h
  61  have hnat := congrArg DistinctionNat.toNat h
  62  simp at hnat
  63
  64theorem six_ne_four : ofNat 6 ≠ ofNat 4 := by
  65  intro h
  66  have hnat := congrArg DistinctionNat.toNat h
  67  simp at hnat
  68
  69/-- Magnitude data cannot identify the left factor in general. -/
  70theorem magnitude_underdetermines_left_factor :
  71    factorPairProduct (ofNat 2) (ofNat 6) =
  72      factorPairProduct (ofNat 3) (ofNat 4) ∧
  73    ofNat 2 ≠ ofNat 3 := by
  74  exact ⟨two_six_product_eq_three_four, two_ne_three⟩
  75
  76/-- Magnitude data cannot identify the right factor in general. -/
  77theorem magnitude_underdetermines_right_factor :
  78    factorPairProduct (ofNat 2) (ofNat 6) =
  79      factorPairProduct (ofNat 3) (ofNat 4) ∧
  80    ofNat 6 ≠ ofNat 4 := by
  81  exact ⟨two_six_product_eq_three_four, six_ne_four⟩
  82
  83/-- A proper nonunit divisor gives a native nontrivial factorization. This is
  84the reusable endpoint for period-readout factoring: once a period witness gives
  85a proper gcd divisor, the δ divisibility layer supplies the factorization. -/
  86theorem nontrivialFactorization_of_proper_divisor {N d : DistinctionNat}
  87    (hN0 : N ≠ zero)
  88    (hd0 : d ≠ zero)
  89    (hdu : ¬ unit d)
  90    (hdN : d ≠ N)
  91    (hdiv : divides d N) :
  92    nontrivialFactorization N := by
  93  let q := quotient N d hd0
  94  have hq0 : q ≠ zero :=
  95    quotient_ne_zero_of_divides (n := N) (d := d) hd0 hdiv hN0
  96  have hmul_toNat : q.toNat * d.toNat = N.toNat :=
  97    quotient_mul_divisor_toNat_of_divides (n := N) (d := d) hd0 hdiv
  98  have hmul : q * d = N := by
  99    apply toNat_inj
 100    rw [toNat_mul]
 101    exact hmul_toNat
 102  have hqu : ¬ unit q := by
 103    intro hqUnit
 104    apply hdN
 105    unfold unit at hqUnit
 106    rw [← hmul, hqUnit, one_mul_eq]
 107  exact ⟨q, d, hq0, hd0, hqu, hdu, hmul⟩
 108
 109/-- Certificate for the chart-transition obstruction surface. -/
 110structure ChartTransitionCertificate : Prop where
 111  product_display :
 112    ∀ a b : DistinctionNat,
 113      (factorPairProduct a b).toNat = a.toNat * b.toNat
 114  same_product_same_magnitude :
 115    ∀ {a b c d : DistinctionNat},
 116      factorPairProduct a b = factorPairProduct c d →
 117        archimedeanMagnitude (factorPairProduct a b) =
 118          archimedeanMagnitude (factorPairProduct c d)
 119  explicit_ambiguous_product :
 120    factorPairProduct (ofNat 2) (ofNat 6) =
 121      factorPairProduct (ofNat 3) (ofNat 4)
 122  explicit_left_factor_difference :
 123    ofNat 2 ≠ ofNat 3
 124  explicit_right_factor_difference :
 125    ofNat 6 ≠ ofNat 4
 126  proper_divisor_to_nontrivial_factorization :
 127    ∀ {N d : DistinctionNat},
 128      N ≠ zero → d ≠ zero → ¬ unit d → d ≠ N → divides d N →
 129        nontrivialFactorization N
 130
 131theorem chart_transition_certificate : ChartTransitionCertificate where
 132  product_display := factorPairProduct_toNat
 133  same_product_same_magnitude := by
 134    intro a b c d h
 135    exact same_product_same_magnitude h
 136  explicit_ambiguous_product := two_six_product_eq_three_four
 137  explicit_left_factor_difference := two_ne_three
 138  explicit_right_factor_difference := six_ne_four
 139  proper_divisor_to_nontrivial_factorization := by
 140    intro N d hN0 hd0 hdu hdN hdiv
 141    exact nontrivialFactorization_of_proper_divisor hN0 hd0 hdu hdN hdiv
 142
 143end Factorization
 144end PrimitiveRecognitionCalculus
 145end Foundation
 146end IndisputableMonolith
 147