canonicalLayerSysPlus
plain-language theorem explainer
The definition assembles the canonical cost algebra using the J-cost function, the phi ring on Z[phi], the admissible-flow ledger for parameter n, and the ZMod 8 octave algebra into a single linked layer system. Researchers working on the Recognition Algebra category cite this as the standard base object for deriving domain functors in §5. The construction is a direct record assembly that discharges the cost-phi bridge by simplification against the J_at_phi theorem.
Claim. For each natural number $n$, the canonical linked layer system is the structure whose cost layer is the canonical cost algebra with cost function $J$, whose phi layer is the canonical phi ring object on $Z[phi]$, whose ledger layer is the admissible flows on $n$, whose octave layer is the canonical octave algebra on $Z/8Z$, and whose bridges satisfy $J(phi) = (sqrt(5)-2)/2$ together with the mode-token cardinality condition of 20.
background
The RecognitionCategory module equips the Recognition Algebra with a category structure whose objects are algebras satisfying the Recognition Composition Law. A LayerSysPlusObj n packages four layers: a RecAlgObj supplying the cost function, a PhiRingObj, a LedgerAlgObj n, and an OctaveAlgObj, together with the two bridge axioms (B1) and (B2) from §4.1. The canonicalCostAlgebra supplies the J-cost function that obeys the Recognition Composition Law, is normalized at 1, symmetric under reciprocals, and nonnegative. The upstream J_at_phi theorem states that J(phi) equals (sqrt(5)-2)/2 and identifies this value as the coherence cost of self-similarity, the minimum nonzero cost on the phi-ladder.
proof idea
The definition is a direct record construction that assigns canonicalCostAlgebra to the cost field, canonicalPhiRingObj to the phi field, canonicalLedgerAlgObj n to the ledger field, and canonicalOctaveAlgObj to the octave field. The cost-phi bridge is discharged by a simpa tactic that unfolds canonicalCostAlgebra and invokes the J_at_phi theorem. The phi-octave bridge is supplied directly by the modeToken_card lemma from OctaveAlgebra.
why it matters
This definition supplies the canonical object of the Recognition Algebra category that serves as the source for the domain functors described in the subsequent §5 comment on functors to qualia, ethics, and semantics algebras. It instantiates the linked layer system that carries the J-cost, the phi self-similar fixed point, the eight-tick octave, and the admissible ledger, thereby closing the bridge axioms required by the Recognition Composition Law. The construction therefore provides the concrete base object needed to extend the T5-T8 forcing chain into domain-specific algebras.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.