MetaphysicalGround
MetaphysicalGround defines a structure that assigns every Law-of-Logic realization its forced arithmetic object while requiring all such objects to be canonically equivalent. Foundation researchers in Recognition Science cite it when stating the universal forcing theorem in neutral structural terms. The definition is a direct encoding of a source name plus two equivalence properties with no computational content or lemmas.
claimA metaphysical ground consists of a string source name together with the properties that, for every logic realization $R$, the Peano carrier of the arithmetic extracted from $R$ is equivalent to the logic natural numbers, and that for any two realizations $R$ and $S$ these carriers are equivalent to each other.
background
LogicRealization supplies a carrier type, a cost type equipped with zero, a comparison map, and a zero element, together with the structural laws required by the forcing program. arithmeticOf extracts from any realization the canonical arithmetic object whose Peano surface is logicNatPeano. LogicNat is the inductive type with constructors identity and step, representing the orbit under the generator that begins at the multiplicative identity and is closed under multiplication by the generator step.
proof idea
This declaration is a pure structure definition. It introduces the three fields sourceName, identifies_arithmetic, and invariant directly, with no lemmas, tactics, or reductions applied.
why it matters in Recognition Science
This definition supplies the type instantiated by universalGround to realize the canonical metaphysical ground supplied by the universal forcing theorem. It makes precise the structural claim that the source of distinguishability yields a unique arithmetic across all realizations. In the Recognition Science framework it closes the metaphysical question in the Universal Forcing paper without committing to any particular doctrine.
scope and limits
- Does not identify the source with any theological or philosophical doctrine.
- Does not supply computational content or decision procedures.
- Does not depend on specific physical constants or spatial dimensions.
- Does not prove uniqueness of the ground beyond carrier equivalence.
formal statement (Lean)
25structure MetaphysicalGround where
26 sourceName : String
27 identifies_arithmetic :
28 ∀ R : LogicRealization, (arithmeticOf R).peano.carrier ≃ ArithmeticFromLogic.LogicNat
29 invariant :
30 ∀ R S : LogicRealization, (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier
31
32/-- The universal forcing theorem supplies a canonical metaphysical-ground