def
definition
layerSysPlus_comp
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Algebra.RecognitionCategory on GitHub at line 743.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
740 octaveHom := octaveAlg_id A.octaveLayer
741
742/-- Composition in `LayerSys⁺`. -/
743def layerSysPlus_comp {n : ℕ} {A B C : LayerSysPlusObj n}
744 (g : LayerSysPlusHom B C) (f : LayerSysPlusHom A B) : LayerSysPlusHom A C where
745 costHom := recAlg_comp g.costHom f.costHom
746 phiHom := phiRing_comp g.phiHom f.phiHom
747 ledgerHom := ledgerAlg_comp g.ledgerHom f.ledgerHom
748 octaveHom := octaveAlg_comp g.octaveHom f.octaveHom
749
750/-- The canonical linked system built from the verified cost, `φ`, ledger, and
751 octave layers. -/
752noncomputable def canonicalLayerSysPlus (n : ℕ) : LayerSysPlusObj n where
753 costLayer := canonicalCostAlgebra
754 phiLayer := canonicalPhiRingObj
755 ledgerLayer := canonicalLedgerAlgObj n
756 octaveLayer := canonicalOctaveAlgObj
757 bridge_cost_phi := by
758 simpa [canonicalCostAlgebra] using PhiRing.J_at_phi
759 bridge_phi_octave := OctaveAlgebra.modeToken_card
760
761/-! ## §5. Functors to Domain Algebras -/
762
763/-- A **domain instance** is a functor from RecAlg to a specific domain.
764 Each domain algebra (qualia, ethics, semantics, etc.) is obtained by
765 applying such a functor to the canonical Recognition Algebra. -/
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) -/