primitiveLedgerPosting_forces_natAffineResponse
plain-language theorem explainer
If a two-variable combiner satisfies primitive ledger-posting semantics, its second-argument response is affine on natural numbers: P(u,n)=(P(u,1)-P(u,0))·n+P(u,0). Cited by anyone closing the T4-to-T5 ledger-to-factorization bridge without continuum completion. Proof is a one-line specialization through the discrete posting intermediate.
Claim. Let $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ obey primitive ledger-posting semantics: symmetry $P(u,v)=P(v,u)$, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and additive response when the second argument is the cost of summed free defect ledgers. Then for every real $u$ and every natural number $n$, $P(u,n)=(P(u,1)-P(u,0))\cdot n+P(u,0)$.
background
This module isolates the remaining algebraic condition for the Phase-3 T4-to-T5 bridge: derive the d'Alembert factorization gate from the recognition ledger rather than assume it analytically. The free ledger already gives unconditional additivity; if a combiner has ledger-linear response in its second argument, the rightAffine field of the factorization gate follows, and with symmetry, boundary law, and unit diagonal the gate forces the RCL polynomial.
Primitive ledger-posting semantics is the Phase-2-near surface: the second coordinate is fed by costs of actual free defect ledgers, and posting those ledgers additively is the operation the combiner sees. It is stricter than discrete posting, which only talks about natural-number costs after fixing the rank-one unit ledger. Discrete posting already forces the same natural-number affine identity (no real-continuum completion), and primitive posting specializes to discrete posting by restricting to that rank-one surface.
proof idea
One-line term wrapper. First apply the specialization lemma that every combiner with primitive ledger-posting semantics also satisfies discrete ledger-posting semantics (copy symmetry, zero boundary, unit diagonal, and restrict right-ledger additivity to the rank-one natural surface). Then invoke the already-proved discrete theorem: under discrete posting, the map $n\mapsto P(u,n)-P(u,0)$ is additive and nonnegative on naturals, hence linear, which rearranges to the stated affine identity.
why it matters
Closes the primitive-to-natural step of the ledger-to-factorization bridge: the free-ledger posting law already forces affine response on the actual natural rank-one cost surface, without analytic completion. That affine law is exactly the finite-ledger form of right-affineness needed so the d'Alembert factorization gate can fire and force the RCL polynomial $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, the T5 landmark. No downstream consumers are wired yet in the graph; the declaration sits as the primitive-side entry point for later gate applications and for the canonical RCL combiner carrying discrete free-ledger posting before analytic completion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.