Fquad_additive
plain-language theorem explainer
The lemma establishes that the quadratic cost Fquad satisfies Fquad(xy) + Fquad(x/y) = 2 Fquad(x) + 2 Fquad(y) for all positive reals x and y. Researchers proving that the quadratic-log branch fails the interaction gate cite this result. The proof is a one-line wrapper applying the consistency lemma Fquad_consistency under the additive combiner Padd.
Claim. Let $F$ denote the quadratic cost obtained by applying the log-cost constructor to the quadratic generator. Then for all $x, y > 0$, $F(xy) + F(x/y) = 2 F(x) + 2 F(y)$.
background
The module implements necessity gates to force the Recognition Composition Law by excluding degenerate cases. The interaction gate HasInteraction F asserts that there exist positive x and y such that F(xy) + F(x/y) is not equal to twice the sum of the separate costs. The counterexample cost Fquad is defined as Cost.F_ofLog applied to the quadratic generator, which yields an additive cost under the combiner Padd(u, v) = 2u + 2v. The upstream lemma Fquad_consistency proves the equality for this Fquad and Padd by working in logarithmic coordinates. This gate is required because symmetry, normalization, twice differentiability, calibration and existence of some combiner P do not suffice to force the d'Alembert structure.
proof idea
The proof applies the upstream consistency lemma Fquad_consistency directly at the parameters x, y, hx, hy and then uses simpa to rewrite with the definition of Padd.
why it matters
The result is invoked by the theorem Fquad_noInteraction to conclude that Fquad fails HasInteraction. It thereby confirms that the quadratic-log branch is ruled out by the minimal non-additivity gate in the necessity argument for the Recognition Composition Law. The gate is the weakest anti-quadratic condition and is satisfied by the J-cost of the Recognition Science framework, which obeys the full RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.