rclGate
plain-language theorem explainer
Defines the forced bilinear gate R(u,v)=2uv+2u+2v that appears on the right-hand side of the Recognition Composition Law. Gravity and ledger authors cite it as the comparison bound in RCL subadditivity on substrate pairs. The body is a direct algebraic abbreviation of that forced form.
Claim. Define the real-valued gate $R(u,v) := 2uv + 2u + 2v$ for $u,v \in \mathbb{R}$. This is the forced composition gate of recognition cost, used as the upper bound in ledger subadditivity: $\mathcal{L}(i,k) \le R(\mathcal{L}(i,j),\mathcal{L}(j,k))$.
background
The Recognition Ledger module treats gravity bookkeeping on a finite substrate lattice $\Lambda$. A ledger $\mathcal{L}:\Lambda\times\Lambda\to[0,\infty)$ records the accumulated recognition cost of comparing cells. Besides symmetry, diagonal zero, and non-negativity, every ledger must obey RCL subadditivity: for every intermediate cell $j$,
$$\mathcal{L}(i,k)\le R(\mathcal{L}(i,j),\mathcal{L}(j,k)),$$
with $R$ the gate defined here.
That gate is not free. The Recognition Composition Law on the J-cost reads $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. The right-hand side, rewritten in cost variables $u=J(x)$, $v=J(y)$, is exactly $R(u,v)=2uv+2u+2v$. The doc-comment points to the forcing theorem gate_forces_rcl in the D'Alembert factorization chain, which isolates this bilinear form as the unique gate compatible with the composition law (and with T5 J-uniqueness $J(x)=(x+x^{-1})/2-1$).
proof idea
Pure definition: the body is the closed-form expression $2uv+2u+2v$ on $\mathbb{R}\times\mathbb{R}$. No tactics or lemmas. Downstream lemmas (rclGate_symmetric, rclGate_zero_left/right, rclGate_nonneg) unfold this abbreviation and finish by ring or nlinarith.
why it matters
This gate is the algebraic hinge of recognition gravity. The structure RecognitionLedger packages RCL subadditivity with rclGate as the comparison bound; flatLedger discharges that field by unfolding the gate and norm_num. Sibling facts (symmetry, one-sided zeros, non-negativity on the positive orthant) make the gate safe to use in total-cost and flatness theorems (totalCost_eq_zero_iff_flat, isFlat).
Downstream SevenGaps constructions (distinctLedger, uniformLedger) reuse the same gate when building non-flat or site-blind ledgers. In the broader framework it is the concrete avatar of the RCL right-hand side forced after T5 J-uniqueness, and it underwrites the three ledger uses named in the module doc: continuum Regge action on codimension-2 hinges, Page-curve entropy across a horizon cut, and vacuum energy as ground-state total cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.