Foundation Dalembert Factorization Forcing Gate Forces Bilinear Family

The forced bilinear family

The theorem gate_forces_bilinear_family concerns a two-argument function P(u, v) that combines two real numbers into one. The framework's ledger, a discrete record of recognition events, needs such a combiner to merge two costs into a single cost. The theorem states a precise rigidity result: if P satisfies four plain conditions, then it must have the form P(u, v) = c·u·v + 2u + 2v for some constant c. The conditions are symmetry (P(u, v) = P(v, u)), affine response in the second argument (for each fixed u, P(u, v) is a straight line in v), a boundary law (P(u, 0) = 2u), and a normalization (P(1, 1) = 6).

The proof is short and entirely algebraic. From the affine response, P(u, v) = α(u)·v + β(u). Symmetry forces the coefficient of v to be linear in u, so α(u) = c·u + d. The boundary law then pins d = 2, and the normalization fixes nothing about c, leaving the one-parameter family. The theorem does not determine c; that requires the additional condition called the canonical normalization, which selects c = 2 and yields the RCL combiner P(u, v) = 2uv + 2u + 2v. The gate is therefore a stepping stone: it narrows all possible combiners to a single line of candidates, and a later theorem in the same module forces the unique member of that line.

The result belongs to a chain that the framework uses to derive physical constants. The same module proves that the gate is exactly equivalent to being the RCL combiner, and that the combiner satisfies the gate. The theorem is machine-checked in the framework's library of formal theorems, with no unverified axioms beyond the standard logical postulates. What the theorem does not claim is just as important: it does not assert that any actual process satisfies the gate, nor that the constant c must be 2, nor that the combiner is unique without the normalization. Those are separate statements, proved elsewhere in the module or left as further steps in the forcing chain.

The practical consequence is a sharp reduction in search space. If a recognition process can be shown to satisfy the four gate conditions, its cost-combining rule is known up to one number, and that number is fixed by a single evaluation at (1, 1). This turns a seemingly open functional problem into a finite check, which is what makes the later derivation of the RCL polynomial and the constants that follow from it tractable.

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

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

/-- 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 assert that any actual recognition process satisfies the four gate conditions. The theorem does not by itself force the constant c to equal 2. The theorem does not claim uniqueness of the combiner without the canonical normalization.

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: