Foundation Dalembert Factorization Forcing Rcl Combiner

The combiner

The combiner is a rule that takes two real numbers and returns a third. The canonical one in this framework is written P(u, v) = 2uv + 2u + 2v. It is the algebraic heart of a larger argument about how recognition events combine, but it can be understood on its own as a piece of constrained algebra.

The rule is not chosen freely. It is forced by four conditions. First, it is symmetric: swapping the two inputs leaves the output unchanged. Second, for any fixed first input, the output is a straight line in the second input, an affine function of the form αv + β. Third, when the second input is zero, the output is exactly twice the first input. Fourth, feeding in 1 and 1 returns 6. These four conditions pin down the polynomial completely.

The formal statement is an equivalence. A function satisfies all four conditions if and only if it equals the canonical combiner. The proof runs in two steps. The conditions first force the function to be bilinear, meaning it has the form c·uv + 2u + 2v for some constant c. Then the condition P(1,1) = 6 forces c to be 2, which yields the final polynomial. This is a machine-checked theorem in the framework's library of formal proofs, so the algebra is verified end to end.

What the declaration does not claim is just as important. It does not say that this combiner is the only possible rule in all of mathematics; the equivalence holds only under the four stated conditions. It does not say that the affine-response condition is derived from anything deeper in this file; that step is assumed as a hypothesis here. And it does not say that the combiner itself describes any physical process; that interpretation belongs to the wider Recognition Science program, not to this algebraic lemma.

The practical upshot is a clean tool. Any future argument that needs a symmetric, affine-in-its-second-slot, boundary-respecting combiner can cite this theorem and know the exact form it must take. The four conditions collapse an infinite space of possible functions to a single polynomial, and that uniqueness is what the rest of the framework builds on.

/-- Exact gate characterization: the factorization gate is equivalent to being
the canonical RCL combiner. -/
theorem factorization_gate_iff_rcl (P : ℝ → ℝ → ℝ) :
    FactorizationAssociativityGate P ↔ ∀ u v, P u v = rclCombiner u v := by
  constructor
  · intro hGate u v
    rw [gate_forces_rcl P hGate u v]
    rfl
  · intro hP
    refine {
      symmetric := ?_
      rightAffine := ?_
      zeroBoundary := ?_
      unitDiagonal := ?_
    }
    · intro u v
      rw [hP u v, hP v u]
      unfold rclCombiner
      ring
    · intro u
      refine ⟨2 * u + 2, 2 * u, ?_⟩
      intro v
      rw [hP u v]
      unfold rclCombiner
      ring
    · intro u
      rw [hP u 0]
      unfold rclCombiner
      ring
    · rw [hP 1 1]
      unfold rclCombiner
      norm_num

/-- Once the affine-response step is known, symmetry and the boundary law force
    the entire bilinear family. -/
theorem gate_forces_bilinear_family (P : ℝ → ℝ → ℝ)
    (hGate : FactorizationAssociativityGate P) :
    ∃ c : ℝ, ∀ u v, P u v = c * u * v + 2 * u + 2 * v := by
  classical
  choose α β hAffine using hGate.rightAffine
  have hβ : ∀ u, β u = 2 * u := by
    intro u
    have h0 : P u 0 = α u * 0 + β u := hAffine u 0
    rw [hGate.zeroBoundary u] at h0
    linarith
  let c : ℝ := α 1 - 2
  refine ⟨c, ?_⟩
  intro u v
  have hsym1 : P u 1 = P 1 u := hGate.symmetric u 1
  have hαu : α u = c * u + 2 := by
    dsimp [c]
    have hcalc : α u * 1 + β u = α 1 * u + β 1 := by
      calc
        α u * 1 + β u = P u 1 := by symm; exact hAffine u 1
        _ = P 1 u := hGate.symmetric u 1
        _ = α 1 * u + β 1 := hAffine 1 u
    rw [hβ u, hβ 1] at hcalc
    linarith
  calc
    P u v = α u * v + β u := hAffine u v
    _ = (c * u + 2) * v + 2 * u := by rw [hαu, hβ u]
    _ = c * u * v + 2 * u + 2 * v := by ring

/-- Canonical normalization selects the RCL member of the bilinear family. -/
theorem gate_forces_rcl (P : ℝ → ℝ → ℝ)
    (hGate : FactorizationAssociativityGate P) :
    ∀ u v, P u v = 2 * u * v + 2 * u + 2 * v := by
  obtain ⟨c, hc⟩ := gate_forces_bilinear_family P hGate
  have hc_two : c = 2 := by
    have h11 : P 1 1 = c * 1 * 1 + 2 * 1 + 2 * 1 := by
      simpa using hc 1 1
    linarith [hGate.unitDiagonal, h11]
  intro u v
  calc
    P u v = c * u * v + 2 * u + 2 * v := hc u v
    _ = 2 * u * v + 2 * u + 2 * v := by rw [hc_two]

What this page does not claim

The combiner is not claimed to be the only possible rule outside the four stated conditions. The affine-response condition is not derived in this file; it is assumed as a hypothesis. The combiner is not claimed to describe any physical process by itself.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/DAlembert/FactorizationForcing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: