def
definition
actionCost_decidable
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts on GitHub at line 144.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
141 · simp [h]
142 · simp [h]
143
144def actionCost_decidable (a b : ActionState) : Decidable (a = b) :=
145 inferInstance
146
147theorem preferenceCompose_assoc (a b c : ActionState) :
148 preferenceCompose (preferenceCompose a b) c =
149 preferenceCompose a (preferenceCompose b c) := by
150 unfold preferenceCompose
151 congr 1
152 exact Nat.add_assoc _ _ _
153
154theorem preferenceCompose_left_id (a : ActionState) :
155 preferenceCompose ethicalZero a =
156 { agent := ethicalZero.agent, improvementRank := a.improvementRank } := by
157 unfold preferenceCompose ethicalZero
158 congr 1
159 simp
160
161end EthicsRich
162
163/-! ## Metaphysical -/
164
165namespace MetaphysicalRich
166
167open Metaphysical
168
169/-- The metaphysical ground supplies an invariant equivalence on arithmetics. -/
170noncomputable def metaphysical_ground_invariant
171 (R S : StrictLogicRealization) :
172 (StrictLogicRealization.arith R).peano.carrier
173 ≃ (StrictLogicRealization.arith S).peano.carrier :=
174 ArithmeticOf.equivOfInitial (StrictLogicRealization.arith R)