ledgerLinearResponse_from_rationalLedgerPosting
plain-language theorem explainer
Rational ledger posting plus continuity upgrades the affine response law from rationals to all reals, producing full ledger-linear response for a two-variable combiner. Anyone closing the free-ledger bridge to the d'Alembert factorization gate cites this. The proof identifies two continuous functions that agree on the dense rationals and invokes the dense-range equalizer.
Claim. Let $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ be symmetric, satisfy $P(u,0)=2u$ and $P(1,1)=6$, be continuous in its second argument, obey the affine identity $P(u,q)-P(u,0)=q\,(P(u,1)-P(u,0))$ for every rational $q$, and inherit free-ledger additivity. Then $P$ has full real right-response: $P(u,v)=(P(u,1)-P(u,0))\,v+P(u,0)$ for all real $u,v$.
background
This module isolates the remaining algebraic condition in the Phase-3 bridge from the recognition ledger to d'Alembert factorization (the T4-to-T5 step). The free ledger already supplies unconditional additivity. What remains is a two-variable combiner whose second argument responds linearly to posted ledger mass; together with symmetry, the boundary law, and the unit diagonal, that response feeds the existing factorization gate and forces the RCL polynomial.
Rational posting semantics is the analytic-completion input: on the countable positive-ratio surface the affine response law already holds, and the response is continuous in the completed real coordinate. Ledger-linear response is the stronger real statement in which the second argument is governed everywhere by its response to one unit of posted mass, with free-ledger additivity pinned as an explicit field rather than prose.
The zero-boundary convention $P(u,0)=2u$ and the unit-diagonal normalization $P(1,1)=6$ are shared by both structures and match the cost conventions used downstream by the factorization gate.
proof idea
Build the target structure by copying symmetry, zero-boundary, unit-diagonal, and free-ledger additivity from the hypothesis. The only remaining field is full real right-response.
Fix $u$ and define $f(x)=P(u,x)-P(u,0)$ and $g(x)=x,(P(u,1)-P(u,0))$. Continuity of $f$ follows from right-continuity of $P$ minus a constant; $g$ is continuous as a scalar multiple of the identity. The two maps agree on $\mathbb{Q}$ by the rational affine field. Since the rationals are dense in $\mathbb{R}$, the dense-range equalizer lemma yields $f=g$ on all reals. Evaluating at $v$ and rearranging (with a trivial commutation of the scalar product) gives the required identity.
why it matters
This is the reverse half of the equivalence between rational posting-plus-continuity and completed ledger-linear response. The parent theorem rationalLedgerPosting_iff_ledgerLinearResponse quotes it as the dense-rational completion direction; the forward direction is purely algebraic.
In the Recognition forcing chain this closes the ledger-side input to the T4-to-T5 bridge: once the combiner has ledger-linear response, the d'Alembert gate produces the RCL polynomial, and T5 uniqueness then forces $J(x)=(x+x^{-1})/2-1$. Without the dense completion step the free ledger would only control a countable surface, leaving the real factorization gate unforced.
The result is fully proved (no sorry). It does not itself derive continuity or the rational affine law; those remain the analytic hypotheses that later calibration or measure-forcing work must discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.