universalGround
plain-language theorem explainer
universalGround constructs the canonical MetaphysicalGround instance that names the source of distinguishability and supplies the arithmetic identification and invariance maps required by the structure. Researchers tracing the structural consequences of canonically equivalent forced arithmetic in the Universal Forcing framework would cite this definition. It is assembled by direct field assignment using the orbit equivalence on each realization and the initial-Peano equivalence construction.
Claim. Let $M$ be the structure with source name ``Universal generator of distinguishability'', such that for every logic realization $R$ the arithmetic carrier of $R$ is identified with the LogicNat object via the orbit equivalence, and for any realizations $R,S$ the carriers are equivalent via the lift supplied by their initial Peano objects.
background
MetaphysicalGround is the structure that assigns every Law-of-Logic realization its forced arithmetic while guaranteeing that the resulting arithmetic objects are canonically the same; its fields are sourceName, identifies_arithmetic, and invariant. The module supplies a theology-neutral formalization of the metaphysical question from the Universal Forcing paper: when all realizations share canonically equivalent forced arithmetic, the source of distinguishability is represented by the universal generator class without reference to any specific doctrine.
proof idea
The definition populates the three fields of MetaphysicalGround by direct assignment. sourceName receives the indicated string. identifies_arithmetic is supplied by the orbit equivalence on each realization. invariant is supplied by invoking equivOfInitial on the arithmetic objects of the two realizations.
why it matters
This definition supplies the canonical metaphysical-ground structure promised by the universal forcing theorem in the neutral structural sense. It makes precise the metaphysical question formalized in the module by providing the universal generator of distinguishability. In the Recognition framework it links the arithmetic invariance from initial Peano objects to the forcing chain that derives physical structure from the J-cost functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.