strict_metaphysical_ground_unique
plain-language theorem explainer
For any strict realization R of the law of logic, this definition supplies a canonical equivalence identifying the Peano carrier inside the forced arithmetic of R with the inductively generated LogicNat. Researchers tracing the strict universal forcing chain to its arithmetic foundation would cite the result when grounding metaphysical structures. The proof is a one-line wrapper that routes through the lightweight conversion and its pre-established orbit equivalence.
Claim. For any strict Law-of-Logic realization $R$, the carrier of the Peano arithmetic extracted from the arithmetic derived from $R$ is equivalent to the natural numbers forced by the Law of Logic.
background
StrictLogicRealization is the structure that encodes a strict realization using only native law data: a Carrier type, a Cost type with zeroCost, a compare function, and a compose operation. LogicNat is the inductive type with constructors identity (zero-cost element) and step, mirroring the orbit generated by repeated multiplication by the generator gamma. The arith operation extracts forced arithmetic from the lightweight interface obtained by toLightweight, which converts a strict realization by deriving all orbit fields from LogicNat rather than taking them as inputs. The module supplies a theology-neutral metaphysical package built directly on the strict Universal Forcing theorem.
proof idea
One-line wrapper that applies toLightweight to the input realization R and then invokes the orbitEquivLogicNat equivalence already available on the resulting lightweight realization.
why it matters
The definition supplies the structural identification required by the strict metaphysical package and is invoked inside the ethics_ok audit in AxiomAudit. It completes the step that equates the metaphysical ground with the universal forced arithmetic object, closing one link in the chain from StrictLogicRealization to the arithmetic forced by logic. No open scaffolding remains at this site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.