areaForm
plain-language theorem explainer
The standard symplectic 2-form on the debit/credit plane: ω(v,w)=v₀w₁−v₁w₀. Anyone treating double-entry ledger maps as linear events on ℝ² cites it as the geometric content of σ=0. It is a one-line definition of the oriented parallelogram area; later lemmas show linear maps scale it by det.
Claim. Define the ledger area form on the two-dimensional debit/credit phase space by $\omega(v,w) := v_0 w_1 - v_1 w_0$ for $v,w\in\mathbb{R}^2$.
background
The module treats a double-entry ledger as a 2D phase space: a state is a pair (debit, credit) ∈ ℝ², and a recognition event is a linear map M : ℝ² → ℝ². The σ = 0 law (no net imbalance created) is identified with preservation of oriented area on that plane.
The form defined here is the classical symplectic area form ω(v,w) = v₀ w₁ − v₁ w₀. For 2×2 real matrices, preserving ω for all pairs is exactly det M = 1, i.e. M ∈ SL(2,ℝ) = Sp(2,ℝ). The module header states this equivalence as the geometric content of σ = 0, not an extra postulate.
Upstream forcing of the cost J itself lives in Cost.FunctionalEquation (RCL plus reciprocity, normalization, calibration, continuity). This definition supplies the independent variational side of the bridge: once area preservation is the group, Cayley–Hamilton yields the SL(2) trace identity that recovers the calibrated trace cost matching J.
proof idea
Pure definition: the body is the bilinear alternating expression v 0 * w 1 - v 1 * w 0 on Fin 2 → ℝ. No lemmas are applied. Downstream, areaForm_mulVec expands mulVec on Fin 2 and rearranges to factor det M; conservesSigma_iff_preservesArea then equates ConservesSigma (det = 1) with pointwise preservation of this form.
why it matters
This is the geometric primitive of the symplectic-ledger bridge. Parent results include areaForm_mulVec (linear maps scale ω by det), conservesSigma_iff_preservesArea (σ = 0 ⇔ area-preserving ⇔ det = 1), and the certificate structure SymplecticActionCert, which packages σ-as-area-preservation with the trace identity and the identification of the calibrated trace cost with J.
Downstream gravity work reuses it: imbalance_total_is_a_canonical_pair shows the imbalance/total chart rescales ω by 2 (hence is symplectic after normalization); ChartStipulatedVerdict imports sigma_is_symplectic; orbitHamiltonian takes ω = dd ∧ dc as the area form for the Casimir Hamiltonian flow on the split torus.
In the framework, this discharges the documented bridge from RCL-forced J to a physical variational principle: the cost is the symplectic action of the double-entry ledger. It sits under T5 J-uniqueness and the RCL, without itself forcing φ, the eight-tick octave, or D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.