LayerSysPlusObj
plain-language theorem explainer
A linked layer system packages the calibrated cost layer with the PhiRing, LedgerAlg, and OctaveAlg layers together with the bridge axioms (B1) and (B2) from section 4.1. Recognition Science modelers cite this structure when assembling the full algebraic model from cost, ring, flow, and periodicity components. The definition is a direct packaging of four layer objects with two explicit numerical bridge conditions.
Claim. An object in the LayerSys⁺ category for natural number $n$ consists of a cost algebra object, a commutative unital ring object with distinguished golden element, a submodule of admissible flows in dimension $n$, and an additive group equivalent to $Z/8Z$, satisfying that the cost of the golden element equals $(√5 - 2)/2$ and that the octave modes have cardinality 20.
background
Recognition Science organizes data into four algebraic layers. The cost layer (RecAlgObj) bundles cost algebra data with the J-cost function. The PhiRingObj carries a commutative unital ring with a distinguished golden element and its inverse. The LedgerAlgObj (n) consists of submodules of admissible flows that are antisymmetric and conserved. The OctaveAlgObj is an additive group explicitly equivalent to ZMod 8, encoding the eight-tick periodicity.
proof idea
The declaration is a direct structure definition that bundles the four layer objects with two explicit equality axioms for the bridges. No lemmas or tactics are applied; it serves as the type for subsequent morphisms and compositions.
why it matters
This structure supplies the object type for the LayerSys⁺ category and feeds the canonicalLayerSysPlus construction together with the composition and identity operations. It assembles the calibrated layers that realize the phi fixed point and the eight-tick octave from the forcing chain, directly supporting the bridge axioms (B1) and (B2) in section 4.1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.