Verification Exclusivity Rclderivation

The composition rule

In Recognition Science, a recognition event carries a cost, a real number measuring how expensive it is for reality to take note of something. The central question is how costs combine when two recognitions happen together. The module RCLDerivation answers that question with a precise rule, and it does so by first clearing away a wrong path.

The rule is a symmetric function f of two cost values. Symmetric means f(a, b) = f(b, a), which says the order of combining does not matter. The module proves two boundary facts about any such rule that respects the composition law J(xy) + J(x/y) = f(J(x), J(y)). First, f(0,0) = 0. Second, f(a,0) = 2a. These are not assumptions; they are theorems that follow from setting x = y = 1 and y = 1 in the composition law, given that J(1) = 0.

Those two boundary facts are enough to rule out an older idea. A previous scaffold guessed that f should be associative, meaning f(f(a,b),c) = f(a,f(b,c)). The module shows this is impossible. Symmetry plus the boundary laws force f(0,1) = 2 and f(0,2) = 4, while associativity at (0,0,1) would force them to be equal. The contradiction is proved as a theorem. The older guess was not merely unproved; it was inconsistent with the boundary laws that the composition rule itself forces.

What replaces associativity is a factorization gate. The module proves a classification theorem: if f is symmetric, satisfies f(a,0) = 2a, responds affinely in its second argument, and is normalized so f(1,1) = 6, then f is forced to be exactly f(a,b) = 2(a+1)(b+1) - 2, which expands to 2ab + 2a + 2b. This is the d'Alembert rule, named for its resemblance to a classical functional equation. The classification is a theorem in the machine-checked library of formal theorems, and it is the exact form the forcing chain uses.

What this means in plain language is that the way costs combine is not a free choice. Once you accept the composition law, the boundary conditions, and a mild regularity condition, there is exactly one possible rule. The module also shows that the earlier associativity guess was not just incomplete but actively wrong, which is why the forcing chain uses the factorization gate instead. The reader can now see that the cost-combining rule has the same forced character as the cost function itself.

/-- Boundary condition 1 (proved): f(0,0) = 0.
    Derivation: set x = y = 1 in J(xy)+J(x/y) = f(J(x),J(y)).
    J(1)+J(1) = f(J(1),J(1)) = f(0,0), so f(0,0) = 0. -/
theorem composition_rule_f00_eq_zero
    (f : CompositionRule) (J : ℝ → ℝ)
    (hJ0   : J 1 = 0)
    (hComp : ∀ x y, 0 < x → 0 < y →
               J (x * y) + J (x / y) = f.f (J x) (J y)) :
    f.f 0 0 = 0 := by
  have h := hComp 1 1 one_pos one_pos
  simp [hJ0] at h
  linarith

/-- Boundary condition 2 (proved): f(a,0) = 2a.
    Derivation: set y = 1.  J(x)+J(x) = f(J(x),0), so f(a,0) = 2a. -/
theorem composition_rule_f_at_zero
    (f : CompositionRule) (J : ℝ → ℝ)
    (hJ0   : J 1 = 0)
    (hComp : ∀ x y, 0 < x → 0 < y →
               J (x * y) + J (x / y) = f.f (J x) (J y))
    (x : ℝ) (hx : 0 < x) :
    f.f (J x) 0 = 2 * J x := by
  have h := hComp x 1 hx one_pos
  simp [hJ0, mul_one, div_one] at h
  linarith

/-- The original associativity-only scaffold is inconsistent with the proved
    boundary law `f(a,0) = 2a`.

    Indeed, symmetry gives `f(0,1) = 2` and `f(0,2) = 4`, while associativity
    at `(0,0,1)` would force `f(0,1) = f(0,2)`. So the old Open Problem B
    statement was malformed: the actual closure step cannot be associativity
    of `f` itself. -/
theorem associativity_contradicts_boundary
    (f        : CompositionRule)
    (h00      : f.f 0 0 = 0)
    (hbdry    : ∀ a, f.f a 0 = 2 * a)
    (h_assoc  : ∀ a b c, f.f (f.f a b) c = f.f a (f.f b c)) :
    False := by
  have h01 : f.f 0 1 = 2 := by
    calc
      f.f 0 1 = f.f 1 0 := f.symmetric 0 1
      _ = 2 * 1 := hbdry 1
      _ = 2 := by norm_num
  have h02 : f.f 0 2 = 4 := by
    calc
      f.f 0 2 = f.f 2 0 := f.symmetric 0 2
      _ = 2 * 2 := hbdry 2
      _ = 4 := by norm_num
  have h_assoc001 := h_assoc 0 0 1
  rw [h00, h01] at h_assoc001
  linarith

/-- Bridge B2 classification in the honest form used by the forcing chain.

    The RS algebraic closure does not use associativity of `f` itself.
    What is actually needed, and already proved elsewhere in the forcing
    chain, is the factorization gate:

    - symmetry,
    - right-affine response in the second argument,
    - the zero-boundary law `f(a,0) = 2a`,
    - and the canonical normalization `f(1,1) = 6`.

    Under those hypotheses the combiner is forced exactly to the RCL
    polynomial. -/
theorem composition_rule_classification
    (f        : CompositionRule)
    (hbdry    : ∀ a, f.f a 0 = 2 * a)
    (hAffine  : ∀ a, ∃ α β, ∀ b, f.f a b = α * b + β)
    (h11      : f.f 1 1 = 6) :
    ∀ a b, f.f a b = 2 * (a + 1) * (b + 1) - 2 := by
  let hGate : FactorizationAssociativityGate f.f :=
    { symmetric := f.symmetric
      rightAffine := hAffine
      zeroBoundary := hbdry
      unitDiagonal := h11 }
  intro a b
  calc
    f.f a b = 2 * a * b + 2 * a + 2 * b := gate_forces_rcl f.f hGate a b
    _ = 2 * (a + 1) * (b + 1) - 2 := by ring

What this page does not claim

This module does not derive the cost function J itself; it only classifies the combining rule f. The classification theorem does not prove that the d'Alembert rule is the only possible combiner without the affine response condition. This module does not establish the physical interpretation of the composition law; that bridge remains open.

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/Verification/Exclusivity/RCLDerivation.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: