layerSysPlus_id
plain-language theorem explainer
The declaration constructs the identity morphism for objects in the LayerSys⁺ category. Algebraists formalizing the Recognition Science layer structure cite it when verifying that the four-component systems admit identities compatible with the cost, phi-ring, ledger, and octave subcategories. The definition assembles the four component identity morphisms into a single LayerSysPlusHom tuple.
Claim. For any natural number $n$ and any linked layer system $A$ (a cost algebra object, a phi-ring object, an $n$-dimensional ledger algebra object, and an octave algebra object satisfying the bridge conditions), the identity morphism $id_A : A → A$ in LayerSys⁺ is the tuple whose cost component is the identity in the cost algebra, whose phi component is the identity in the phi ring, whose ledger component is the identity linear map, and whose octave component is the identity additive monoid homomorphism.
background
LayerSysPlusObj packages four calibrated layers: a RecAlgObj for the cost structure, a PhiRingObj, a LedgerAlgObj n, and an OctaveAlgObj, together with explicit bridge axioms such as costLayer.cost PhiRing.φ = (Real.sqrt 5 - 2)/2 and the requirement that the octave algebra has exactly 20 modes. LayerSysPlusHom is the structure whose fields are morphisms in each of these four component categories. The present definition draws on the already-established identity morphisms recAlg_id, phiRing_id, ledgerAlg_id, and octaveAlg_id in the respective subcategories.
proof idea
The definition is a direct structural construction: it supplies the four fields of LayerSysPlusHom by applying recAlg_id to A.costLayer, phiRing_id to A.phiLayer, ledgerAlg_id to A.ledgerLayer, and octaveAlg_id to A.octaveLayer. No tactics or lemmas beyond these component identities are invoked.
why it matters
The identity is required to turn the collection of LayerSysPlusObj and LayerSysPlusHom into a category inside the Recognition Science algebraic development. It supplies the neutral element needed for composition of morphisms that preserve the calibrated cost-phi bridges and the octave periodicity, thereby supporting later statements about the Recognition Composition Law and the eight-tick octave structure. Because the module has no recorded downstream uses yet, the definition remains a foundational scaffolding step for any future categorical treatment of the linked layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.