DiscreteLedgerPostingSemantics
plain-language theorem explainer
Packages the discrete posting axioms for a two-variable combiner P on the rank-one ledger-cost surface, with the second argument restricted to natural-number costs from finite multiplicities. The fields are symmetry, the boundary law P(u,0)=2u, the unit diagonal P(1,1)=6, additivity of posted increments along ℕ, and free-ledger cost additivity. Downstream results cite it to force affine response on the finite ledger without continuum completion. Pure definitional structure; no proof body.
Claim. A map $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ has discrete ledger posting semantics when: (i) $P(u,v)=P(v,u)$; (ii) $P(u,0)=2u$; (iii) $P(1,1)=6$; (iv) for all real $u$ and naturals $m,n$, the posted increment $P(u,m+n)-P(u,0)$ equals the sum of the increments at $m$ and at $n$; (v) for every index type $I$, weight $w:I\to\mathbb{R}$, and finitely supported defect ledgers $\Gamma,\Delta$, the weighted ledger cost of $\Gamma+\Delta$ equals the sum of the costs of $\Gamma$ and $\Delta$.
background
Module setting is the Ledger-to-Factorization bridge: Phase 3 derives the T4-to-T5 gate from the recognition ledger rather than taking analytic input. The free ledger already has unconditional additivity; the remaining algebraic condition is a two-variable combiner with ledger-linear response in its second argument, plus symmetry, boundary law, and unit diagonal, so the d'Alembert factorization gate forces the RCL polynomial.
A defect ledger is a finitely supported multiplicity map $I\to_0\mathbb{N}$ (the free commutative monoid on primitive distinctions). Its recognition cost under weights $w$ is the total weighted multiplicity $\sum n_i w_i$. Discrete posting restricts the second coordinate of $P$ to natural-number ledger costs produced by finite multiplicities, before any analytic completion to the continuum.
Upstream, the free-ledger and primitive-posting packages supply the same symmetry, zero-boundary, and unit-diagonal fields; the discrete variant weakens the second-argument law to ℕ-additivity of posted increments and records free-ledger cost additivity explicitly.
proof idea
Definitional structure (structure ... : Prop), not a proved theorem. The five fields are the axioms themselves: three shared gate conditions (symmetry, zero boundary, unit diagonal), natural-number posted additivity of increments $P(u,\cdot)-P(u,0)$ along $\mathbb{N}$, and free-ledger cost additivity under ledger sum. No tactics or lemmas; inhabitants are built by supplying proofs of each field (as in the specialization from primitive posting and the check that the canonical RCL combiner satisfies the package).
why it matters
This is the finite-ledger surface used to force right-affineness without continuum completion. The parent theorem discreteLedgerPosting_forces_natAffineResponse concludes $P(u,n)=(P(u,1)-P(u,0))\cdot n+P(u,0)$ for all natural $n$, the discrete form of the right-affine field the factorization gate needs. Specialization from primitive posting shows the discrete package is weaker and inherited; the canonical RCL combiner is shown to carry these semantics before analytic completion.
In the forcing chain this sits on the T4-to-T5 bridge: once discrete (then continuum) right-affineness is in hand with symmetry, boundary, and unit diagonal, the existing gate forces the Recognition Composition Law polynomial and thence J-uniqueness (T5). It also feeds the free-ledger combiner semantics package used elsewhere in the same bridge file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.