factorizationGate_of_rationalLedgerPosting
plain-language theorem explainer
Rational completed ledger posting on a real combiner forces the full factorization associativity gate. Cite this when closing the T4-to-T5 bridge from ledger semantics rather than from analytic axioms. The proof is a one-line composition: convert rational posting to ledger-linear response, then apply the existing linear-response gate theorem.
Claim. Let $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$. If $P$ obeys rational ledger posting semantics (symmetry $P(u,v)=P(v,u)$, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, right-continuity in the second argument, and affine response on rational second arguments), then $P$ satisfies the factorization associativity gate: symmetry, existence of right-affine coefficients $\alpha,\beta$ with $P(u,v)=\alpha v+\beta$, the same zero boundary, and the same 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 analytically. This module isolates the remaining algebraic condition: free-ledger additivity is already unconditional; what remains is a two-variable combiner with ledger-linear response in its second argument, plus symmetry, boundary law, and unit diagonal.
Rational ledger posting semantics is the analytic-completion input. On the countable positive-ratio completion of the free ledger, costs already obey an affine response law at rational second arguments, and the response extends continuously in the completed real coordinate. The structure packages symmetry, $P(u,0)=2u$, $P(1,1)=6$, right-continuity, rational right-affinity, and free-ledger additivity.
The factorization associativity gate is the packaged combiner hypothesis used by the d'Alembert factorization bridge: symmetry, right-affinity (existence of $\alpha,\beta$ with $P(u,v)=\alpha v+\beta$), zero boundary, and unit diagonal. Upstream, ledger-linear response is equivalent to rational posting plus continuity, and that response already yields the full gate.
proof idea
One-line term wrapper. Apply the forward direction of rationalLedgerPosting_iff_ledgerLinearResponse to turn the rational-posting hypothesis into ledger-linear response, then feed that into factorizationGate_of_ledgerLinearResponse, which already constructs the gate fields (symmetry and boundaries by projection; right-affinity by the linear-response lemma).
why it matters
This is the clean entry point from completed ledger semantics to the factorization gate that forces the Recognition Composition Law polynomial. The module doc states the goal explicitly: with right-affinity in hand, symmetry, boundary law, and unit diagonal, the existing gate theorem forces the RCL polynomial $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, which is the T5 landmark (J-uniqueness) in the forcing chain.
No downstream consumers are wired yet in the graph, so the declaration presently closes the ledger-to-gate arrow rather than feeding a named parent theorem. It sits at the end of the rational-completion ladder (primitive posting to discrete to rational to linear response to gate) and is the statement a paper-level T4-to-T5 derivation would cite when the input is rational ledger posting rather than an abstract linear-response package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.