Foundation Dalembert Factorization Forcing Factorization Gate Iff Rcl

The factorization gate

A combiner, a rule that takes two numbers and returns one, appears throughout mathematics whenever two inputs must be merged. The classical question is which combiners are well behaved. The framework's library, a machine-checked collection of formal theorems, answers this question for one natural set of conditions: any combiner that is symmetric, responds linearly to its second input, sends zero to twice the first input, and sends (1,1) to 6 must equal the polynomial P(u,v) = 2uv + 2u + 2v. The declaration factorization_gate_iff_rcl proves this equivalence: a combiner satisfies the gate exactly when it is this polynomial.

The conditions are not arbitrary. Symmetry says the order of inputs does not matter. Right-affineness says that for each fixed first input, the combiner is a straight line in the second. The boundary law P(u,0) = 2u and the normalization P(1,1) = 6 pin down the remaining freedom. The theorem first shows the gate forces a bilinear family, P(u,v) = cuv + 2u + 2v, then uses the normalization to force c = 2. The result is a uniqueness statement: no other polynomial satisfies all four conditions.

In Recognition Science, this combiner is the RCL polynomial, the algebraic core of the framework's cost function. The framework models recognition as a ledger, a discrete record of events, and derives its cost function from five plain conditions. The factorization gate supplies the algebraic step: once the analytic work shows the combiner is affine in its second argument, symmetry, the boundary law, and normalization force the exact RCL form. The theorem is the clean algebraic finish to that argument.

The declaration does not claim that the analytic step itself is proved. The passage from factorization plus three-way compatibility to right-affineness is the hard analytic part, and it is not part of this theorem. The gate also does not prove the cost function's uniqueness; it proves a conditional statement about combiners satisfying the gate. The framework's full cost theorem rests on additional analytic input.

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

/-- The canonical RCL polynomial satisfies the full factorization gate. -/
theorem rclCombiner_satisfies_gate :
    FactorizationAssociativityGate rclCombiner where
  symmetric := by
    intro u v
    unfold rclCombiner
    ring
  rightAffine := by
    intro u
    refine ⟨2 * u + 2, 2 * u, ?_⟩
    intro v
    unfold rclCombiner
    ring
  zeroBoundary := by
    intro u
    unfold rclCombiner
    ring
  unitDiagonal := by
    unfold rclCombiner
    norm_num

What this page does not claim

The theorem does not prove the analytic step that factorization plus three-way compatibility forces right-affineness. The theorem does not establish the uniqueness of the framework's cost function; it only characterizes combiners satisfying the gate. The theorem does not say that every symmetric combiner with the boundary law is the RCL polynomial; right-affineness is essential.

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: