def
definition
arith_universal_initial
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.UniversalForcing on GitHub at line 36.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
33/-- The forced arithmetic of every realization is canonically equivalent to
34the reference `LogicNat` Peano object. This is the simplest form of the
35Universal Forcing theorem. -/
36noncomputable def arith_universal_initial (R : LogicRealization) :
37 (arithmeticOf R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
38 R.orbitEquivLogicNat
39
40/-- **Universal Forcing Meta-Theorem, abstract spine.**
41
42Any two Law-of-Logic realizations have canonically equivalent forced
43arithmetic objects. -/
44noncomputable def universal_forcing (R S : LogicRealization) :
45 (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier :=
46 ArithmeticOf.equivOfInitial (arithmeticOf R) (arithmeticOf S)
47
48/-- The continuous positive-ratio realization has the same forced arithmetic
49as every other realization. -/
50noncomputable def continuous_positive_ratio_arithmetic_invariant
51 (C : LogicAsFunctionalEquation.ComparisonOperator)
52 (h : LogicAsFunctionalEquation.SatisfiesLawsOfLogic C)
53 (S : LogicRealization.{0, 0}) :
54 (arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)).peano.carrier
55 ≃ (arithmeticOf S).peano.carrier :=
56 ArithmeticOf.equivOfInitial
57 (arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)) (arithmeticOf S)
58
59/-- The Peano surface is available for the forced arithmetic of every
60realization. -/
61theorem peano_surface (R : LogicRealization) :
62 ArithmeticOf.PeanoSurface (arithmeticOf R) :=
63 ArithmeticOf.extracted_peanoSurface R
64
65end UniversalForcing
66end Foundation