strictUniversalGround
plain-language theorem explainer
The declaration supplies the canonical instance of StrictMetaphysicalGround in the Recognition Science foundation. It equips every strict logic realization with its forced arithmetic Peano carrier and establishes invariance of that carrier across realizations via initial-object lifts. The construction is a direct field assignment that composes the lightweight realization map with the orbit equivalence and applies equivOfInitial to the extracted arithmetic objects.
Claim. The canonical strict metaphysical ground is the structure whose source name is the string ``Strict universal generator of distinguishability'', whose identifies_arithmetic field sends each strict logic realization $R$ to the equivalence $(StrictLogicRealization.arith R).peano.carrier ≃ ArithmeticFromLogic.LogicNat$ obtained from the orbit map, and whose invariant field supplies, for any pair of realizations $R,S$, the equivalence of their Peano carriers given by the lift through their initiality properties.
background
In Strict/Metaphysical.lean the module supplies a theology-neutral structural package based on the strict Universal Forcing theorem. A StrictMetaphysicalGround is defined as a record containing a sourceName string together with two maps: identifies_arithmetic, which for every strict logic realization $R$ produces an equivalence between the Peano carrier of its forced arithmetic and LogicNat, and invariant, which produces an equivalence between the Peano carriers of any two such arithmetics. The upstream ArithmeticOf structure packages a Peano object together with its initiality witness for a given logic realization; equivOfInitial then constructs the canonical equivalence between any two initial Peano objects by composing the unique lifts guaranteed by initiality.
proof idea
The definition is a direct structure constructor. It populates identifies_arithmetic by applying StrictLogicRealization.toLightweight to $R$ and then orbitEquivLogicNat. It populates invariant by extracting the arithmetic objects via StrictLogicRealization.arith on each realization and feeding them to ArithmeticOf.equivOfInitial.
why it matters
This supplies the canonical strict metaphysical ground required by the strict Universal Forcing theorem, identifying the ground of distinguishability with the universal forced arithmetic object in a theology-neutral manner. It closes the interface defined by StrictMetaphysicalGround and thereby makes the strict realization package available for use in the foundation layer. No downstream dependents are recorded, so the definition functions as a terminal structural anchor rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.