metaphysical_ground_invariant
plain-language theorem explainer
The metaphysical ground invariant defines a canonical equivalence between the Peano carriers of any two strict logic realizations. Researchers establishing domain-independent arithmetic in the strict realization framework cite it when verifying that the forced Peano structure does not depend on the choice of realization. The definition is a direct one-line wrapper around the equivalence of initial Peano objects.
Claim. For any two strict logic realizations $R$ and $S$, the carriers of their induced Peano objects satisfy $(arith(R)).peano.carrier ≃ (arith(S)).peano.carrier$.
background
StrictLogicRealization is the structure carrying a type, a cost type with zero, a comparison map, and a composition operation that realizes the laws of logic without supplied orbits. ArithmeticOf wraps a LogicRealization into a PeanoObject together with a proof that the object is initial in the category of Peano objects. The arith projection extracts this ArithmeticOf from any StrictLogicRealization by first converting to the lightweight form and then applying the arithmetic construction.
proof idea
One-line wrapper that applies ArithmeticOf.equivOfInitial to the arithmetics of the two realizations.
why it matters
This definition supplies the invariance content for the metaphysical domain inside the Rich Domain Costs module, replacing the placeholder invariance_law with a concrete statement. It guarantees that every strict realization yields the same arithmetic carrier up to equivalence, which is required for the master certificate that the strict realization is non-trivially law-bearing. In the Recognition framework it confirms that the arithmetic forced by the logic laws is canonical and independent of domain-specific cost data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.