Foundation Dalembert Necessity Gates Fquad No Interaction

The non-additivity gate

The Recognition Science framework starts from the idea that reality keeps a discrete record of events, a ledger, and that the cost of recognizing a combination of events is forced by simple conditions. A central theorem proves that any cost function satisfying five conditions must equal J(x) = (x + 1/x)/2 - 1. But before that theorem can hold, the framework must rule out alternative branches that satisfy most of the conditions but not all. One such branch is the quadratic-log cost, F(x) = (log x)^2 / 2, which arises when costs combine purely additively.

The declaration Fquad_noInteraction is a theorem in the framework's machine-checked library of formal theorems. It proves that the quadratic-log cost has no interaction: for any positive x and y, the combined cost of the product and quotient equals exactly twice the sum of the individual costs. In symbols, F(xy) + F(x/y) = 2F(x) + 2F(y). This means the quadratic branch is purely additive, with no cross-talk between the two comparisons. The theorem is proved by contradiction: assuming an interaction exists leads directly to a violation of the additive identity, so no such pair can exist.

The point of this theorem is to define a gate. The framework needs at least one additional condition beyond the five basic ones to rule out the quadratic branch. The interaction gate asserts that there exists at least one pair of comparisons whose combined cost is not purely additive. Fquad_noInteraction shows the quadratic branch fails this gate. The framework's preferred cost J satisfies the gate, with a concrete witness at x = 2 and y = 2, where J(4) + J(1) = 9/8 does not equal 2J(2) + 2J(2) = 1.

What this theorem does not claim is broader. It does not prove that the quadratic branch is impossible under the five basic conditions alone; in fact, the counterexample module shows the opposite, that those conditions do not force the d'Alembert structure. It also does not establish that the interaction gate is the only possible gate, nor does it prove that J is unique. The theorem only establishes a negative fact about one specific candidate, clearing one branch so the forcing chain can proceed.

theorem Fquad_noInteraction : ¬ HasInteraction Fquad := by
  intro h
  rcases h with ⟨x, y, hx, hy, hneq⟩
  exact hneq (Fquad_additive 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

This does not prove the quadratic branch is impossible under the five basic conditions alone, since the counterexample module shows those conditions do not force the d'Alembert structure. This does not establish that the interaction gate is the only possible gate, nor does it prove that J is unique.

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: