def definition def or abbrev

`ethicsDomain`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 784noncomputable def ethicsDomain : DomainInstance where
 785  name := "Ethics (DREAM)"

proof body

Definition body.

 786  stateType := Unit  -- Placeholder for moral state
 787  costEmbed := fun j => j  -- J-cost IS moral imbalance
 788  monotone := fun _ _ h => h
 789
 790/-- **Semantics domain instance**: defect = distance to structured set -/

depends on (5)

Lean names referenced from this declaration's body.

DomainInstance in IndisputableMonolith.Algebra.RecognitionCategory decl_use
defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use