LedgerAlgHom
plain-language theorem explainer
LedgerAlgHom defines morphisms in the LedgerAlg category as linear maps between admissible-flow subspaces. Algebraists assembling Recognition Science's layered categories cite it when building composite morphisms for flow conservation. The declaration is a direct structure definition specifying only the map field.
Claim. A morphism from admissible-flow object $A$ to $B$ is a linear map $A.carrier →_ℝ B.carrier$, where each object is a submodule of FlowSpace $n$ closed under antisymmetry and conservation.
background
LedgerAlgObj consists of submodules of FlowSpace $n$ satisfying antisymmetry and conservation of flows. The RecognitionCategory module assembles four parallel categories (cost, phi, ledger, octave) whose morphisms compose under the Recognition Composition Law. Upstream LedgerAlgObj supplies the objects; the present structure supplies the corresponding hom-sets.
proof idea
The declaration is the structure definition itself, introducing the single field map as a linear map between carriers. No lemmas or tactics are invoked.
why it matters
LedgerAlgHom supplies the hom-sets for the ledger layer, which LayerSysPlusHom bundles with cost, phi, and octave morphisms to form the full RecognitionCategory. It directly enables the composition and identity operations ledgerAlg_comp, ledgerAlg_id, and their associativity and unit theorems. The construction supports the algebraic backbone of the T0-T8 forcing chain and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.