LedgerAlgHom
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not require the linear map to preserve antisymmetry or conservation.
- Does not fix the dimension $n$ or the concrete FlowSpace.
- Does not include composition or identity morphisms.
formal statement (Lean)
592structure LedgerAlgHom {n : ℕ} (A B : LedgerAlgObj n) where
593 map : A.carrier →ₗ[ℝ] B.carrier
594
595/-- The full subspace of antisymmetric conserved flows. -/