ethicsRealization
plain-language theorem explainer
This definition supplies the LogicRealization instance whose carrier is the natural numbers counting moral improvement steps. Workers on the universal forcing chain cite it when embedding an ethical orbit into the arithmetic structure required by NarrativeRealization. The construction is a direct record assignment that delegates the orbit axioms to the LogicNat inductive type and its lemmas.
Claim. The ethics realization is the structure whose carrier is the set of natural numbers, cost function is the ethics cost, zero element is 0, step is the successor, orbit is the inductive type LogicNat, interpretation maps identity to 0 and step to successor, and the remaining fields witness the required identities, injectivity, induction, and nontriviality.
background
MoralImprovementStep is the abbreviation for the carrier type Nat. LogicRealization is the record type that packages a carrier, a cost function, an orbit type, an interpretation map, and the axioms needed to realize logical structure inside the forcing chain. The module states that only the identity/step comparison structure required by UniversalForcing is formalized; the full domain theory of ethics is not rebuilt here.
proof idea
The definition populates the LogicRealization record by setting Carrier to MoralImprovementStep, Cost to Nat, compare to ethicsCost, Orbit to LogicNat, interpret to ethicsInterpret, and the remaining fields to the corresponding constants or lemmas. The interpret_step and orbit_induction fields are proved by rfl and by delegating to LogicNat.induction; orbit_no_confusion uses zero_ne_succ; orbit_step_injective uses succ_injective; nontrivial supplies the witness 1.
why it matters
It supplies the ethical instance required by the UniversalForcing layer so that moral improvement steps can participate in the same orbit structure as arithmetic. The immediate parent is ethics_arith_equiv_nat, which extracts the equivalence (arithmeticOf ethicsRealization).peano.carrier ≃ LogicNat. The construction sits inside the lightweight EthicsRealization module that closes the forcing chain without reopening domain-specific ethics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.