factorizationGate_of_primitiveLedgerPosting_monotone
plain-language theorem explainer
Primitive free-ledger posting for a two-variable combiner P, together with monotonicity in the second argument, yields the full factorization/associativity gate on P. Anyone closing the T4-to-T5 ledger bridge without a continuity hypothesis would cite this. The proof is a two-step term composition: monotone primitive posting implies ledger-linear response, which already supplies the gate.
Claim. Let $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$. Suppose $P$ is symmetric, satisfies the zero boundary $P(u,0)=2u$ and the unit diagonal $P(1,1)=6$, and is additive in free defect-ledger costs in its second argument (primitive ledger-posting semantics). If moreover $v\mapsto P(u,v)$ is monotone for every fixed $u$, then $P$ satisfies the factorization associativity gate: in particular, for each $u$ the map $v\mapsto P(u,v)$ is affine.
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. The free ledger already gives unconditional additivity of defect costs. The remaining algebraic condition is that a two-variable combiner $P$ respond linearly (affinely) to those posted costs in its second argument.
Primitive ledger-posting semantics packages the ledger-native surface: symmetry $P(u,v)=P(v,u)$, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and right-posted additivity on free defect ledgers (posting $\Gamma+\Delta$ splits the excess cost $P(u,\mathrm{cost}(\cdot))-P(u,0)$). This is closer to the Phase-2 ledger than the discrete natural-number posting surface.
The factorization associativity gate is the packaged combiner hypothesis used by the d'Alembert factorization bridge: the same symmetry, boundary, and diagonal fields, plus a right-affine field ($\forall u,\exists\alpha,\beta,\forall v,,P(u,v)=\alpha v+\beta$). Upstream, ledger-linear response already implies that gate via factorizationGate_of_ledgerLinearResponse.
proof idea
Pure term-mode composition of two in-module lemmas. First apply ledgerLinearResponse_from_primitiveLedgerPosting_monotone to the primitive posting hypothesis and the pointwise monotonicity assumption; that upgrades free-ledger additivity plus order regularity into full ledger-linear response (monotonicity replaces any continuity gate). Then feed the resulting linear-response package into factorizationGate_of_ledgerLinearResponse, which copies symmetry, zero boundary, and unit diagonal, and obtains the missing right-affine field from the linear-response theorem. No continuity or completeness is invoked.
why it matters
This is the order-regularity route from the recognition ledger to the factorization gate that forces the Recognition Composition Law polynomial (the T5 J-uniqueness step in the forcing chain). The module isolates the precise remaining algebraic condition after free-ledger additivity: with symmetry, boundary law, unit diagonal, and right-affine response, the existing d'Alembert gate theorem forces the RCL combiner $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
Relative to continuity-based routes, monotonicity is a weaker regularity demand and stays native to ordered ledger costs. No downstream consumers are wired yet (used_by is empty), so the declaration currently closes the primitive-posting branch of the ledger-to-factorization bridge rather than feeding a named parent theorem. It sits beside the discrete and rational posting surfaces as the most ledger-faithful path into the gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.