structure definition def or abbrev

`DomainInstance`

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

formal statement (Lean)

 766structure DomainInstance where
 767  /-- Name of the domain -/
 768  name : String
 769  /-- The state space of this domain -/
 770  stateType : Type
 771  /-- How to embed cost into domain-specific measurement -/
 772  costEmbed : ℝ → ℝ
 773  /-- The embedding preserves ordering (monotone) -/
 774  monotone : ∀ a b : ℝ, a ≤ b → costEmbed a ≤ costEmbed b
 775
 776/-- **Qualia domain instance**: strain = phase_mismatch × J(intensity) -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

ethicsDomain in IndisputableMonolith.Algebra.RecognitionCategory decl_use
qualiaDomain in IndisputableMonolith.Algebra.RecognitionCategory decl_use
semanticsDomain in IndisputableMonolith.Algebra.RecognitionCategory decl_use

depends on (12)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
embed in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
embed in IndisputableMonolith.Foundation.HamiltonianEmergence decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
phase_mismatch in IndisputableMonolith.Gap45.RecognitionBarrier decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
Qualia in IndisputableMonolith.Measurement.RSNative.Core decl_use
intensity in IndisputableMonolith.Quantum.DoubleSlit decl_use