LayerSysPlusObj

formal source

 716/-- A linked layer system packages the calibrated cost layer with the
 717    `PhiRing`, `LedgerAlg`, and `OctaveAlg` layers together with the bridge
 718    axioms `(B1)` and `(B2)` from §4.1. -/
 719structure LayerSysPlusObj (n : ℕ) where
 720  costLayer : RecAlgObj
 721  phiLayer : PhiRingObj
 722  ledgerLayer : LedgerAlgObj n
 723  octaveLayer : OctaveAlgObj
 724  bridge_cost_phi : costLayer.cost PhiRing.φ = (Real.sqrt 5 - 2) / 2
 725  bridge_phi_octave : Fintype.card OctaveAlgebra.ModeToken = 20
 726
 727/-- Morphisms in `LayerSys⁺` are tuples of morphisms in the four layer
 728    categories. -/
 729structure LayerSysPlusHom {n : ℕ} (A B : LayerSysPlusObj n) where
 730  costHom : RecAlgHom A.costLayer B.costLayer
 731  phiHom : PhiRingHom A.phiLayer B.phiLayer
 732  ledgerHom : LedgerAlgHom A.ledgerLayer B.ledgerLayer
 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