ethics_arith_equiv_nat
plain-language theorem explainer
The declaration defines an equivalence between the Peano carrier extracted from the ethical realization and the LogicNat structure. Researchers tracing universal forcing would cite it to confirm that moral improvement counts form standard naturals. The definition is a one-line wrapper applying the orbit equivalence supplied by the ethics realization.
Claim. The carrier of the Peano arithmetic extracted from the ethical realization (whose carrier counts morally meaningful improvement steps) is equivalent to the natural numbers forced by the Law of Logic.
background
In the EthicsRealization module the ethical realization is defined with carrier MoralImprovementStep and cost in Nat, supplying only the identity and step-comparison structure required by Universal Forcing. The upstream arithmeticOf function extracts an ArithmeticOf object from any LogicRealization; its peano field yields the induced natural-number carrier. LogicNat is the inductive type with constructors identity (zero-cost element) and step, mirroring the orbit generated by repeated multiplication by the forcing element gamma.
proof idea
This definition is a one-line wrapper that applies the orbitEquivLogicNat equivalence supplied by ethicsRealization.
why it matters
The equivalence confirms that the arithmetic object forced from the ethical realization coincides with LogicNat, thereby supporting the universal forcing claim that any two realizations produce equivalent arithmetics. It closes the link between the ethics carrier (moral improvement count) and the Law-of-Logic naturals inside the Universal Forcing chain. No downstream uses are recorded, leaving the result as an internal consistency check rather than a lemma invoked elsewhere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.