metaphysical_ground_unique
The declaration supplies a canonical isomorphism identifying the Peano carrier of the arithmetic extracted from any Law-of-Logic realization with the forced natural numbers. Researchers tracing the Universal Forcing chain cite it to record uniqueness of the arithmetic ground. The definition is a one-line wrapper that directly invokes the orbit equivalence supplied by the realization.
claimFor any Law-of-Logic realization $R$, the Peano carrier of the arithmetic object extracted from $R$ is canonically equivalent to the natural numbers forced by the Law of Logic: $(arithmeticOf R).peano.carrier ≃ LogicNat$.
background
LogicRealization is a structure that supplies a carrier type, a cost type equipped with a zero element, a comparison map between carriers, a distinguished zero carrier, and the structural propositions required by the Universal Forcing program. The arithmeticOf operation extracts the forced arithmetic object from any such realization. LogicNat is the inductive type whose constructors are an identity element (the zero-cost multiplicative identity) and a step generator; it encodes the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by the generator and containing 1.
proof idea
The definition is a one-line wrapper that applies the orbitEquivLogicNat field carried by the input realization R.
why it matters in Recognition Science
The definition records the uniqueness, up to canonical equivalence, of the arithmetic ground extracted from any Law-of-Logic realization. It thereby makes precise the structural claim in the Universal Forcing paper that all realizations yield the same forced arithmetic. The module itself remains theology-neutral and only formalizes the question of the source of distinguishability.
scope and limits
- Does not identify the generator class with any concrete theological or philosophical doctrine.
- Does not construct or enumerate concrete realizations beyond the abstract LogicRealization interface.
- Does not prove existence or uniqueness of realizations themselves.
formal statement (Lean)
41noncomputable def metaphysical_ground_unique (R : LogicRealization) :
42 (arithmeticOf R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
proof body
Definition body.
43 R.orbitEquivLogicNat
44
45end MetaphysicalRealization
46end UniversalForcing
47end Foundation
48end IndisputableMonolith