Foundation Dalembert Right Affine From Factorization Rcl Without Gate

What the gate-free theorem proves

The declaration rcl_without_gate is a theorem in the framework's machine-checked library of formal theorems. It concerns a two-variable function P that describes how a recognition cost, a discrete record of events, combines when two costs are added. The theorem states: if the cost function J satisfies a specific consistency relation, then P must equal the polynomial 2uv + 2u + 2v on the nonnegative quadrant.

In plainer terms, the theorem pins down the exact algebraic form of the combination rule. The consistency relation is F(xy) + F(x/y) = P(F(x), F(y)), where F is the cost function J. The theorem's conclusion is that P(u,v) = 2uv + 2u + 2v. This is a strong result because it holds for any function P whatsoever that satisfies the relation; no assumption about P being polynomial, smooth, or right-affine is needed.

The theorem is proved in Lean 4, a proof assistant, and is axiom-clean. It is a re-exposition of an earlier result, rcl_unconditional, which established the same conclusion using only the surjectivity of J onto the nonnegative reals and J's intrinsic identity. The declaration closes a gap in the framework's development by showing that a previously assumed hypothesis, right-affineness, is not actually required for the main forcing result.

What the theorem does not claim is equally important. It does not claim that the cost function J itself is derived here; that is established elsewhere. It does not claim that P must be a polynomial in general; that remains an open problem. It only claims that if P satisfies the consistency relation with J, then P takes the RCL form. The theorem is a precise, conditional statement, not a claim about the origin of the cost function or the polynomial form.

/-- **Gate-free RCL theorem (from Unconditional.lean, re-exposed here).**

If F = J and F has any consistency relation F(xy) + F(x/y) = P(F(x), F(y))
with some function P, then P equals the RCL polynomial on [0, ∞)². This holds
without any assumption on P's form (polynomial, right-affine, smooth, etc.).
-/
theorem rcl_without_gate
    (P : ℝ → ℝ → ℝ)
    (hCons : ∀ x y : ℝ, 0 < x → 0 < y →
      Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y)) :
    ∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2*u*v + 2*u + 2*v :=
  Unconditional.rcl_unconditional P hCons

/-- **Gate-free RCL theorem (from Unconditional.lean, re-exposed here).**

If F = J and F has any consistency relation F(xy) + F(x/y) = P(F(x), F(y))
with some function P, then P equals the RCL polynomial on [0, ∞)². This holds
without any assumption on P's form (polynomial, right-affine, smooth, etc.).
-/
theorem rcl_without_gate
    (P : ℝ → ℝ → ℝ)
    (hCons : ∀ x y : ℝ, 0 < x → 0 < y →
      Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y)) :
    ∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2*u*v + 2*u + 2*v :=
  Unconditional.rcl_unconditional P hCons

What this page does not claim

The theorem does not derive the cost function J itself. The theorem does not prove that P must be a polynomial in general. The theorem does not claim the consistency relation holds for all functions F, only for the specific cost function J.

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/RightAffineFromFactorization.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: