StrictMetaphysicalGround
plain-language theorem explainer
StrictMetaphysicalGround packages a source name with the property that every strict logic realization extracts arithmetic whose Peano carrier is equivalent to the logic-forced natural numbers, plus invariance of that carrier across all such realizations. Researchers working on the strict universal forcing theorem cite it to ground distinguishability in forced arithmetic without doctrinal identification. The declaration is a direct structure definition that introduces the three fields with no proof obligations.
Claim. A strict metaphysical ground consists of a source name string together with the assertion that for every strict logic realization $R$ the Peano carrier of its extracted arithmetic is equivalent to the natural numbers forced by logic, and that these carriers are equivalent for any pair of realizations $R$ and $S$.
background
The module supplies a theology-neutral metaphysical package based on the strict universal forcing theorem. A strict logic realization is a structure with a carrier type, a cost type equipped with a zero element, and compare and compose operations that encode native law data without a supplied orbit. The arithmetic extraction operation on such a realization produces a structure whose Peano carrier is canonically equivalent to LogicNat, the inductive type whose identity constructor represents the zero-cost element and whose step constructor iterates the generator, mirroring the orbit closed under multiplication by the generator and containing the multiplicative identity.
proof idea
The declaration is a pure structure definition that directly introduces the three fields source name, identifies arithmetic, and invariant. No lemmas or tactics are applied; the fields stand as the definition itself.
why it matters
This structure is instantiated by the canonical strict universal ground supplied by strict universal forcing. It completes the metaphysical layer of the strict realization, ensuring arithmetic invariance across realizations as required by the universal forcing chain. It addresses the role of a ground of distinguishability in a theology-neutral manner within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.