pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.DAlembert.NecessityGates

show as:
view Lean formalization →

This module introduces the interaction gate for cost functions in the d'Alembert framework of Recognition Science. It defines HasInteraction F to mean that F(xy) + F(x/y) deviates from pure additivity 2F(x) + 2F(y) for some x, y > 0. Researchers proving inevitability of the d'Alembert equation from structural axioms cite this gate as the first of four necessary conditions. The module pairs the definition with counterexamples showing that existence of any combiner P alone fails to force the log-lift structure.

claimA cost function $F$ satisfies the interaction gate when there exist $x, y > 0$ such that $F(xy) + F(x/y) ≠ 2F(x) + 2F(y)$.

background

The module resides in the Foundation.DAlembert namespace and imports the Cost module together with Counterexamples. The upstream Counterexamples module records that the mere existence of a combiner P satisfying F(xy) + F(x/y) = P(F(x), F(y)) does not force the d'Alembert structure on the log-lift of F. In the Recognition framework, cost functions F are constrained by the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), and the interaction gate distinguishes additive from non-additive behavior under product-quotient combination.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the Interaction Gate that feeds the Bridge Theorem in AnalyticBridge: if F satisfies structural axioms and has interaction, then the log-lift H(t) = F(e^t) + 1 obeys the d'Alembert equation. It is also used by EntanglementGate and by the TriangulatedProof that unifies the four gates into a single inevitability result.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (4)