IndisputableMonolith.Foundation.DistinctionToArithmetic

   1import IndisputableMonolith.Foundation.ArithmeticFromLogic
   2import IndisputableMonolith.Foundation.ArithmeticOf
   3import IndisputableMonolith.Foundation.UniversalForcing
   4import IndisputableMonolith.Foundation.UniversalForcing.CanonicalForcing
   5import IndisputableMonolith.Foundation.UniversalInstantiationFromDistinction
   6import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealLineNonNativity
   7
   8/-!
   9# Distinction to Arithmetic: the named bridge (Universal Forcing, distinction side)
  10
  11This module welds the two halves of the Universal-Forcing program that were
  12already proved separately, into the single named object the program register
  13(`δ native analysis / unification from distinction`, L5) asks for: a Lean object
  14that maps a *distinction* to its forced `ArithmeticOf` and proves that object is
  15canonical.
  16
  17Until now the route from a distinction to `ArithmeticOf` existed only
  18compositionally:
  19
  20```
  21(∃ x y : K, x ≠ y)
  22  → logicRealizationOfDistinction K x y hxy : LogicRealization      -- instantiation
  23  → UniversalForcing.arithmeticOf …          : ArithmeticOf _        -- extraction
  24  → distinction_arithmetic_equiv_logicNat    : carrier ≃ LogicNat    -- identification
  25```
  26
  27There was no single named `ArithmeticOf`-valued constructor from distinction
  28data, and no statement that the resulting forcing map is the *unique*
  29structure-preserving map (canonicity, not bare iso). This module supplies both,
  30and then states the δ-native scope honestly: a distinction forces the *countable*
  31initial Peano arithmetic (`LogicNat`), and the continuum is **not** forced from
  32countable distinction certificates (`real_not_forced_from_distinction`). So the
  33forced arithmetic of a distinction lands at `LogicNat`, never at `ℝ`; the real
  34line enters only through a completion/display interface, not from distinction
  35alone.
  36
  37What is THEOREM-grade here (0 sorry, no project-local axioms):
  38
  39* `arithmeticOfDistinction` — the named `ArithmeticOf` object of one distinction.
  40* `arithmeticOfDistinction_peanoSurface` — it carries the Peano surface
  41  (zero ≠ step, step injective, induction).
  42* `arithmeticOfDistinction_carrier_equiv_logicNat` — its carrier is `LogicNat`.
  43* `arithmeticOfDistinction_carrier_countable` — hence countable.
  44* `distinction_forcing_map` / `distinction_forcing_map_unique` /
  45  `distinction_arithmetic_universal_objective` — between any two distinctions
  46  (carriers in one universe) the forcing map exists and is the *unique*
  47  zero/step-preserving map. This is canonicity, the content of
  48  `universal-forcing-program.mdc`'s "canonical equivalence of `ArithmeticOf R`
  49  and `ArithmeticOf S`", instantiated on the distinction primitive.
  50* `real_not_forced_from_distinction` — the δ-native upper scope: ℝ is not
  51  faithfully certifiable from any countable certificate system.
  52* `DistinctionArithmeticCert` / `distinctionArithmeticCert` — the bundle.
  53
  54This does not re-prove Universal Forcing Part II; it **anchors** it to the
  55distinction primitive that the `δ` papers and `RealityFromDistinction` use.
  56-/
  57
  58namespace IndisputableMonolith
  59namespace Foundation
  60namespace DistinctionToArithmetic
  61
  62open ArithmeticFromLogic
  63open UniversalForcing
  64open UniversalInstantiationFromDistinction
  65
  66universe u
  67
  68/-! ## The named forced-arithmetic object of one distinction -/
  69
  70/-- **The forced arithmetic object of a single distinction.** Given a carrier `K`
  71with two distinguishable points `x ≠ y`, this is the `ArithmeticOf` extracted from
  72the `K`-native Law-of-Logic realization. It is the named object the program
  73register asks for: a Lean map from distinction data to `ArithmeticOf`. -/
  74noncomputable def arithmeticOfDistinction
  75    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
  76    ArithmeticOf.{u, 0, u, u, u} (logicRealizationOfDistinction K x y hxy) :=
  77  UniversalForcing.arithmeticOf (logicRealizationOfDistinction K x y hxy)
  78
  79/-- The distinction-forced arithmetic carries the Peano surface: its zero is never
  80a step, its step is injective, and it satisfies induction. -/
  81theorem arithmeticOfDistinction_peanoSurface
  82    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
  83    ArithmeticOf.PeanoSurface (arithmeticOfDistinction x y hxy) :=
  84  UniversalForcing.peano_surface (logicRealizationOfDistinction K x y hxy)
  85
  86/-- The carrier of the distinction-forced arithmetic is canonically `LogicNat`. -/
  87noncomputable def arithmeticOfDistinction_carrier_equiv_logicNat
  88    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
  89    (arithmeticOfDistinction x y hxy).peano.carrier ≃ LogicNat :=
  90  distinction_arithmetic_equiv_logicNat.{u, u, u} x y hxy
  91
  92/-- The distinction-forced arithmetic carrier is **countable**: it is `LogicNat`,
  93which is equivalent to `ℕ`. This is the δ-native lower fact: a distinction forces
  94exactly the countable initial Peano object, no more. -/
  95theorem arithmeticOfDistinction_carrier_countable
  96    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
  97    Countable (arithmeticOfDistinction x y hxy).peano.carrier := by
  98  haveI : Countable LogicNat := Countable.of_equiv Nat LogicNat.equivNat.symm
  99  exact Countable.of_equiv LogicNat
 100    (arithmeticOfDistinction_carrier_equiv_logicNat x y hxy).symm
 101
 102/-- **Distinction forces an initial Peano arithmetic.** From the bare proposition
 103that `K` has two distinct points, there is a named distinction whose forced
 104arithmetic carrier is canonically `LogicNat`. -/
 105theorem distinction_forces_arithmeticOf
 106    {K : Type u} [DecidableEq K] (h : ∃ x y : K, x ≠ y) :
 107    ∃ (x y : K) (hxy : x ≠ y),
 108      Nonempty ((arithmeticOfDistinction x y hxy).peano.carrier ≃ LogicNat) := by
 109  obtain ⟨x, y, hxy⟩ := h
 110  exact ⟨x, y, hxy, ⟨arithmeticOfDistinction_carrier_equiv_logicNat x y hxy⟩⟩
 111
 112/-! ## Canonicity: the forcing map between two distinctions is unique
 113
 114These statements fix both carriers in one universe `u`. That is the standard
 115"shared carrier universe" setting documented in `CanonicalForcing.lean`; it is not
 116a restriction on the mathematics, only the setting in which "the unique structure
 117morphism" is a well-formed comparison. -/
 118
 119/-- The canonical forcing equivalence between the forced arithmetics of two
 120distinctions. -/
 121noncomputable def distinction_forcing_map
 122    {K L : Type u} [DecidableEq K] [DecidableEq L]
 123    {x y : K} {a b : L} (hxy : x ≠ y) (hab : a ≠ b) :
 124    (arithmeticOfDistinction x y hxy).peano.carrier ≃
 125      (arithmeticOfDistinction a b hab).peano.carrier :=
 126  ArithmeticOf.equivOfInitial (arithmeticOfDistinction x y hxy) (arithmeticOfDistinction a b hab)
 127
 128/-- **Canonicity for distinctions.** Any zero/step-preserving function between the
 129forced arithmetics of two distinctions *is* the forcing map. The map is determined
 130by the distinction data alone, with no representational freedom. -/
 131theorem distinction_forcing_map_unique
 132    {K L : Type u} [DecidableEq K] [DecidableEq L]
 133    {x y : K} {a b : L} (hxy : x ≠ y) (hab : a ≠ b)
 134    (f : (arithmeticOfDistinction x y hxy).peano.carrier →
 135          (arithmeticOfDistinction a b hab).peano.carrier)
 136    (hz : f (arithmeticOfDistinction x y hxy).peano.zero =
 137            (arithmeticOfDistinction a b hab).peano.zero)
 138    (hs : ∀ p, f ((arithmeticOfDistinction x y hxy).peano.step p) =
 139            (arithmeticOfDistinction a b hab).peano.step (f p)) :
 140    f = (distinction_forcing_map hxy hab).toFun :=
 141  ArithmeticOf.forcing_map_unique
 142    (arithmeticOfDistinction x y hxy) (arithmeticOfDistinction a b hab) f hz hs
 143
 144/-- **The Universal-Forcing objective on the distinction primitive.** For any two
 145distinctions, there is a structure-preserving equivalence between their forced
 146arithmetics that is *the unique* zero/step-preserving map: existence plus
 147canonicity in one statement. -/
 148theorem distinction_arithmetic_universal_objective
 149    {K L : Type u} [DecidableEq K] [DecidableEq L]
 150    {x y : K} {a b : L} (hxy : x ≠ y) (hab : a ≠ b) :
 151    ∃ e : (arithmeticOfDistinction x y hxy).peano.carrier ≃
 152            (arithmeticOfDistinction a b hab).peano.carrier,
 153      e (arithmeticOfDistinction x y hxy).peano.zero =
 154          (arithmeticOfDistinction a b hab).peano.zero
 155      ∧ (∀ p, e ((arithmeticOfDistinction x y hxy).peano.step p) =
 156            (arithmeticOfDistinction a b hab).peano.step (e p))
 157      ∧ (∀ f : (arithmeticOfDistinction x y hxy).peano.carrier →
 158              (arithmeticOfDistinction a b hab).peano.carrier,
 159            f (arithmeticOfDistinction x y hxy).peano.zero =
 160                (arithmeticOfDistinction a b hab).peano.zero →
 161            (∀ p, f ((arithmeticOfDistinction x y hxy).peano.step p) =
 162                  (arithmeticOfDistinction a b hab).peano.step (f p)) →
 163            f = e.toFun) :=
 164  ArithmeticOf.universal_objective
 165    (arithmeticOfDistinction x y hxy) (arithmeticOfDistinction a b hab)
 166
 167/-! ## δ-native scope: the continuum is not forced from a distinction
 168
 169The forced arithmetic of any distinction is countable (`LogicNat`). The continuum
 170is a strictly larger object, and the cardinality obstruction shows it cannot be
 171faithfully covered by any countable certificate system. So the real line is not
 172native to distinction; it is reached only by completion/display. -/
 173
 174/-- **ℝ is not forced from a distinction.** No countable certificate system
 175faithfully covers ℝ. Restated from `RealLineNonNativity.real_not_faithfully_certifiable`
 176to sit beside the distinction-forced (countable) arithmetic and make the
 177unification explicit: distinction forces `LogicNat`, never `ℝ`. -/
 178theorem real_not_forced_from_distinction
 179    {Cert : Type} [Countable Cert] (assign : ℝ → Cert) :
 180    ¬ PrimitiveRecognitionCalculus.RealLineNonNativity.Faithful assign :=
 181  PrimitiveRecognitionCalculus.RealLineNonNativity.real_not_faithfully_certifiable assign
 182
 183/-! ## Certificate -/
 184
 185/-- **Distinction-to-arithmetic certificate.** For any carrier `K`, every
 186distinction on `K` forces an initial Peano arithmetic object whose carrier is
 187`LogicNat` (hence countable) and which carries the full Peano surface. -/
 188structure DistinctionArithmeticCert (K : Type u) [DecidableEq K] : Prop where
 189  /-- Every distinction forces an arithmetic carrier equivalent to `LogicNat`. -/
 190  forces_initial_arithmetic :
 191    ∀ (x y : K) (hxy : x ≠ y),
 192      Nonempty ((arithmeticOfDistinction x y hxy).peano.carrier ≃ LogicNat)
 193  /-- The forced arithmetic carrier is countable. -/
 194  forced_arithmetic_countable :
 195    ∀ (x y : K) (hxy : x ≠ y),
 196      Countable (arithmeticOfDistinction x y hxy).peano.carrier
 197  /-- The forced arithmetic carries the Peano surface. -/
 198  peano_surface :
 199    ∀ (x y : K) (hxy : x ≠ y),
 200      ArithmeticOf.PeanoSurface (arithmeticOfDistinction x y hxy)
 201
 202/-- The distinction-to-arithmetic certificate holds for every carrier. -/
 203theorem distinctionArithmeticCert (K : Type u) [DecidableEq K] :
 204    DistinctionArithmeticCert K where
 205  forces_initial_arithmetic := fun x y hxy =>
 206    ⟨arithmeticOfDistinction_carrier_equiv_logicNat x y hxy⟩
 207  forced_arithmetic_countable := fun x y hxy =>
 208    arithmeticOfDistinction_carrier_countable x y hxy
 209  peano_surface := fun x y hxy =>
 210    arithmeticOfDistinction_peanoSurface x y hxy
 211
 212end DistinctionToArithmetic
 213end Foundation
 214end IndisputableMonolith
 215