module module high

`IndisputableMonolith.Algebra.RecognitionCategory`

The RecognitionCategory module defines the category RecAlg whose objects are cost algebra data bundles equipped with J-cost, phi-ring, ledger, and octave structures. Researchers formalizing categorical aspects of recognition algebras would cite it when building initial objects or verifying composition laws. This is a definition module containing no proofs, only declarations of objects, homomorphisms, identities, and associativity axioms.

claimLet $RecAlg$ be the category whose objects are cost algebra data bundles and whose morphisms are structure-preserving homomorphisms that respect the $J$-cost function and the phi-ring operations.

background

This module resides in the Algebra domain and imports CostAlgebra (which supplies the J-cost function obeying the Recognition Composition Law), PhiRing (which encodes the self-similar fixed point phi), LedgerAlgebra, and OctaveAlgebra. It introduces RecAlgObj as cost algebra data bundles and RecAlgHom as the corresponding morphisms, together with the standard category operations recAlg_id, recAlg_comp, and the initialObject construction.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the categorical framework that supports the initial object and costFamily constructions appearing among its sibling declarations. It provides the algebraic setting required for the forcing chain steps T5 through T8 and for applications of the Recognition Composition Law in later modules.

scope and limits

Does not contain any proved theorems.
Does not specify concrete realizations of the cost algebra bundles.
Does not derive physical constants such as alpha or G.
Does not implement the full UnifiedForcingChain.

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