`preferenceCompose_left_id`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts
domain: Foundation
line: 154 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts on GitHub at line 154.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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)
 175    (StrictLogicRealization.arith S)
 176
 177end MetaphysicalRich
 178
 179/-! ## Master cert -/
 180
 181structure RichDomainCostsCert where
 182  music_compose_assoc : ∀ a b c : Music.FrequencyRatio,
 183      Music.strictMusicRealization.compose
 184        (Music.strictMusicRealization.compose a b) c =

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.