layerSysPlus_comp
plain-language theorem explainer
Defines the composition of morphisms in LayerSys⁺ by delegating componentwise to the recognition algebra, phi-ring, ledger algebra, and octave algebra compositions. Modelers building the full linked layer system from calibrated cost, phi, ledger, and octave layers cite this when assembling the category structure. The definition is a direct wrapper that applies the four underlying component compositions to the respective homomorphism fields.
Claim. For objects $A,B,C$ of the linked layer system LayerSys⁺(n) and morphisms $g:B→C$, $f:A→B$ whose components are homomorphisms in the recognition algebra, phi-ring, ledger algebra, and octave algebra, the composite $g∘f$ is the morphism whose recognition-algebra component is the composite of the cost homomorphisms, whose phi-ring component is the composite of the phi homomorphisms, and likewise for the ledger and octave components.
background
LayerSysPlusObj n packages a RecAlgObj (cost layer), PhiRingObj, LedgerAlgObj n, and OctaveAlgObj together with bridge axioms (B1) relating cost to phi and (B2) fixing octave cardinality at 20. LayerSysPlusHom is the structure whose fields are parallel homomorphisms, one per layer. The upstream results supply the component compositions: recAlg_comp on recognition algebra homs, phiRing_comp on phi-ring maps, ledgerAlg_comp on ledger maps, and octaveAlg_comp on octave maps, each defined by direct composition of the underlying functions or linear maps.
proof idea
The definition is a direct one-line wrapper that applies recAlg_comp to the costHom fields, phiRing_comp to the phiHom fields, ledgerAlg_comp to the ledgerHom fields, and octaveAlg_comp to the octaveHom fields.
why it matters
This definition supplies the composition operation required for LayerSys⁺ to function as a category whose objects are the canonical linked systems built from the verified cost, phi, ledger, and octave layers. It integrates the recognition algebra (tied to J-cost and the Recognition Composition Law), the phi-ring (self-similar fixed point), and the octave layer (eight-tick period) into a single morphism structure. No downstream uses are recorded, so it serves as internal scaffolding for the RecognitionCategory module rather than feeding a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.