HasInteraction
plain-language theorem explainer
HasInteraction defines the non-additivity gate on a cost function F from positive reals to reals. Analysts deriving full inevitability of the Recognition Composition Law cite it to exclude the quadratic-log branch. The definition is a direct existential predicate asserting that some product-quotient pair violates pure additivity in the separate costs.
Claim. A cost function $F: (0,∞) → ℝ$ satisfies the interaction gate when there exist $x,y > 0$ such that $F(xy) + F(x/y) ≠ 2F(x) + 2F(y)$.
background
The module implements minimal nondegeneracy conditions that force the d'Alembert/RCL structure once symmetry, normalization, C² smoothness, and calibration are assumed. The interaction gate specifically rules out the additive branch, which in log coordinates yields the quadratic cost $F(x) = (log x)^2 / 2$ with combiner $P(u,v) = 2u + 2v$. Upstream results supply concrete instances of F, including the gap function $F(Z) = log(1 + Z/φ)/log(φ)$ from AnchorPolicy and the generating functional $F(z) = log(1 + z/φ)$ from Pipelines.
proof idea
Direct definition. The predicate is introduced by an existential quantifier over positive reals x and y that violate the additivity equation; no lemmas or tactics are applied.
why it matters
The definition supplies the fundamental nondegeneracy condition invoked by analytic_bridge_full, F_forced_to_Jcost, P_forced_to_RCL, full_inevitability, and gates_connected. Those theorems chain interaction to an entangling combiner, then to the hyperbolic ODE whose unique solution is G = cosh(log x) - 1, hence F = Jcost. In the Recognition framework it closes the gap left by the counterexamples module and aligns with T5 J-uniqueness by excluding the additive branch that would otherwise block the self-similar fixed point and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.