factorizationGate_of_primitiveLedgerPosting_nonneg
plain-language theorem explainer
Primitive ledger posting plus cost non-negativity under non-negative defect mass forces the full factorization associativity gate on a two-variable combiner. Researchers closing the T4-to-T5 bridge from ledger axioms (rather than analytic regularity) would cite this. The proof is a one-line composition: non-negativity upgrades primitive posting to ledger-linear response, which already yields the gate.
Claim. Let $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$. Suppose $P$ has primitive ledger-posting semantics: symmetry $P(u,v)=P(v,u)$, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and right additivity when the second argument is the cost of free defect ledgers under additive posting. If moreover $0\le v$ implies $P(u,0)\le P(u,v)$ for all $u,v$, then $P$ satisfies the factorization associativity gate (symmetry, right-affineness $P(u,v)=\alpha_u v+\beta_u$, zero boundary, and unit diagonal).
background
Phase 3 of the foundation chain asks that the T4-to-T5 bridge be derived from the recognition ledger rather than assumed as an analytic input. This module isolates the remaining algebraic condition: free-ledger additivity is already unconditional; if a two-variable combiner has the matching ledger-linear response in its second argument, the right-affine field of the d'Alembert factorization gate follows, and with symmetry, boundary law, and unit diagonal the gate forces the RCL polynomial.
Primitive ledger-posting semantics feeds the second coordinate of $P$ by the cost of actual free defect ledgers, with additive ledger posting as the operation the combiner sees. It packages symmetry, $P(u,0)=2u$, $P(1,1)=6$, and right ledger-posted additivity. The factorization associativity gate is the packaged target: those same boundary and diagonal laws plus, for each fixed $u$, coefficients $\alpha,\beta$ with $P(u,v)=\alpha v+\beta$.
The regularity input is only the order shadow of ledger-cost non-negativity: posting non-negative defect mass never lowers cost. No continuity hypothesis is used.
proof idea
One-line term proof composing two sibling results. First, primitive ledger posting plus the non-negativity hypothesis is upgraded to ledger-linear response (additivity of increments comes from ledger-cost additivity under posting; monotonicity on the non-negative ray comes from the order hypothesis). Second, that linear response is fed to the existing gate theorem, which extracts right-affineness and packages it with the symmetry, zero-boundary, and unit-diagonal fields already present in the posting semantics.
why it matters
Supplies the fully ledger-internal route to right-affineness on the T4-to-T5 bridge: from recognition-ledger structure to the factorization gate that forces the RCL combiner and, downstream in the forcing chain, T5 J-uniqueness $J(x)=(x+x^{-1})/2-1$. The free ledger already proves unconditional additivity; the only extra order input is the non-negativity shadow of ledger cost, not an analytic continuity assumption. The module doc states the program explicitly: ledger-linear response plus symmetry, boundary law, and unit diagonal let the existing gate theorem force the RCL polynomial. No recorded downstream consumers yet; the declaration is a terminal packaging theorem for the primitive-posting path inside the Ledger-to-Factorization bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.