Foundation Dalembert Factorization Forcing

The combiner gate

A combiner is a function that takes two numbers and returns a third. In Recognition Science, the numbers are costs of recognition events, and the combiner says how two such costs join into one. The framework called foundation dalembert factorization forcing studies combiners that satisfy four plain rules: swapping the inputs changes nothing, fixing the first input makes the function a straight line in the second, combining any cost with zero doubles it, and combining one with one gives six. These are not arbitrary choices; each one states a symmetry or a boundary condition that a cost ledger should respect.

The classical ancestor of this setup is Jean le Rond d'Alembert's 1747 solution to the vibrating string equation, where a function of two variables that splits into parts forces a specific functional form. The same move appears here. The framework proves that any combiner meeting the four rules must equal 2uv + 2u + 2v. The proof runs in two steps. First, symmetry plus the straight-line property forces the combiner to be bilinear, meaning it has the shape c times u times v plus 2u plus 2v for some constant c. Second, the boundary condition at one and one pins c to 2, leaving exactly the formula above. The result is an exact characterization: a combiner satisfies the gate if and only if it is that formula.

This matters because the formula is not a guess. It is the unique object that survives the four constraints, and it is the same polynomial that appears elsewhere in the framework as the cost function's composition law. The final theorem states the equivalence directly: the gate holds precisely when the combiner is the canonical one. In plain terms, if reality keeps a ledger where recognition costs combine by these rules, there is no freedom left in how they combine. The algebra closes, and the framework can move on to the next forcing step.

In Recognition Science, this gate is the algebraic core of a larger closure program. The hard analytic step, showing that factorization plus three-way compatibility makes the combiner affine in its second argument, is assumed here as a premise. Once that step is granted, the remaining forcing is pure algebra: symmetry, the zero boundary, and the normalization at one and one force the polynomial exactly. The framework does not prove the affine step itself; it proves what follows after that step is available.

/-- 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]

/-- 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

What this page does not claim

This framework does not prove the affine-response step; it assumes that step as a premise. The gate does not by itself force the cost function J; it forces the combiner polynomial only.

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: