rclGate_zero_right
plain-language theorem explainer
When the second argument of the forced recognition gate vanishes, the gate collapses to twice the first cost: R(u,0)=2u. Ledger and gravity arguments cite this boundary identity whenever one pairwise cost is zero (diagonal or flat pairs). The proof is a one-line unfold of the bilinear gate followed by ring normalization.
Claim. For every real $u$, the forced recognition gate $R(u,v)=2uv+2u+2v$ satisfies $R(u,0)=2u$.
background
The recognition ledger is the bookkeeping object of recognition gravity: on a finite substrate lattice it assigns to each pair of cells a nonnegative cost, interpreted as accumulated J-cost of the comparison. Among its structural axioms is RCL subadditivity: the cost of a composite path is bounded by the forced gate R applied to intermediate costs.
That gate is the bilinear form R(u,v)=2uv+2u+2v, forced upstream by the factorization of the Recognition Composition Law (the same algebraic identity that yields J-uniqueness in the T5 step of the forcing chain). The present identity is the right-zero specialization of R.
In the ledger setting this specialization is the natural boundary case when one argument is a diagonal entry (cost zero) or a flat pair.
proof idea
One-line wrapper: unfold the definition R(u,v)=2uv+2u+2v, substitute v=0, and close by the ring tactic, which reduces 2u·0+2u+2·0 to 2u.
why it matters
This is elementary gate algebra inside the Recognition Ledger module, which the module doc positions as the central structure for three gravity applications: continuum limit of total ledger cost to the Regge action on codimension-2 hinges, Page-curve entropy from reduced states across a horizon cut, and vacuum energy as ground-state total cost on the substrate lattice.
No downstream theorem currently depends on it in the graph, but it sits with the sibling gate lemmas (symmetry, left-zero, nonnegativity) that underwrite RCL subadditivity of the ledger and the flatness criterion (total cost zero iff the ledger is identically zero). Framework landmark: the gate R is exactly the right-hand side of the Recognition Composition Law, so these identities keep ledger inequalities aligned with the forced J-cost calculus rather than an ad hoc metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.