`distinction_realizations_have_same_arithmetic`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalInstantiationFromDistinction
domain: Foundation
line: 178 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.UniversalInstantiationFromDistinction on GitHub at line 178.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 175
 176/-- Any two non-singleton carriers, with chosen distinctions, have
 177canonically equivalent forced arithmetic. -/
 178noncomputable def distinction_realizations_have_same_arithmetic
 179    {K L : Type u} [DecidableEq K] [DecidableEq L]
 180    {x y : K} {a b : L} (hxy : x ≠ y) (hab : a ≠ b) :
 181    (UniversalForcing.arithmeticOf
 182      (logicRealizationOfDistinction K x y hxy)).peano.carrier ≃
 183    (UniversalForcing.arithmeticOf
 184      (logicRealizationOfDistinction L a b hab)).peano.carrier :=
 185  (logicRealizationOfDistinction K x y hxy).orbitEquivLogicNat.trans
 186    (logicRealizationOfDistinction L a b hab).orbitEquivLogicNat.symm
 187
 188/-! ## Certificate -/
 189
 190structure UniversalInstantiationCert (K : Type u) [Nonempty K] : Prop where
 191  instantiate :
 192    (∃ x y : K, x ≠ y) → Nonempty (LogicRealization.{u, 0})
 193  named :
 194    (∃ x y : K, x ≠ y) →
 195      ∃ x y : K, ∃ hxy : x ≠ y,
 196        Nonempty (LogicRealization.{u, 0})
 197
 198theorem universalInstantiationCert
 199    (K : Type u) [Nonempty K] :
 200    UniversalInstantiationCert K where
 201  instantiate := exists_logicRealization_of_distinction K
 202  named := exists_named_logicRealization_of_distinction K
 203
 204end UniversalInstantiationFromDistinction
 205end Foundation
 206end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.