FreeLedgerCombinerSemantics
plain-language theorem explainer
Free-ledger combiner semantics is the Prop bundle a bivariate map P must satisfy to sit on the recognition ledger: symmetry, boundary law P(u,0)=2u, unit diagonal P(1,1)=6, additive centered response in the second argument, continuity in that argument, and free defect-ledger cost additivity. Anyone deriving the T4-to-T5 factorization bridge from ledger posting cites this interface. It is a definitional structure, deliberately weaker than full ledger-linear response so Cauchy linearization stays a theorem.
Claim. A map $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ has free-ledger combiner semantics when (i) $P(u,v)=P(v,u)$ for all $u,v$; (ii) $P(u,0)=2u$; (iii) $P(1,1)=6$; (iv) the centered second-argument response is additive: $P(u,v+w)-P(u,0)=(P(u,v)-P(u,0))+(P(u,w)-P(u,0))$; (v) $v\mapsto P(u,v)$ is continuous for each fixed $u$; (vi) free defect-ledger cost is additive under ledger sum for every index type, weight, and pair of defect ledgers.
background
Phase 3 of the foundation 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 the right-affine field of the d'Alembert factorization gate follows, and with symmetry, the zero-boundary law, and the unit diagonal the gate forces the Recognition Composition Law (RCL) polynomial.
The free ledger already proves unconditional cost additivity. Defect is the J-cost on positive ratios ($J(x)=(x+x^{-1})/2-1$), and ledger cost sums weighted defects over a defect ledger. The present structure records additive posting of real increments in the second coordinate plus a continuity gate, without baking in full $\mathbb{R}$-linearity.
Compared with ledger-linear response (which asserts $P(u,v)=(P(u,1)-P(u,0))v+P(u,0)$ outright) and with discrete posting semantics (restricted to natural-number ledger costs on the rank-one surface), free-ledger semantics is the intermediate completed interface: real additive response plus continuity, with free-ledger additivity pinned as a field rather than prose.
proof idea
Definitional Prop structure with no proof body. Six fields package the semantic interface: three shared gate axioms (symmetry, zero boundary, unit diagonal), the weaker right-posted additivity law on centered increments $P(u,\cdot)-P(u,0)$, pointwise continuity in the second argument, and the free-ledger cost-additivity identity over arbitrary index types and defect ledgers. Cauchy linearization from additive continuous response to full ledger-linear response is intentionally left to downstream theorems rather than encoded as a field.
why it matters
This is the completed free-ledger semantic bridge in the ledger-to-factorization path toward T5 (J-uniqueness) and the RCL. Downstream, free-ledger semantics is shown equivalent to ledger-linear response (via continuous additive response implying $\mathbb{R}$-linearity), equivalent to rational completed ledger posting, and equivalent to $P$ being the canonical RCL combiner. Primitive ledger posting plus continuity constructs an instance; the canonical RCL combiner itself carries free-ledger semantics.
The module goal is explicit: free-ledger additivity is already unconditional; once the combiner matches this response law, the right-affine field of the d'Alembert factorization gate follows, and the existing gate theorem forces the RCL polynomial. That closes the Phase-3 demand that T4-to-T5 be ledger-derived rather than an analytic input. Landmarks: T5 J-uniqueness, the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, and the factorization forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.