Foundation Dalembert Necessity Gates

Necessity gates

The d'Alembert equation, in its classical form, asks for functions that satisfy a symmetry condition relating values at products and quotients. The standard continuous solutions include the logarithm squared, F(x) = (log x)²/2, alongside the more structured solutions that Recognition Science studies. A machine-checked library of formal theorems shows that the first five conditions of the framework, symmetry, normalization, continuity, calibration, and existence of some combiner, do not by themselves single out the framework's cost function. The quadratic-log branch slips through those conditions.

To close that gap, the framework adds a necessity gate, an extra condition any candidate cost must pass. The gate is called interaction, or non-additivity. It requires that there exist at least one pair of positive comparisons whose combined cost is not purely the sum of the two individual costs. In symbols, for some x and y greater than zero, F(x·y) + F(x/y) must differ from 2F(x) + 2F(y). The quadratic-log branch fails this test: for every x and y, its combined cost is exactly additive, so it cannot satisfy the gate. The framework's own cost function, J(x) = (x + 1/x)/2 − 1, passes it, with the concrete witness x = y = 2 giving J(4) + J(1) = 9/8 + 0, which is not equal to 2·(1/4) + 2·(1/4) = 1.

This gate is the weakest possible anti-quadratic condition: it rules out the additive branch without imposing any stronger structure. Its role in the framework is to make the inevitability claim honest. Without it, the five earlier conditions permit two families of solutions; with it, the framework's cost function is the one that survives. The gate does not by itself force the full d'Alembert structure, but it removes the known counterexample and lets the later theorems in the chain proceed on firmer ground.

theorem Fquad_noInteraction : ¬ HasInteraction Fquad := by
  intro h
  rcases h with ⟨x, y, hx, hy, hneq⟩
  exact hneq (Fquad_additive x y hx hy)

lemma Fquad_additive (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
    Fquad (x * y) + Fquad (x / y) = 2 * Fquad x + 2 * Fquad y := by
  -- This is exactly `Fquad_consistency` with `Padd u v = 2u+2v`.
  simpa [Padd] using (Fquad_consistency x y hx hy)

theorem Jcost_hasInteraction : HasInteraction Jcost := by
  -- Concrete witness: x = y = 2.
  refine ⟨2, 2, by norm_num, by norm_num, ?_⟩
  -- Evaluate numerically: J(4) + J(1) ≠ 2J(2) + 2J(2).
  -- J(1)=0, J(2)=1/4, J(4)=9/8.
  norm_num [Jcost]

What this page does not claim

The interaction gate alone forces the full d'Alembert structure; it only rules out the quadratic-log branch. The quadratic-log branch satisfies all five earlier conditions; the gate is an additional requirement. The framework's cost function is the only function satisfying the interaction gate.

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