IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ObjecthoodRegistry

   1/-
   2  PrimitiveRecognitionCalculus/ObjecthoodRegistry.lean
   3
   4  Phase 8 of the Delta-Native Analysis frontier: the periodic table of
   5  mathematical objecthood.
   6
   7  The Delta program's recurring move is to ask, for any object, by what
   8  commitment it comes to exist. Some objects are forced by the law. Some are
   9  permitted free choices. Some are quotients under an equivalence. Some are
  10  completions that add an independent axiom. Some are displays: instruments, not
  11  ingredients. Some are observables. Some are conventions (gauge).
  12
  13  This module makes the classification a typed object. `Commitment` is the seven
  14  categories; `RSObject` is the catalogue of objects this program has built;
  15  `commitmentOf` assigns each its category; and the `classify_*` theorems supply
  16  the evidence, each drawn from the proved content of the other Delta-Native
  17  modules. The headline `objecthood_periodic_table` records the assignment table.
  18
  19  Evidence sources:
  20  * display      ← `DeltaReal.Protocol.display_real_forgetful`
  21  * completion   ← `Real.exists_isLUB` (independence proof: `PRCCompletenessIndependence`)
  22  * convention   ← `DeltaRealCalibration.discrete_does_not_force_unit`
  23  * quotient     ← `QuotientSelection.forced_iff`
  24  * observable   ← `QuotientSelection.observable_descends`
  25  * forced       ← prime field membership; `PrimeAxisCoherence.powerLaw_iff_aligned`
  26  * permitted    ← `GenerableReal.genField_countable`/`genField_proper`
  27
  28  No project-local axioms. No sorry.
  29-/
  30
  31import Mathlib
  32import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaReal
  33import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaRealCalibration
  34import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuotientSelection
  35import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PrimeAxisCoherence
  36import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.GenerableReal
  37import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaProbability
  38import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaAmplitude
  39import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparison
  40import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CompletionConservativity
  41
  42namespace IndisputableMonolith
  43namespace Foundation
  44namespace PrimitiveRecognitionCalculus
  45namespace ObjecthoodRegistry
  46
  47/-- The seven commitments that produce a mathematical object. -/
  48inductive Commitment where
  49  | forced       -- uniquely determined by the law; no freedom
  50  | permitted    -- an admissible free choice
  51  | quotient     -- identification under an equivalence
  52  | completion   -- closure adding limit points; an independent axiom
  53  | display      -- a rendering / instrument, not a native ingredient
  54  | observable   -- defined by what can be measured
  55  | convention   -- a gauge / labeling choice
  56  deriving DecidableEq, Repr
  57
  58/-- The objects this program has built and now classifies. -/
  59inductive RSObject where
  60  | deltaRationals     -- ℚδ, the finite-distinction carrier
  61  | protocolReals      -- ℝδ as the value display onto ℝ
  62  | classicalReals     -- ℝ, the order-complete field
  63  | calibrationUnit    -- the cost-scale unit λ
  64  | physicalQuotient   -- the gauge quotient by indistinguishability
  65  | observableFamily   -- an admissible observable family
  66  | generableCarrier   -- the finite-generation carrier over a chosen inventory
  67  | primeScale         -- the single exponent forced by coherence
  68  | continuum          -- continuity/completion interface
  69  | point              -- stabilized localization display
  70  | space              -- display geometry of stable distinctions
  71  | setObject          -- closure over many distinctions
  72  | equalityRegime     -- indistinguishability under an admissible regime
  73  | infinityMode       -- typed mode of completion
  74  | functionTransport  -- distinction-preserving transport
  75  | finiteProbability  -- finite rational counting over distinction alternatives
  76  | finiteAmplitude    -- finite amplitude data before Hilbert completion
  77  | validComparison    -- native/display/observable bridge
  78  | conservativeCompletion -- completion controlled by finite certificates
  79  | complexNumbers     -- complex scalar display over paired real carriers
  80  | finiteHilbertSpace -- finite Hilbert display of F_RS[i] amplitudes
  81  | infiniteHilbertSpace -- completed Hilbert display
  82  | manifoldDisplay    -- local chart/gluing display
  83  | measureDisplay     -- sigma/completion display of finite probability
  84  | physicsDisplayObject -- physical observable display object
  85  deriving DecidableEq, Repr
  86
  87/-- The classification assignment: the periodic table itself. -/
  88def commitmentOf : RSObject → Commitment
  89  | .deltaRationals => .forced
  90  | .protocolReals => .display
  91  | .classicalReals => .completion
  92  | .calibrationUnit => .convention
  93  | .physicalQuotient => .quotient
  94  | .observableFamily => .observable
  95  | .generableCarrier => .permitted
  96  | .primeScale => .forced
  97  | .continuum => .completion
  98  | .point => .display
  99  | .space => .display
 100  | .setObject => .permitted
 101  | .equalityRegime => .quotient
 102  | .infinityMode => .completion
 103  | .functionTransport => .observable
 104  | .finiteProbability => .forced
 105  | .finiteAmplitude => .permitted
 106  | .validComparison => .observable
 107  | .conservativeCompletion => .completion
 108  | .complexNumbers => .display
 109  | .finiteHilbertSpace => .display
 110  | .infiniteHilbertSpace => .completion
 111  | .manifoldDisplay => .display
 112  | .measureDisplay => .completion
 113  | .physicsDisplayObject => .observable
 114
 115/-! ### Evidence -/
 116
 117/-- `forced`: the rationals are forced into every carrier; they are the unique
 118prime subfield. No carrier of the framework can omit them. -/
 119theorem classify_forced_rationals :
 120    ∀ (K : Subfield ℝ) (q : ℚ), (q : ℝ) ∈ K :=
 121  fun K q => SubfieldClass.ratCast_mem K q
 122
 123/-- `forced`: once coherence (a single global power law) holds, the prime weights
 124are forced to one common scale. Coherence forces the single exponent. -/
 125theorem classify_forced_scale :
 126    ∀ a w : ℕ → ℝ,
 127      PrimeAxisCoherence.IsPowerLaw a w ↔ PrimeAxisCoherence.WeightsAligned a w :=
 128  PrimeAxisCoherence.powerLaw_iff_aligned
 129
 130/-- `display`: the protocol-real value map is surjective onto ℝ and faithful
 131(observational equality = equal value). ℝ is the forgetful display of the `ℝδ`
 132protocol interface. -/
 133theorem classify_display :
 134    Function.Surjective DeltaReal.Protocol.value
 135      ∧ (∀ x y : DeltaReal.Protocol,
 136          DeltaReal.Protocol.ObsEq x y ↔ x.value = y.value) := by
 137  obtain ⟨hsurj, _, hfaithful, _⟩ := DeltaReal.Protocol.display_real_forgetful
 138  exact ⟨hsurj, hfaithful⟩
 139
 140/-- `completion`: ℝ has the least-upper-bound property. (That no countable
 141cost-closed carrier has it, so completeness is an independent axiom, is
 142`PRCCompletenessIndependence.completeness_is_exactly_the_continuum`.) -/
 143theorem classify_completion :
 144    ∀ S : Set ℝ, S.Nonempty → (∃ b, ∀ x ∈ S, x ≤ b) → ∃ s, IsLUB S s := by
 145  intro S hne hbdd
 146  obtain ⟨b, hb⟩ := hbdd
 147  exact Real.exists_isLUB hne ⟨b, fun x hx => hb x hx⟩
 148
 149/-- `convention`: the cost-scale unit is a faithful, transitively-rescaled torsor,
 150a single free real fixed only by a continuum-side datum. It is a gauge. -/
 151theorem classify_convention :
 152    (∀ c d : ℝ, 0 < c → 0 < d →
 153        (fun t => Real.cosh (c * t) - 1) = (fun t => Real.cosh (d * t) - 1) → c = d)
 154      ∧ (∀ c d : ℝ, 0 < c → 0 < d →
 155          ∃ μ : ℝ, 0 < μ ∧
 156            (fun t => Real.cosh (c * (μ * t)) - 1) = (fun t => Real.cosh (d * t) - 1)) :=
 157  DeltaRealCalibration.discrete_does_not_force_unit
 158
 159/-- `quotient`: the physical quotient identifies two states iff no observable
 160distinguishes them. The quotient is forced by indistinguishability. -/
 161theorem classify_quotient :
 162    ∀ {X C : Type} (F : Set (X → C)) (x y : X),
 163      QuotientSelection.proj F x = QuotientSelection.proj F y ↔ QuotientSelection.ObsEquiv F x y :=
 164  fun F x y => QuotientSelection.forced_iff F x y
 165
 166/-- `observable`: every admissible observable descends to the physical quotient;
 167the quotient loses no observable information. -/
 168theorem classify_observable :
 169    ∀ {X C : Type} (F : Set (X → C)) (f : X → C), f ∈ F →
 170      ∃ g : QuotientSelection.PhysicalQuotient F → C, ∀ x, g (QuotientSelection.proj F x) = f x :=
 171  fun F f hf => QuotientSelection.observable_descends F f hf
 172
 173/-- `permitted`: the constant inventory of the generable carrier is a free but
 174admissible choice. Every countable inventory yields a valid countable carrier
 175that is a proper subset of ℝ. -/
 176theorem classify_permitted :
 177    ∀ κ : ℕ → ℝ,
 178      (GenerableReal.genField κ : Set ℝ).Countable
 179        ∧ (GenerableReal.genField κ : Set ℝ) ≠ Set.univ :=
 180  fun κ => ⟨GenerableReal.genField_countable κ, GenerableReal.genField_proper κ⟩
 181
 182/-- **Phase 8 headline: the periodic table of objecthood.** Each catalogued object
 183carries its commitment, and the assignment is exactly the evidence above:
 184distinction-forced (rationals, the coherence scale), display (ℝδ value map),
 185completion (ℝ), convention (cost unit), quotient and observable (the gauge
 186quotient and its probes), permitted (the generable inventory). Objecthood is not
 187flat: each object is produced by a specific kind of commitment, and the kind is
 188now a typed, proved attribute. -/
 189theorem objecthood_periodic_table :
 190    commitmentOf RSObject.deltaRationals = Commitment.forced
 191      ∧ commitmentOf RSObject.protocolReals = Commitment.display
 192      ∧ commitmentOf RSObject.classicalReals = Commitment.completion
 193      ∧ commitmentOf RSObject.calibrationUnit = Commitment.convention
 194      ∧ commitmentOf RSObject.physicalQuotient = Commitment.quotient
 195      ∧ commitmentOf RSObject.observableFamily = Commitment.observable
 196      ∧ commitmentOf RSObject.generableCarrier = Commitment.permitted
 197      ∧ commitmentOf RSObject.primeScale = Commitment.forced :=
 198  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
 199
 200/-- **Background-object audit.** The conversation's broader target is now inside
 201the objecthood registry: continuum, point, space, set, equality, infinity,
 202function, probability, amplitude, valid comparison, and conservative completion
 203all receive explicit commitment tags. This prevents background objects from
 204entering the theory untyped. -/
 205theorem background_object_audit :
 206    commitmentOf RSObject.continuum = Commitment.completion
 207      ∧ commitmentOf RSObject.point = Commitment.display
 208      ∧ commitmentOf RSObject.space = Commitment.display
 209      ∧ commitmentOf RSObject.setObject = Commitment.permitted
 210      ∧ commitmentOf RSObject.equalityRegime = Commitment.quotient
 211      ∧ commitmentOf RSObject.infinityMode = Commitment.completion
 212      ∧ commitmentOf RSObject.functionTransport = Commitment.observable
 213      ∧ commitmentOf RSObject.finiteProbability = Commitment.forced
 214      ∧ commitmentOf RSObject.finiteAmplitude = Commitment.permitted
 215      ∧ commitmentOf RSObject.validComparison = Commitment.observable
 216      ∧ commitmentOf RSObject.conservativeCompletion = Commitment.completion
 217      ∧ commitmentOf RSObject.complexNumbers = Commitment.display
 218      ∧ commitmentOf RSObject.finiteHilbertSpace = Commitment.display
 219      ∧ commitmentOf RSObject.infiniteHilbertSpace = Commitment.completion
 220      ∧ commitmentOf RSObject.manifoldDisplay = Commitment.display
 221      ∧ commitmentOf RSObject.measureDisplay = Commitment.completion
 222      ∧ commitmentOf RSObject.physicsDisplayObject = Commitment.observable :=
 223  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl,
 224    rfl⟩
 225
 226/-- **Display-object extension.** Complex numbers, finite and infinite Hilbert
 227spaces, manifolds, measures, and physics display objects are now explicitly
 228typed. This closes the objecthood-table extension requested by the completion
 229plan. -/
 230theorem display_object_extension :
 231    commitmentOf RSObject.complexNumbers = Commitment.display
 232      ∧ commitmentOf RSObject.finiteHilbertSpace = Commitment.display
 233      ∧ commitmentOf RSObject.infiniteHilbertSpace = Commitment.completion
 234      ∧ commitmentOf RSObject.manifoldDisplay = Commitment.display
 235      ∧ commitmentOf RSObject.measureDisplay = Commitment.completion
 236      ∧ commitmentOf RSObject.physicsDisplayObject = Commitment.observable :=
 237  ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩
 238
 239end ObjecthoodRegistry
 240end PrimitiveRecognitionCalculus
 241end Foundation
 242end IndisputableMonolith
 243