LedgerLinearResponse
plain-language theorem explainer
A Prop structure packaging the algebraic hypotheses that turn a two-variable cost combiner into the d'Alembert factorization gate: symmetry, zero-boundary law, unit diagonal, affine response in the second argument, and free-ledger cost additivity. Anyone deriving the Recognition Composition Law from ledger posting rather than analytic input cites this interface. It is a pure structure definition; no proof body.
Claim. A binary combiner $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ has ledger-linear response when: (i) $P(u,v)=P(v,u)$; (ii) $P(u,0)=2u$; (iii) $P(1,1)=6$; (iv) the second argument responds affinely, $P(u,v)=(P(u,1)-P(u,0))\,v+P(u,0)$; (v) recognition cost on defect ledgers is additive, $\mathrm{cost}_w(\Gamma+\Delta)=\mathrm{cost}_w(\Gamma)+\mathrm{cost}_w(\Delta)$ for every weight $w$ and every pair of finitely supported multiplicity ledgers.
background
Phase 3 of the foundation chain asks that the T4-to-T5 bridge be derived from the recognition ledger rather than assumed analytically. The free ledger already proves unconditional additivity of cost. The remaining algebraic condition is that a two-variable combiner respond linearly in its second argument to posted ledger mass.
A defect ledger is the free commutative monoid on an index type $I$: finitely supported multiplicities of primitive distinctions. Recognition cost under a weight $w$ is the total weighted multiplicity $\sum_i n_i,w(i)$. The free-ledger theorem says this cost is additive under pointwise sum of ledgers.
The module isolates the precise package of fields (symmetry, boundary, unit diagonal, right-affine response, and that free additivity) under which the existing factorization gate forces the RCL polynomial $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
proof idea
No proof: this is a structure definition of type $\mathrm{Prop}$. The five fields are the hypotheses later theorems discharge or consume. Downstream constructors such as ledgerLinearResponse_from_free_ledger and ledgerLinearResponse_from_primitiveLedgerPosting fill the fields from weaker posting semantics plus a regularity gate (continuity or per-slice directional monotonicity). Consumers read the fields directly, e.g. factorizationGate_of_ledgerLinearResponse copies symmetry and zero-boundary and derives rightAffine from rightResponse.
why it matters
This is the precise remaining algebraic condition for the ledger-to-factorization bridge. Once inhabited, factorizationGate_of_ledgerLinearResponse yields the full d'Alembert factorization gate, and ledgerLinearResponse_forces_rcl concludes that $P$ equals the RCL combiner everywhere. That is the T4-to-T5 step: ledger posting forces the Recognition Composition Law, which in the forcing chain (T5) uniquely determines $J(x)=(x+x^{-1})/2-1$.
Equivalence with free-ledger combiner semantics (freeLedgerCombinerSemantics_iff_ledgerLinearResponse) and the primitive-posting constructors show the interface is not an extra axiom: it is the completed real form of free additive posting plus a mild regularity hypothesis. The directional (monotone-or-antitone per slice) variant is the non-vacuous order replacement for continuity, consistent with the canonical RCL slope $2(u+1)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.