IndisputableMonolith.Foundation.UniversalForcing.ForcedIntegers

   1/-
   2  UniversalForcing/ForcedIntegers.lean
   3
   4  The middle forced layer: from counting to the integers, by differences.
   5
   6  The δ paper claims distinction forces three discrete layers: the natural
   7  numbers, the integers, and the rational field. The Lean spine forced the first
   8  (`ForcedSemiring`: the forced arithmetic is canonically `ℕ`) and the third
   9  (`ForcedRatios`: the ratios of forced numbers are exactly `ℚ_{>0}`). This module
  10  fills the middle: the *differences* of forced numbers are exactly `ℤ`.
  11
  12  The construction is the additive mirror of `ForcedRatios`. There, two counts are
  13  compared multiplicatively (the ratio `a/b`), the comparison symmetry is the
  14  reciprocal involution `x ↦ x⁻¹`, and its fixed locus is the unit ratio `a = b`,
  15  which is the recognition cost's zero. Here two counts are compared additively
  16  (the difference `a − b`), the comparison symmetry is negation `z ↦ −z` (the
  17  debit/credit swap of the ledger), and its fixed locus is again the diagonal
  18  `a = b`, the additive null. Counting forces `ℕ`; the ledger's two-sided
  19  (credit/debit) nature forces its difference group `ℤ`.
  20
  21  Results, parallel to `ForcedRatios`:
  22
  23  * `integers_surject`: every integer is a difference of two forced numbers, so
  24    the forced difference layer is all of `ℤ`, with the embedding `toInt`
  25    preserving `0, 1, +, ×` and injective.
  26  * `forced_difference_zero_iff`: a difference of forced numbers vanishes exactly
  27    on the diagonal `a = b` (the additive null locus).
  28  * `forced_difference_fixed_iff`: the negation involution fixes a forced
  29    difference exactly on the diagonal — the additive analogue of the reciprocal
  30    involution fixing the unit ratio.
  31-/
  32
  33import IndisputableMonolith.Foundation.UniversalForcing.ForcedSemiring
  34
  35namespace IndisputableMonolith
  36namespace Foundation
  37namespace UniversalForcing
  38namespace ForcedIntegers
  39
  40open ArithmeticFromLogic
  41open ArithmeticFromLogic.LogicNat
  42
  43/-! ## The canonical embedding of the forced arithmetic into `ℤ`. -/
  44
  45/-- Embed a forced number into the integers by its iteration count. -/
  46def toInt (n : LogicNat) : ℤ := (LogicNat.toNat n : ℤ)
  47
  48@[simp] theorem toInt_zero : toInt LogicNat.zero = 0 := by simp [toInt]
  49
  50@[simp] theorem toInt_one : toInt 1 = 1 := by
  51  show ((LogicNat.toNat 1 : ℕ) : ℤ) = 1
  52  rw [show LogicNat.toNat 1 = 1 from rfl]
  53  norm_num
  54
  55theorem toInt_add (a b : LogicNat) : toInt (a + b) = toInt a + toInt b := by
  56  simp only [toInt]
  57  rw [LogicNat.toNat_add]
  58  push_cast
  59  ring
  60
  61theorem toInt_mul (a b : LogicNat) : toInt (a * b) = toInt a * toInt b := by
  62  simp only [toInt]
  63  rw [LogicNat.toNat_mul]
  64  push_cast
  65  ring
  66
  67theorem toInt_injective : Function.Injective toInt := by
  68  intro a b h
  69  have hnat : LogicNat.toNat a = LogicNat.toNat b := by
  70    have : (LogicNat.toNat a : ℤ) = (LogicNat.toNat b : ℤ) := h
  71    exact_mod_cast this
  72  exact LogicNat.equivNat.injective hnat
  73
  74theorem toInt_nonneg (n : LogicNat) : 0 ≤ toInt n := by
  75  simp only [toInt]
  76  exact Int.natCast_nonneg _
  77
  78/-! ## The forced differences are exactly the integers. -/
  79
  80/-- **Every integer is a difference of two forced numbers.** The forced
  81difference layer is all of `ℤ`, so distinction forces the full additive group of
  82integers, not a proper sub-collection. -/
  83theorem integers_surject (z : ℤ) :
  84    ∃ a b : LogicNat, z = toInt a - toInt b := by
  85  refine ⟨LogicNat.fromNat z.toNat, LogicNat.fromNat (-z).toNat, ?_⟩
  86  simp only [toInt, LogicNat.toNat_fromNat]
  87  omega
  88
  89/-! ## The negation involution acts on the forced differences. -/
  90
  91/-- A difference of forced numbers vanishes exactly on the diagonal: the additive
  92null locus is `a = b`, mirroring the multiplicative unit locus of `ForcedRatios`. -/
  93theorem forced_difference_zero_iff (a b : LogicNat) :
  94    toInt a - toInt b = 0 ↔ a = b := by
  95  constructor
  96  · intro h
  97    have : toInt a = toInt b := by omega
  98    exact toInt_injective this
  99  · intro h; subst h; ring
 100
 101/-- Negation swaps the two counts of a forced difference: `−(a − b) = b − a`. This
 102is the additive analogue of the reciprocal swap `(a/b)⁻¹ = b/a` on forced ratios. -/
 103theorem forced_difference_neg_swap (a b : LogicNat) :
 104    -(toInt a - toInt b) = toInt b - toInt a := by ring
 105
 106/-- **The additive analogue of the reciprocal fixed-point law.** The negation
 107involution fixes a forced difference exactly on the diagonal `a = b` — just as the
 108reciprocal involution fixes a forced ratio exactly on the unit `a = b`. The two
 109forced layers, integers and ratios, carry the same comparison geometry: an
 110involution that swaps two counts, fixed precisely where the counts agree. -/
 111theorem forced_difference_fixed_iff (a b : LogicNat) :
 112    (toInt a - toInt b = -(toInt a - toInt b)) ↔ a = b := by
 113  rw [forced_difference_neg_swap]
 114  constructor
 115  · intro h
 116    have hz : toInt a - toInt b = 0 := by omega
 117    exact (forced_difference_zero_iff a b).mp hz
 118  · intro h; subst h; ring
 119
 120/-! ## Certificate: distinction forces the additive group of integers. -/
 121
 122/-- **Certificate.** The forced arithmetic embeds in `ℤ` preserving `0, 1, +, ×`;
 123its differences are exactly `ℤ`; and the negation involution fixes a difference
 124precisely on the diagonal. The integer layer the δ paper names is forced,
 125canonical, and carries the additive mirror of the ratio layer's comparison
 126geometry. -/
 127structure ForcedIntegersCert where
 128  embed : LogicNat → ℤ
 129  embed_zero : embed LogicNat.zero = 0
 130  embed_one : embed 1 = 1
 131  embed_add : ∀ a b, embed (a + b) = embed a + embed b
 132  embed_mul : ∀ a b, embed (a * b) = embed a * embed b
 133  embed_injective : Function.Injective embed
 134  differences_surject : ∀ z : ℤ, ∃ a b : LogicNat, z = embed a - embed b
 135  negation_diagonal : ∀ a b : LogicNat,
 136      (toInt a - toInt b = -(toInt a - toInt b)) ↔ a = b
 137
 138/-- The forced-integers certificate holds. -/
 139def forcedIntegersCert_holds : ForcedIntegersCert where
 140  embed := toInt
 141  embed_zero := toInt_zero
 142  embed_one := toInt_one
 143  embed_add := toInt_add
 144  embed_mul := toInt_mul
 145  embed_injective := toInt_injective
 146  differences_surject := integers_surject
 147  negation_diagonal := forced_difference_fixed_iff
 148
 149end ForcedIntegers
 150end UniversalForcing
 151end Foundation
 152end IndisputableMonolith
 153