strictEthicsRealization
This definition assembles a StrictLogicRealization for the ethics domain by equipping the ActionState carrier with Nat costs, minimalImprovement as generator, and ethicalZero as unit. Workers on admissible realizations cite it to witness the ethics component of the four canonical domains. The body is a direct record that wires sibling cost and composition functions into the required fields, with one law discharged by simp.
claimThe strict ethics realization is the StrictLogicRealization whose carrier consists of action states (pairs of agent identifier and improvement rank), whose cost function returns 0 on identical states and 1 otherwise, whose composition is preference composition, whose generator is the minimal improvement step, and whose unit is ethical zero, satisfying the self-cost, symmetry, and nontriviality laws.
background
ActionState is the structure with fields agent : Nat and improvementRank : Nat. The cost function actionCost returns 0 precisely when the two states coincide and 1 otherwise; its self and symmetry properties are already established by direct case analysis. The module sets the local setting as a domain-rich ethical realization whose generator is the smallest recognized improvement step. Upstream, compose from VirtueComposition supplies the additive structure on sigma changes and multipliers, while the one constants from IntegersFromLogic and RationalsFromLogic supply the arithmetic units used in the lightweight orbit equivalence.
proof idea
The definition is a direct record that assigns Carrier to ActionState, Cost to Nat, compare to actionCost, compose to preferenceCompose, one to ethicalZero, and generator to minimalImprovement. The identity, non-contradiction, and excluded-middle laws are set to the corresponding theorems or True. The nontrivial law is discharged by a single simp tactic that unfolds actionCost, minimalImprovement, and ethicalZero.
why it matters in Recognition Science
It supplies the ethics_adm witness required by AdmissibleClassCert and four_canonical_domains_admissible, which together establish that all four canonical domains admit the universal forcing equivalence. The construction closes the strict metaphysical package by providing the arithmetic equivalence to LogicNat via toLightweight. It directly instantiates the generator-as-smallest-improvement step described in the module doc-comment.
scope and limits
- Does not derive any new cost identities beyond the wired siblings.
- Does not address continuous or probabilistic extensions of the cost function.
- Does not prove the full universal forcing equivalence; that is supplied by StrictLogicRealization.
- Does not constrain the agent or improvementRank coordinates beyond their Nat type.
Lean usage
noncomputable def ethics_admissible : AdmissibleRealization Ethics.strictEthicsRealization := by refine ⟨?_, ?_, Or.inl ?_⟩; · intro a b; exact decEq (Ethics.actionCost a b) 0; · exact RichDomainCosts.EthicsRich.preferenceCompose_assoc; · show Ethics.preferenceCompose Ethics.ethicalZero Ethics.ethicalZero = Ethics.ethicalZeroformal statement (Lean)
42def strictEthicsRealization : StrictLogicRealization where
43 Carrier := ActionState
proof body
Definition body.
44 Cost := Nat
45 zeroCost := inferInstance
46 compare := actionCost
47 compose := preferenceCompose
48 one := ethicalZero
49 generator := minimalImprovement
50 identity_law := actionCost_self
51 non_contradiction_law := actionCost_symm
52 excluded_middle_law := True
53 composition_law := True
54 invariance_law := True
55 nontrivial_law := by
56 simp [actionCost, minimalImprovement, ethicalZero]
57