def
definition
arithmetic_invariant
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.UniversalForcing on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
25modules enrich the interpretation map from each carrier into this invariant
26arithmetic object. This definition now uses the realization's own internal
27orbit, not the reference `LogicNat` object. -/
28noncomputable def arithmetic_invariant
29 (R S : LogicRealization) :
30 (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier :=
31 ArithmeticOf.equivOfInitial (arithmeticOf R) (arithmeticOf S)
32
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