strict_metaphysical_ground_unique
plain-language theorem explainer
This definition equates the Peano carrier of the arithmetic derived from any strict logic realization R to the logic-forced natural numbers LogicNat. Researchers tracing the strict universal forcing chain to its metaphysical ground would cite it to confirm the identification. The definition is a one-line wrapper that applies the orbit equivalence after converting R to the lightweight realization interface.
Claim. For any strict logic realization $R$, the Peano carrier of the arithmetic extracted from $R$ is canonically equivalent to the logic-forced natural numbers LogicNat.
background
A StrictLogicRealization supplies a carrier type, cost type with zero element, comparison, and composition, all native to the law of logic with no supplied orbit. The arith operation extracts the forced arithmetic structure from the lightweight conversion of R. LogicNat is the inductive type whose identity constructor is the zero-cost multiplicative identity and whose step constructor iterates the generator, forming the smallest orbit closed under multiplication by γ and containing 1.
proof idea
The definition is a one-line wrapper that applies the orbitEquivLogicNat field of the lightweight realization produced by toLightweight R.
why it matters
The definition supplies the structural identification required by the axiom audit, directly feeding the _ethics_ok declaration that aligns ethical realizations with forced arithmetic. It completes the metaphysical grounding step in the strict universal forcing package, linking the realization carrier to LogicNat without extra hypotheses. It touches no open questions and closes the identification for downstream audits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.