LayerSysPlusHom
LayerSysPlusHom defines morphisms in the LayerSys⁺ category as quadruples consisting of a cost morphism, a PhiRing homomorphism preserving the golden element, a linear map on ledger carriers, and an additive map on octave carriers between two LayerSysPlusObj instances. Recognition Science researchers assembling the integrated layer category cite this when building morphism data for linked systems that incorporate the bridge axioms. The declaration is a bare structure definition with no proof obligations or additional constraints.
claimA morphism from linked layer system $A$ to $B$ (each packaging a cost layer, a golden-ratio ring layer, an $n$-dimensional ledger flow space, and an octave algebra layer) consists of a cost morphism $A$.costLayer to $B$.costLayer, a ring homomorphism $A$.phiLayer to $B$.phiLayer sending the distinguished golden element to its counterpart, a linear map $A$.ledgerLayer.carrier to $B$.ledgerLayer.carrier over the reals, and an additive homomorphism $A$.octaveLayer.carrier to $B$.octaveLayer.carrier.
background
LayerSysPlusObj packages four layers into a single object: the RecAlgObj carrying cost data, the PhiRingObj with its distinguished golden element, the LedgerAlgObj n whose carrier holds admissible flows, and the OctaveAlgObj whose carrier is the eight-tick structure, together with the explicit bridge equations linking cost to phi and fixing the octave cardinality at 20. Each layer supplies its own notion of morphism: cost morphisms via the RecAlgHom abbreviation, ring homomorphisms that preserve addition, multiplication, and the golden element, linear maps on the ledger carriers, and additive maps on the octave carriers. The module Algebra.RecognitionCategory assembles these into a single category whose objects satisfy the bridge axioms (B1) and (B2) from section 4.1.
proof idea
The declaration is a structure definition that simply declares four independent fields; it performs no computation and imposes no proof obligations beyond the component homomorphism types already defined in the sibling structures.
why it matters in Recognition Science
LayerSysPlusHom supplies the morphism type required by the downstream definitions layerSysPlus_id and layerSysPlus_comp, thereby completing the category structure on LayerSys⁺. This categorical packaging directly supports the Recognition Science program of deriving physics from a single functional equation by furnishing the algebraic setting in which the forcing chain T0-T8, the Recognition Composition Law, and the phi-ladder mass formula can be expressed uniformly across the four layers.
scope and limits
- Does not impose any cross-layer compatibility conditions between the four homomorphisms.
- Does not act on or preserve the bridge axioms of the underlying LayerSysPlusObj instances.
- Applies only when the dimension parameter n matches on source and target objects.
- Does not define composition or identities; those are supplied by separate declarations.
- Does not address functoriality with respect to J-cost or defectDist operations.
formal statement (Lean)
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⁺`. -/