def
definition
layerSysPlus_id
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Algebra.RecognitionCategory on GitHub at line 736.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
733 octaveHom : OctaveAlgHom A.octaveLayer B.octaveLayer
734
735/-- Identity morphism in `LayerSys⁺`. -/
736def layerSysPlus_id {n : ℕ} (A : LayerSysPlusObj n) : LayerSysPlusHom A A where
737 costHom := recAlg_id A.costLayer
738 phiHom := phiRing_id A.phiLayer
739 ledgerHom := ledgerAlg_id A.ledgerLayer
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