metaphysical_ground_unique
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.