rclGate_nonneg

In Recognition Science gravity the recognition ledger on a finite substrate lattice Λ is a map ℒ:Λ×Λ→[0,∞) recording pairwise recognition cost. Besides symmetry and vanishing diagonal, the ledger is required to obey RCL subadditivity: ℒ(i,k)≤R(ℒ(i,j),ℒ(j,k)) for every intermediate cell j.

The gate itself is the forced bilinear form R(u,v)=2uv+2u+2v, obtained from the Recognition Composition Law factorization (cited upstream as the gate forced by D'Alembert factorization). It is the unique algebraic combination that turns the J-cost composition identity into a subadditive comparison on nonnegative costs.

The present lemma is the elementary positivity fact that keeps R inside the codomain [0,∞) whenever its arguments do, so the subadditivity inequality is well-typed for ledger values.

Term-mode proof: unfold the definition of the gate to 2uv+2u+2v, then apply nlinarith under the hypotheses u≥0 and v≥0. No external lemmas are required; nonnegativity is pure real arithmetic on the expanded bilinear form.

Module status is structural theorem (0 sorry). Nonnegativity of R is a prerequisite for the ledger axioms listed in the module doc: the codomain [0,∞), total ledger cost Σ ℒ(i,j)≥0, and the flatness characterization (total cost zero iff the ledger vanishes). Sibling results (symmetry, zero on axes, totalCost_nonneg, totalCost_eq_zero_iff_flat) sit on the same foundation.

Downstream the ledger continuum limit on codimension-2 hinges is identified with the Regge action; vacuum energy is the ground-state total cost; Page-curve entropy uses the reduced state across a horizon cut. All three uses need R to map nonnegative costs to nonnegative costs so the bookkeeping stays inside the physical cone. The gate is the RCL landmark (T5 J-uniqueness forces the composition law whose gate is exactly this R). No used_by edges are recorded yet; the lemma is infrastructure for the ledger structure itself.