rclGate_zero_left
plain-language theorem explainer
Setting the first argument of the forced recognition gate R to zero collapses it to twice the second argument: R(0,v)=2v. Ledger and gravity authors use this when simplifying RCL subadditivity along a zero-cost edge. The proof is a one-line unfold of the bilinear definition followed by ring.
Claim. For every real $v$, the forced recognition gate satisfies $R(0,v)=2v$, where $R(u,v)=2uv+2u+2v$.
background
The recognition ledger is the central bookkeeping object of recognition gravity: on a finite substrate lattice it assigns to each pair of cells a nonnegative cost, intended as the accumulated J-cost of their comparison. Among its structural axioms is RCL subadditivity: the cost of a direct pair is at most the forced gate R applied to the two legs of any intermediate path, with $R(u,v)=2uv+2u+2v$.
That gate is forced by the Recognition Composition Law (and ultimately by J-uniqueness in the T5 step of the forcing chain). The module records it as a plain bilinear form on $\mathbb{R}\times\mathbb{R}$. Specializing one argument to zero is the elementary reduction needed when a ledger edge is already flat (cost zero) and one wants the residual bound on the other leg.
Upstream, the definition is exactly $R(u,v)=2uv+2u+2v$, as forced in the D'Alembert factorization development.
proof idea
One-line wrapper. Unfold the definition of the gate to $2\cdot 0\cdot v+2\cdot 0+2\cdot v$, then close by the ring tactic, which cancels the zero terms and leaves $2v$.
why it matters
Inside the recognition-ledger package this is the left-zero specialization of the forced gate that appears in RCL subadditivity. Together with the matching right-zero lemma and the nonnegativity and symmetry facts for R, it supplies the elementary algebra used when proving that total ledger cost vanishes if and only if the ledger is flat, and when reducing path inequalities along already-zero edges.
Framework-wise the gate itself is the multiplicative form forced by the Recognition Composition Law once J is fixed as $J(x)=(x+x^{-1})/2-1$ (T5). The present identity is bookkeeping rather than a new physical claim, but it is the clean left-boundary case every continuum or discrete gravity argument that routes through a flat hinge will invoke. No downstream theorems currently depend on it by name; it sits as a local algebraic utility beside its siblings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.