pith. machine review for the scientific record. sign in
def definition def or abbrev high

canonicalLayerSysPlus

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 752noncomputable def canonicalLayerSysPlus (n : ℕ) : LayerSysPlusObj n where
 753  costLayer := canonicalCostAlgebra

proof body

Definition body.

 754  phiLayer := canonicalPhiRingObj
 755  ledgerLayer := canonicalLedgerAlgObj n
 756  octaveLayer := canonicalOctaveAlgObj
 757  bridge_cost_phi := by
 758    simpa [canonicalCostAlgebra] using PhiRing.J_at_phi
 759  bridge_phi_octave := OctaveAlgebra.modeToken_card
 760
 761/-! ## §5. Functors to Domain Algebras -/
 762
 763/-- A **domain instance** is a functor from RecAlg to a specific domain.
 764    Each domain algebra (qualia, ethics, semantics, etc.) is obtained by
 765    applying such a functor to the canonical Recognition Algebra. -/

depends on (18)

Lean names referenced from this declaration's body.