IndisputableMonolith.Foundation.UniversalForcing.Strict.Metaphysical

   1import IndisputableMonolith.Foundation.UniversalForcing.Strict.Ethics
   2
   3/-!
   4  Strict/Metaphysical.lean
   5
   6  Structural, theology-neutral metaphysical package based on the strict
   7  Universal Forcing theorem.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Foundation
  12namespace UniversalForcing
  13namespace Strict
  14namespace Metaphysical
  15
  16open Invariance
  17
  18/-- A strict metaphysical ground is a structural package assigning every strict
  19realization its forced arithmetic and proving invariance across all strict
  20realizations. This is theology-neutral: it names the mathematical role of a
  21ground of distinguishability without identifying it with any doctrine. -/
  22structure StrictMetaphysicalGround where
  23  sourceName : String
  24  identifies_arithmetic :
  25    ∀ R : StrictLogicRealization,
  26      (StrictLogicRealization.arith R).peano.carrier ≃ ArithmeticFromLogic.LogicNat
  27  invariant :
  28    ∀ R S : StrictLogicRealization,
  29      (StrictLogicRealization.arith R).peano.carrier
  30        ≃ (StrictLogicRealization.arith S).peano.carrier
  31
  32/-- Canonical strict metaphysical ground supplied by strict universal forcing. -/
  33noncomputable def strictUniversalGround : StrictMetaphysicalGround where
  34  sourceName := "Strict universal generator of distinguishability"
  35  identifies_arithmetic := fun R =>
  36    (StrictLogicRealization.toLightweight R).orbitEquivLogicNat
  37  invariant := fun R S =>
  38    ArithmeticOf.equivOfInitial (StrictLogicRealization.arith R)
  39      (StrictLogicRealization.arith S)
  40
  41/-- Structural identification of the metaphysical ground with the universal
  42forced arithmetic object. -/
  43noncomputable def strict_metaphysical_ground_unique (R : StrictLogicRealization) :
  44    (StrictLogicRealization.arith R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  45  (StrictLogicRealization.toLightweight R).orbitEquivLogicNat
  46
  47end Metaphysical
  48end Strict
  49end UniversalForcing
  50end Foundation
  51end IndisputableMonolith
  52