PrimitiveLedgerPostingSemantics
plain-language theorem explainer
Primitive ledger-posting semantics packages the algebraic axioms on a two-variable combiner whose second argument is fed by free defect-ledger costs. Phase-3 work deriving the Recognition Composition Law from the ledger (T4-to-T5) cites this interface. Fields are symmetry, zero-boundary response, unit-diagonal calibration, right-posted additivity on ledger costs, and free-ledger cost additivity. It is a Prop structure, not a uniqueness theorem.
Claim. A map $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ has primitive ledger-posting semantics when: $P(u,v)=P(v,u)$; $P(u,0)=2u$; $P(1,1)=6$; for every index type $I$, weight $w$, and free defect ledgers $\Gamma,\Delta$, the excess $P(u,\mathrm{cost}_w(\Gamma+\Delta))-P(u,0)$ splits as the sum of the excesses on $\Gamma$ and on $\Delta$; and ledger cost is additive, $\mathrm{cost}_w(\Gamma+\Delta)=\mathrm{cost}_w(\Gamma)+\mathrm{cost}_w(\Delta)$.
background
Phase 3 asks that the T4-to-T5 bridge be derived from the recognition ledger rather than assumed analytically. This module isolates the remaining algebraic condition on a two-variable combiner $P$: if $P$ has ledger-linear response in its second argument, then together with symmetry, the boundary law, and the unit diagonal, the d'Alembert factorization gate forces the RCL polynomial.
A defect ledger on $I$ is a finitely supported multiplicity map (the free commutative monoid of primitive distinctions). Its recognition cost under weight $w$ is total weighted multiplicity. The free ledger already proves unconditional additivity of that cost. The defect functional equals the $J$-cost on positives.
Primitive posting is closer to the Phase-2 ledger than discrete posting: the second coordinate of $P$ is fed by actual free-ledger costs, and additive ledger posting is the operation the combiner sees. Discrete posting only sees natural-number rank-one costs after that specialization.
proof idea
No proof body: this is a Prop-valued structure with five fields, packaging axioms rather than deriving them. Downstream lemmas project fields directly. Symmetry, zero-boundary, and unit diagonal copy into discrete posting and the factorization gate. Right-posted additivity plus free-ledger additivity supply the ledger-linear response that yields the gate's right-affine field. Specialization to natural-number rank-one costs is a field-wise projection into the discrete posting structure.
why it matters
This interface is the ledger-side hypothesis that closes Phase 3. Primitive posting plus continuity yields the full factorization associativity gate. With per-slice monotone or antitone regularity it forces $P$ to be the RCL combiner, so any cost that composes through $P$ satisfies the Recognition Composition Law. Downstream composites then finish: ledger composition forces $F=J$ on positives, and the comparison-cost route does the same under reciprocity, normalization, calibration, and continuity, with no analytic composition-law hypothesis assumed.
In the forcing chain this is T4-to-T5 bridge material: once the gate fires, T5 $J$-uniqueness and the RCL are available from ledger structure. Free-ledger additivity is already proved on the floor; packaging it here keeps the combiner axioms self-contained for the gate theorems and the Phase-3 composition certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.