MetaphysicalGround
plain-language theorem explainer
MetaphysicalGround supplies a structure that pairs a source identifier with the guarantee that every logic realization extracts an arithmetic object canonically equivalent to the logic naturals and invariant across realizations. Workers on the universal forcing theorem cite it when they need a neutral container for the source of distinguishability. The declaration is supplied directly as a structure definition with three fields.
Claim. A metaphysical ground consists of a string identifier together with the assertions that, for every logic realization $R$, the Peano carrier of the arithmetic object extracted from $R$ is equivalent to the logic natural numbers, and that this equivalence is the same for any pair of realizations $R$ and $S$.
background
LogicRealization is a carrier equipped with a comparison cost, zero-cost element, identity, and generator step, together with the structural laws required by the forcing program. arithmeticOf extracts from any such realization the initial Peano object whose carrier is the orbit generated by repeated application of the step. LogicNat is the inductive type whose constructors identity and step mirror the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by the generator and containing the multiplicative identity.
proof idea
The declaration is a direct structure definition that records the source name and the two equivalence statements; no lemmas are applied.
why it matters
universalGround in the same module instantiates the structure with the universal generator as source and the orbit equivalence supplied by arithmeticOf. The module doc-comment states that the construction makes the metaphysical question from the Universal Forcing paper precise in a theology-neutral way: if all realizations share canonically equivalent forced arithmetic, the source of distinguishability is represented by this generator class. It therefore sits at the interface between the arithmetic extraction theorem and any later identification of the generator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.