Fquad_consistency
plain-language theorem explainer
The lemma shows that the quadratic log-cost satisfies F(xy) + F(x/y) = 2F(x) + 2F(y) for all positive reals x and y. Researchers constructing necessity gates for d'Alembert structures cite it to exhibit a concrete combiner that works for the unshifted quadratic while failing after the +1 shift. The proof reduces the relation to log-space addition and subtraction identities then closes by simplification and the ring tactic.
Claim. Let $F(x) = (1/2) (log x)^2$ for $x > 0$. Then for all $x, y > 0$, $F(xy) + F(x/y) = 2 F(x) + 2 F(y)$.
background
The declaration sits inside the counterexamples module whose module doc states that 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. Here Fquad is the lift of the quadratic Gquad(t) = t²/2 via the map x ↦ G(log x). Padd is the specific additive combiner (u, v) ↦ 2u + 2v. Upstream Calibration normalizes the second derivative of the log-lift at the origin to 1, which this quadratic satisfies.
proof idea
The tactic proof first records the log-multiplication and log-division identities, then invokes simp on the definitions of Fquad, Gquad, Padd together with those identities, and finishes with the ring tactic.
why it matters
It supplies the concrete equality used by the downstream lemma Fquad_additive, which populates the HasInteraction gate inside NecessityGates. The module doc notes that any claim forcing the Recognition Composition Law or d'Alembert form from weak combiner existence must add a further nondegeneracy axiom; this lemma closes one half of the counterexample pair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.