factorizationGate_of_primitiveLedgerPosting_directional
plain-language theorem explainer
Primitive ledger posting plus per-slice directional regularity (each fixed-u slice monotone or antitone) forces the full factorization associativity gate on the combiner. Cite this when deriving the T4-to-T5 bridge from the recognition ledger rather than as analytic input. Proof is a one-line composition: directional primitive posting yields ledger-linear response, which already packages the gate.
Claim. Let $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ obey primitive ledger-posting semantics: symmetry $P(u,v)=P(v,u)$, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and additive response of $v\mapsto P(u,v)$ under free defect-ledger posting in the second argument. If for every $u$ the slice $v\mapsto P(u,v)$ is monotone or antitone, then $P$ satisfies the factorization associativity gate (symmetry, right-affinity in the second argument, zero boundary, unit diagonal).
background
This module is the Ledger-to-Factorization bridge. Phase 3 asks that the T4-to-T5 step be derived from the recognition ledger rather than assumed analytically. The free ledger already supplies unconditional additivity of ledger cost. The remaining algebraic condition is that a two-variable combiner respond linearly (affine) in its second argument when that argument is a posted ledger cost; together with symmetry, the zero boundary, and the unit diagonal, the existing d'Alembert gate then forces the RCL polynomial.
Primitive ledger-posting semantics is the structure closest to the Phase-2 ledger: the second coordinate is fed by the cost of actual free defect ledgers, and additive posting of ledgers is exactly the operation the combiner sees. It is stricter than the discrete surface, which only talks about natural-number costs after choosing a rank-one unit ledger.
The factorization associativity gate packages four fields: symmetry, right-affinity ($\exists\alpha,\beta$ with $P(u,v)=\alpha v+\beta$), zero boundary $P(u,0)=2u$, and unit diagonal $P(1,1)=6$. Ledger-linear response is the intermediate that already carries symmetry, boundary, diagonal, and the linear-response law needed to build right-affinity.
proof idea
One-line term wrapper. First apply the sibling lemma that turns primitive ledger-posting semantics plus the per-slice monotone-or-antitone hypothesis into ledger-linear response. Then feed that response into the already-proved gate constructor, which copies symmetry, zero boundary, and unit diagonal, and obtains right-affinity from the linear-response field. No new algebra is done at this layer.
why it matters
This is the non-vacuous order route from the recognition ledger to the factorization gate: the only regularity asked beyond primitive posting is directional monotonicity of each fixed-cost slice, and the canonical RCL combiner is known to satisfy that hypothesis, so the forcing is not empty. In the framework it sits on the T4-to-T5 bridge that ultimately feeds T5 J-uniqueness and the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. The module goal is exactly to isolate this algebraic condition so the d'Alembert factorization gate can force the RCL polynomial from ledger data rather than analytic assumption. No downstream consumers are wired yet; the declaration is a proved leaf ready for the gate-to-RCL step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.