factorizationGate_of_primitiveLedgerPosting
plain-language theorem explainer
Primitive ledger-posting semantics for a two-argument combiner P, plus continuity in the second slot, already imply the full d'Alembert factorization associativity gate on P. Anyone closing the T4-to-T5 ledger bridge cites this to upgrade free-defect posting to the packaged gate (symmetry, right-affinity, zero boundary, unit diagonal). The proof is a two-step composition: primitive posting yields ledger-linear response, which yields the gate.
Claim. Let $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$. Suppose $P$ is symmetric, obeys the zero boundary $P(u,0)=2u$ and the unit diagonal $P(1,1)=6$, and is additive in the second argument when that argument is the cost of a free defect ledger (primitive ledger-posting). If moreover $v\mapsto P(u,v)$ is continuous for every fixed $u$, then $P$ satisfies the factorization associativity gate: symmetry, right-affinity ($P(u,v)=\alpha_u v+\beta_u$), zero boundary, and unit diagonal.
background
Phase 3 of the foundation asks that the T4-to-T5 bridge be derived from the recognition ledger rather than taken as an analytic input. This module isolates the remaining algebraic condition: if a two-variable combiner has ledger-linear response in its second argument, the rightAffine field of the d'Alembert factorization gate follows; with symmetry, the boundary law, and the unit diagonal, the existing gate theorem forces the Recognition Composition Law polynomial.
Primitive ledger-posting semantics is the structure closest to the Phase-2 free defect ledger. Its second coordinate is fed by actual free-ledger costs, and additive posting of ledgers is exactly the operation the combiner sees. It packages symmetry $P(u,v)=P(v,u)$, the zero boundary $P(u,0)=2u$, the unit diagonal $P(1,1)=6$, and right-ledger-posted additivity on free defect ledgers.
The target gate FactorizationAssociativityGate is the packaged combiner gate used by the factorization/associativity bridge: the same symmetry, boundary, and diagonal, plus right-affinity (for each $u$ there exist $\alpha,\beta$ with $P(u,v)=\alpha v+\beta$). Upstream, ledger-linear response is the intermediate completed real response obtained from free-ledger combiner semantics; the theorem ledgerLinearResponse_from_primitiveLedgerPosting already lifts primitive posting plus continuity to that intermediate.
proof idea
One-line term composition of two existing lifts. First apply ledgerLinearResponse_from_primitiveLedgerPosting to $P$, the primitive-posting hypothesis, and the continuity assumption; that yields LedgerLinearResponse P (itself via free-ledger combiner semantics). Then feed that response into factorizationGate_of_ledgerLinearResponse, which copies symmetry, zero boundary, and unit diagonal from the response package and obtains right-affinity from the ledger-linear response lemma. No new algebra is proved here.
why it matters
This is the clean top-level statement of the ledger-to-factorization bridge: the primitive free-ledger posting surface, plus a continuity regularity hypothesis, is already enough to discharge the full factorization associativity gate. The module doc frames the goal as deriving the T4-to-T5 bridge from the recognition ledger; once the gate is in hand, the existing factorization/associativity machinery forces the RCL polynomial $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, which is the analytic content feeding T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$).
No downstream consumers are recorded yet (used_by is empty), so the declaration currently sits as the packaged export of the bridge rather than an internal lemma. It closes the primitive-posting path in this file; the discrete and rational posting surfaces are sibling routes to related response statements, but this is the direct primitive-to-gate arrow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.