module module high

`IndisputableMonolith.Algebra.RecognitionCategory`

RecognitionCategory defines the category RecAlg whose objects are cost algebra data bundles assembled from four imported algebras. Algebraists working on Recognition Science foundations cite it when constructing morphisms or initial objects in this setting. It is a definition module that organizes imported structures into categorical form without internal proofs.

claimThe category $\mathrm{RecAlg}$ whose objects are cost algebra data bundles, equipped with morphisms $\mathrm{RecAlgHom}$, identities, and composition satisfying associativity.

background

This module introduces the category RecAlg in the algebra domain. It imports CostAlgebra for underlying cost structures, PhiRing for phi-ladder operations, LedgerAlgebra for defect and cost tracking, and OctaveAlgebra for eight-tick periodicity. The module doc comment states that objects in RecAlg are cost algebra data bundles.

Sibling declarations define RecAlgObj, RecAlgHom, recAlg_id, recAlg_comp, recAlg_comp_assoc, initialObject, and costFamily, indicating the module assembles a complete category on the imported components.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the categorical infrastructure for Recognition Algebra, enabling sibling constructions such as initial morphisms and cost families. It organizes data bundles to support the Recognition Composition Law and related identities from the upstream CostAlgebra, PhiRing, LedgerAlgebra, and OctaveAlgebra modules.

scope and limits

Does not contain theorem statements or proofs.
Does not define numerical constants such as phi or alpha.
Does not provide concrete instances of RecAlg objects.
Does not connect objects to physical forcing chain steps T0-T8.

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Algebra.CostAlgebra module_import
IndisputableMonolith.Algebra.LedgerAlgebra module_import
IndisputableMonolith.Algebra.OctaveAlgebra module_import
IndisputableMonolith.Algebra.PhiRing module_import

declarations in this module (65)

abbrev RecAlgObj L55
abbrev RecAlgHom L58
def recAlg_id L61
def recAlg_comp L65
theorem recAlg_comp_assoc L70
theorem recAlg_id_left L77
theorem recAlg_id_right L83
def initialObject L92
def initial_morphism_exists L96
def costFamily L113
theorem costFamily_one_eq_J L117
theorem costFamily_unit L123
def powerMap L129
theorem powerMap_pos L132
theorem powerMap_mul L138
theorem costFamily_comp_powerMap L145
theorem costFamily_neg_param L152
structure CostAlgObjKappa L159
structure CostAlgHomKappa L169
def costAlgKappaInitial L255
theorem costAlgKappaInitial_cost_eq_J L260
structure CostAlgPlusObj L321
structure CostAlgPlusHom L332
def costAlgPlusInitial L390
theorem costAlgPlusInitial_cost_eq_J L395
theorem costAlgPlus_initiality L446
structure PhiRingObj L459
structure PhiRingHom L485
def phiRing_id L495
def phiRing_comp L505
def canonicalPhiRingObj L531
theorem phiRing_comp_assoc L556
theorem phiRing_id_left L563
theorem phiRing_id_right L569
abbrev FlowSpace L575
def IsAntisymmetricFlow L578
def IsConservedFlow L582
structure LedgerAlgObj L586
structure LedgerAlgHom L592
def admissibleFlows L596
def canonicalLedgerAlgObj L631
def ledgerAlg_id L641
def ledgerAlg_comp L645
theorem ledgerAlg_comp_assoc L650
theorem ledgerAlg_id_left L657
theorem ledgerAlg_id_right L663
structure OctaveAlgObj L669
structure OctaveAlgHom L678
def canonicalOctaveAlgObj L682
def octaveAlg_id L689
def octaveAlg_comp L693
theorem octaveAlg_comp_assoc L698
theorem octaveAlg_id_left L705
theorem octaveAlg_id_right L711
structure LayerSysPlusObj L719
structure LayerSysPlusHom L729
def layerSysPlus_id L736
def layerSysPlus_comp L743
def canonicalLayerSysPlus L752
structure DomainInstance L766
def qualiaDomain L777
def ethicsDomain L784
def semanticsDomain L791
theorem monotone_preserves_argmin L802
theorem category_certificate L825