pith. machine review for the scientific record. sign in
theorem proved tactic proof high

gate_forces_rcl

show as:
view Lean formalization →

Any combiner P obeying the factorization associativity gate equals the RCL polynomial 2uv + 2u + 2v. Workers on the B2 bridge in Recognition Science cite this to select the canonical member of the bilinear family. The proof first extracts the general form c uv + 2u + 2v from the gate via an upstream lemma, then fixes c to 2 by evaluating at the unit diagonal and applying linear arithmetic.

claimLet $P : ℝ → ℝ → ℝ$ satisfy the factorization associativity gate (symmetry $P(u,v)=P(v,u)$, right-affine response, boundary $P(u,0)=2u$, and $P(1,1)=6$). Then $P(u,v)=2uv + 2u + 2v$ for all real $u,v$.

background

The FactorizationAssociativityGate packages symmetry, right-affine form in the second argument, zero boundary $P(u,0)=2u$, and unit diagonal $P(1,1)=6$. This module supplies the algebraic forcing after the analytic step that yields right-affine response. The upstream result gate_forces_bilinear_family establishes that any such P must be of the form $c uv + 2u + 2v$ for some constant $c$. From the module documentation, once affine response is available, symmetry and boundary law force the bilinear family, after which normalization selects the RCL member.

proof idea

The proof obtains the bilinear family expression from gate_forces_bilinear_family. It then evaluates the expression at u=v=1, uses the unit diagonal condition P(1,1)=6 together with the gate property to conclude c=2 by linear arithmetic. The general case follows by substitution.

why it matters in Recognition Science

This result supplies the final normalization step that selects the RCL combiner inside the factorization forcing module. It is invoked by ledger_forces_rcl to derive the RCL form from ledger substitutivity and regrouping invariance, and by polynomial_consistency_forces_rcl to close the polynomial consistency gap. In the Recognition framework it completes the algebraic core of the B2 closure program leading to the Recognition Composition Law.

scope and limits

Lean usage

gate_forces_rcl R.combiner (regrouping_forces_gate J R)

formal statement (Lean)

  63theorem gate_forces_rcl (P : ℝ → ℝ → ℝ)
  64    (hGate : FactorizationAssociativityGate P) :
  65    ∀ u v, P u v = 2 * u * v + 2 * u + 2 * v := by

proof body

Tactic-mode proof.

  66  obtain ⟨c, hc⟩ := gate_forces_bilinear_family P hGate
  67  have hc_two : c = 2 := by
  68    have h11 : P 1 1 = c * 1 * 1 + 2 * 1 + 2 * 1 := by
  69      simpa using hc 1 1
  70    linarith [hGate.unitDiagonal, h11]
  71  intro u v
  72  calc
  73    P u v = c * u * v + 2 * u + 2 * v := hc u v
  74    _ = 2 * u * v + 2 * u + 2 * v := by rw [hc_two]
  75
  76end FactorizationForcing
  77end DAlembert
  78end Foundation
  79end IndisputableMonolith

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.