Foundation Dalembert Triangulated Proof Gates Equivalent For Jcost

The equivalence theorem

The declaration gates_equivalent_for_Jcost is a formal theorem in the machine-checked library of the Recognition Science framework. It states an equivalence between two properties of a specific cost function, denoted J. The first property is that J has interaction: there exist positive numbers x and y for which J(xy) + J(x/y) is not equal to 2J(x) + 2J(y). The second property is that there exists a two-variable function P such that J obeys the composition law J(xy) + J(x/y) = P(J(x), J(y)) for all positive x and y, and P is entangling, meaning its mixed second difference is not identically zero. The theorem proves that J has the first property if and only if it has the second.

The substance of the theorem is that two distinct recognition criteria coincide for J. One criterion looks directly at J and asks whether it deviates from a simple additive rule. The other looks at the combiner P that links J at different scales, and asks whether that combiner is genuinely nonlinear. The equivalence says these two checks are the same for J: if one holds, the other must hold, and conversely. This is a theorem in the framework's library, meaning it is a proved statement within the formal system, not an empirical observation or a definitional choice.

What the theorem does not do is force J to be the unique cost function. It takes J as given and compares two of its properties. The theorem does not assert that J is the only function with interaction, nor that J is the only function with an entangling combiner. It also does not prove that interaction alone forces the hyperbolic differential equation G'' = G + 1 for the log-lift of J; that bridge is stated in the library as an explicit hypothesis, not as a proved theorem. The equivalence is a classification result about J, not a derivation of J from first principles.

/-- The three gates are equivalent for distinguishing J from Fquad. -/
theorem gates_equivalent_for_Jcost :
    HasInteraction Cost.Jcost ↔
    (∃ P, (∀ x y, 0 < x → 0 < y →
      Cost.Jcost (x*y) + Cost.Jcost (x/y) = P (Cost.Jcost x) (Cost.Jcost y)) ∧
      IsEntangling P) := by
  constructor
  · intro _
    use Prcl
    refine ⟨?_, Prcl_entangling⟩
    intro x y hx hy
    -- This follows from the J_computes_P lemma
    have h := J_computes_P x y hx hy
    -- h : J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y)
    -- Prcl u v = 2uv + 2u + 2v
    unfold Prcl
    linarith
  · intro ⟨_, _, _⟩
    exact Jcost_hasInteraction

What this page does not claim

The theorem does not prove that J is the unique cost function with interaction. The theorem does not prove that interaction alone forces the hyperbolic differential equation. The theorem does not derive J from first principles; it compares two properties of 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/TriangulatedProof.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: