MetaphysicalGround
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.