IndisputableMonolith.Foundation.UniversalForcing.Strict.CanonicalIso

   1import IndisputableMonolith.Foundation.UniversalForcing.Strict.Invariance
   2import IndisputableMonolith.Foundation.UniversalForcing.CanonicalIso
   3
   4/-!
   5  Strict/CanonicalIso.lean
   6
   7  Structure-preserving Universal Forcing for the strict "no escape hatch"
   8  realizations.
   9
  10  `Strict/Invariance.lean` already proves the strict universal forcing bijection
  11  `strict_universal_forcing R S` between the forced arithmetics of any two
  12  `StrictLogicRealization`s.  This module upgrades that bijection, on the strict
  13  surface, to a *unique structure-preserving isomorphism* of Peano algebras,
  14  reusing `UniversalForcing.universalForcingPeanoEquiv` and
  15  `UniversalForcing.peanoEquiv_unique` through the strict-to-lightweight functor.
  16
  17  A strict realization supplies only native comparison / composition / identity /
  18  invariance / non-triviality data; its forced arithmetic is derived, not
  19  supplied.  So the canonical Peano isomorphism here is genuinely forced by the
  20  native law data, with no orbit handed in by the caller.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Foundation
  25namespace UniversalForcing
  26namespace Strict
  27namespace CanonicalIso
  28
  29/-- **Strict Universal Forcing, structure-preserving form.**
  30
  31For any two strict Law-of-Logic realizations, the bijection between their forced
  32arithmetics is a structure-preserving isomorphism of Peano algebras: it sends
  33zero to zero and commutes with the successor map. -/
  34noncomputable def strict_universal_forcing_peanoEquiv
  35    (R S : StrictLogicRealization) :
  36    PeanoEquiv (StrictLogicRealization.arith R).peano
  37      (StrictLogicRealization.arith S).peano :=
  38  universalForcingPeanoEquiv (StrictLogicRealization.toLightweight R)
  39    (StrictLogicRealization.toLightweight S)
  40
  41/-- **Strict canonicality.**
  42
  43Any two structure-preserving isomorphisms between the forced arithmetics of two
  44strict realizations have the same underlying function.  The strict universal
  45forcing isomorphism is therefore the unique one. -/
  46theorem strict_peanoEquiv_unique (R S : StrictLogicRealization)
  47    (e₁ e₂ : PeanoEquiv (StrictLogicRealization.arith R).peano
  48      (StrictLogicRealization.arith S).peano) :
  49    (e₁.toEquiv : (StrictLogicRealization.arith R).peano.carrier
  50        → (StrictLogicRealization.arith S).peano.carrier)
  51      = e₂.toEquiv :=
  52  peanoEquiv_unique (StrictLogicRealization.toLightweight R)
  53    (StrictLogicRealization.toLightweight S) e₁ e₂
  54
  55/-- **Strict Universal Forcing isomorphism certificate.**
  56
  57For any two strict Law-of-Logic realizations there is a canonical
  58structure-preserving isomorphism between their forced arithmetics, and it is
  59unique. -/
  60structure StrictUniversalForcingIsoCert where
  61  /-- The canonical Peano-algebra isomorphism between any two strict forced
  62  arithmetics. -/
  63  iso : ∀ R S : StrictLogicRealization,
  64    PeanoEquiv (StrictLogicRealization.arith R).peano
  65      (StrictLogicRealization.arith S).peano
  66  /-- That isomorphism is unique as a structure-preserving map. -/
  67  unique : ∀ (R S : StrictLogicRealization)
  68      (e₁ e₂ : PeanoEquiv (StrictLogicRealization.arith R).peano
  69        (StrictLogicRealization.arith S).peano),
  70      (e₁.toEquiv : (StrictLogicRealization.arith R).peano.carrier
  71          → (StrictLogicRealization.arith S).peano.carrier)
  72        = e₂.toEquiv
  73
  74/-- The strict certificate is inhabited by the strict canonical iso and its
  75uniqueness. -/
  76noncomputable def strictUniversalForcingIsoCert : StrictUniversalForcingIsoCert where
  77  iso := fun R S => strict_universal_forcing_peanoEquiv R S
  78  unique := fun R S => strict_peanoEquiv_unique R S
  79
  80end CanonicalIso
  81end Strict
  82end UniversalForcing
  83end Foundation
  84end IndisputableMonolith
  85