structure
definition
StrictMetaphysicalGround
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.UniversalForcing.Strict.Metaphysical on GitHub at line 22.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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