linFunctional
plain-language theorem explainer
A general linear functional on the debit-credit plane is written by its two real coefficients: on a ledger state $z=(d,c)$ it returns $a d + b c$. Downstream uniqueness theorems cite it to show that any such functional vanishing on the balanced locus is a scalar multiple of net imbalance. The body is the bilinear formula itself; linearity is data, not a comment promise.
Claim. For coefficients $a,b\in\mathbb{R}$ and a ledger state $z=(z_1,z_2)\in\mathbb{R}\times\mathbb{R}$, define the linear functional $\ell_{a,b}(z):=a z_1+b z_2$.
background
This module asks whether the half-imbalance chart used in classical gravity can be derived from recognition primitives on the ledger, or must be stipulated. The local phase space is a ledger state: a debit-credit pair $(d,c)\in\mathbb{R}\times\mathbb{R}$, the same plane whose area form is preserved by sigma-conserving (symplectic) maps in Cost.SymplecticAction.
The balanced ground state is equal debit and credit. Double-entry bookkeeping treats that locus as prior to any cost functional. Part 2 of the module studies linear observables that vanish there; the point of writing the functional by coefficients is that "linear" is a property of the data, not an informal promise. Recognition cost (J-cost on ratios or events) is deliberately absent from this definition.
Upstream cost definitions (observer J-cost, multiplicative-recognizer cost, rung-coarsened totals) supply the broader recognition setting, but this abbreviation does not invoke them.
proof idea
Definitional: expand the pair projection and form the real linear combination $a\cdot z.1+b\cdot z.2$. No lemmas, tactics, or cost identities are required.
why it matters
This is the carrier type for Part 2 of Gap 5 (chart from ledger momentum). It feeds VanishesAtBalanced, the iff characterizations of vanishing on the balanced state or locus, and the uniqueness theorems: every linear observable vanishing at balance is a scalar multiple of net imbalance (imbalance_is_the_unique_linear_selection, imbalance_forced_by_balance_locus), with the special case $\ell_{1,-1}$ recovering imbalance exactly. The tolerated family of such functionals collapses to a scale ray along imbalance (tolerated_family_is_a_scale_ray).
Those facts are assembled into ChartStipulatedVerdict: the four technical parts hold, yet the chart remains stipulated because linearity is a smuggled premise (without it the tolerated family is infinite-dimensional), because event cost and state cost are spliced, and because the remaining ADM identification is logically equivalent to the chart. In the Recognition programme this records a failed attribution on Pillar 1 rather than a derivation of classical gravity from a recognition primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.