areaForm_mulVec
plain-language theorem explainer
A 2×2 real linear map scales the ledger area form by its determinant: ω(Mv, Mw) = (det M) ω(v, w). Anyone identifying σ-conservation with Sp(2,ℝ) area preservation cites this. The proof expands the matrix-vector product on Fin 2, substitutes the 2×2 determinant formula, and closes by ring.
Claim. For any $2\times 2$ real matrix $M$ and vectors $v,w\in\mathbb{R}^2$, the ledger area form satisfies $\omega(Mv, Mw) = (\det M)\,\omega(v,w)$, where $\omega(v,w)=v_0 w_1-v_1 w_0$.
background
The module treats a double-entry ledger as a two-dimensional phase space with states (debit, credit) ∈ ℝ². A recognition event is a linear map M : ℝ² → ℝ². The ledger symplectic area form is the standard alternating bilinear form ω(v,w) = v₀ w₁ − v₁ w₀ on that phase space (def areaForm).
σ = 0 conservation (no net imbalance created) is identified with preservation of this area form. For 2×2 maps, area preservation is exactly det M = 1, i.e. M ∈ SL(2,ℝ) = Sp(2,ℝ). The present lemma is the elementary scaling identity that makes that equivalence quantitative: any linear map multiplies areas by its determinant.
Upstream, areaForm is the bare definition of ω. Downstream equivalences (σ-conservation ↔ area preservation ↔ det = 1) and chart changes that rescale ω by a constant both rest on this identity.
proof idea
Tactic proof, purely algebraic. First prove a componentwise expansion: (M · u)i = M{i0} u_0 + M_{i1} u_1 for each coordinate i ∈ Fin 2, by unfolding mulVec and summing over Fin 2. Then unfold areaForm on both sides, substitute that expansion, and replace det M by the Fin-2 formula M₀₀ M₁₁ − M₀₁ M₁₀. The resulting polynomial identity is discharged by ring.
why it matters
This is the computational engine behind the module's bridge from ledger bookkeeping to symplectic geometry. The parent theorem conservesSigma_iff_preservesArea states that σ = 0 iff the map preserves ω for all pairs iff det M = 1; one direction applies this lemma and cancels det = 1. Downstream in Gap5, imbalance_total_is_a_canonical_pair rewrites ω under the imbalance/total chart via areaForm_mulVec and the chart's determinant 2, concluding the imbalance is a momentum conjugate to the total in the substrate's own symplectic structure.
In the broader Recognition chain this supports the identification of J-cost with the calibrated SL(2) trace functional (traceCost M = ½ tr M − 1), which the module derives from the SL(2) trace identity forced by area preservation. That is the physical variational reading of the RCL-forced J (T5), not an extra postulate. Without the det-scaling of ω, the σ ↔ Sp(2) dictionary does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.