discreteLedgerPosting_forces_natAffineResponse
plain-language theorem explainer
Discrete ledger posting forces the combiner P to be affine in its second argument on natural ranks: P(u,n)=(P(u,1)-P(u,0))n+P(u,0). Cited by anyone deriving right-affineness for the d'Alembert factorization gate from the recognition ledger rather than assuming it. Proof builds an additive excess map on ℕ, inducts to homogeneity, then rearranges; no continuum completion is used.
Claim. If $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ obeys discrete ledger posting semantics (symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, right natural posted additivity of the excess over $P(u,0)$, and free-ledger additivity), then for every real $u$ and every $n\in\mathbb{N}$, $P(u,n)=(P(u,1)-P(u,0))\cdot n+P(u,0)$.
background
The module is the ledger-to-factorization bridge: Phase 3 asks that the T4-to-T5 step be derived from the recognition ledger instead of taken as an analytic input. The free ledger already gives unconditional additivity; what remains is to turn ledger-linear response in the second argument into the rightAffine field of the d'Alembert factorization gate.
Discrete ledger posting semantics live on the actual rank-one ledger-cost surface with second coordinate restricted to natural numbers (finite multiplicities, before analytic completion). The operative field is right natural posted additivity: $P(u,m+n)-P(u,0)$ splits as the sum of the excesses at $m$ and at $n$. Symmetry, the zero boundary $P(u,0)=2u$, and the unit diagonal $P(1,1)=6$ ride along in the structure but are not consumed by this identity.
The theorem is the finite-ledger form of right-affineness: it converts posted additivity on $\mathbb{N}$ into an affine formula on that discrete surface alone.
proof idea
Fix $u$. Define the excess $R:\mathbb{N}\to\mathbb{R}$ by $R(k):=P(u,k)-P(u,0)$. Right natural posted additivity yields $R(m+n)=R(m)+R(n)$ at once. Induction on $n$ gives $R(n)=n\cdot R(1)$: the zero case is immediate, and the successor step rewrites $R(n+1)=R(n)+R(1)$, substitutes the inductive hypothesis, and clears by ring arithmetic. Unwinding $R$ produces $P(u,n)-P(u,0)=n\cdot(P(u,1)-P(u,0))$; commuting the real factors and a final linear-arithmetic close deliver the affine identity.
why it matters
This supplies the finite-ledger right-affineness that the d'Alembert factorization gate needs, without continuum completion. Its sole downstream consumer is the companion result that primitive ledger posting already forces the same natural affine response (by embedding into discrete semantics and applying this theorem). With symmetry, the boundary law, and the unit diagonal, affine response feeds the existing gate that forces the Recognition Composition Law polynomial, closing the T4-to-T5 bridge toward T5 J-uniqueness. The module's stated goal is exactly this isolation: free-ledger additivity plus ledger-linear response imply the algebraic input the factorization gate demands.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.