canonicalLedgerAlgObj
plain-language theorem explainer
The definition supplies the canonical object in the ledger algebra by taking the full submodule of all antisymmetric conserved flows in the n-dimensional flow space. Algebraists assembling layered recognition structures cite it when building the complete system from cost, phi, ledger, and octave components. The construction is a direct structure instance that delegates the two required properties to the admissibleFlows definition via field projection.
Claim. For each natural number $n$, the canonical ledger object is the submodule of the flow space consisting of all flows that are both antisymmetric and conserved.
background
In the RecognitionCategory module the ledger algebra is built from subspaces of admissible flows. The LedgerAlgObj structure for a fixed $n$ consists of a carrier submodule of FlowSpace n together with the two properties that every element of the carrier is antisymmetric and conserved. The admissibleFlows definition supplies exactly this full submodule by collecting all flows satisfying both conditions simultaneously.
proof idea
The definition is a structure constructor that sets the carrier field directly to admissibleFlows n. The antisymm field is filled by a tactic that introduces an element and projects out the first conjunct of its defining pair. The conserved field is filled by the symmetric projection of the second conjunct.
why it matters
This definition provides the ledger layer inside canonicalLayerSysPlus, which assembles the verified cost algebra, phi ring, ledger algebra, and octave algebra into a single linked system. It realizes the complete admissible flow space as the canonical object, supporting applications of the Recognition Composition Law at the algebra level and interfacing with the foundational Identity property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.