Fquad_symm
plain-language theorem explainer
The quadratic log-cost is invariant under inversion for positive reals. Researchers constructing counterexamples to weak forcing of d'Alembert equations cite this symmetry to separate additive combiners from the full Recognition Composition Law. The proof is a direct simplification that unfolds Fquad as the quadratic applied to the logarithm and invokes the reciprocal logarithm identity.
Claim. For every positive real number $x$, $F(x) = F(x^{-1})$, where $F(x) = G(log x)$ and $G(t) = t^2/2$.
background
The module documents that existence of some combiner P satisfying F(xy) + F(x/y) = P(F(x), F(y)) does not force d'Alembert structure on the log-lift. It defines Gquad(t) := t²/2 and sets Fquad(x) := Gquad(log x) = (log x)²/2, which admits the additive combiner P(u,v) := 2u + 2v yet whose shifted lift H(t) := t²/2 + 1 fails d'Alembert. Upstream, F_ofLog is the composition G ∘ log, and the same quadratic appears in the CurvatureGate counterexample.
proof idea
One-line wrapper that applies simp to unfold Fquad as Cost.F_ofLog Gquad, substitutes the quadratic definition, and reduces via Real.log_inv together with the positivity hypothesis to equate the squared terms.
why it matters
The lemma supplies an explicit symmetry used in the module's obstruction argument: weak consistency with an additive combiner is insufficient to recover the Recognition Composition Law or d'Alembert form, so any forcing theorem from ∃P must add nondegeneracy axioms. It sits inside the counterexample construction that separates the quadratic case from the hyperbolic G required by T5 J-uniqueness and the RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.