Fquad
plain-language theorem explainer
Fquad defines the quadratic log-cost F(x) = (log x)^2 / 2 on positive reals. Researchers constructing counterexamples to weak forcing of d'Alembert equations from mere existence of a combiner P cite this definition. It is a one-line composition of the log-lift operator F_ofLog with the quadratic Gquad.
Claim. Define the function $F : (0,∞) → ℝ$ by $F(x) = G(log x)$ where $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 of F. Gquad supplies the concrete quadratic G(t) = t^2 / 2. F_ofLog is the lift operator sending any G : ℝ → ℝ to the function x ↦ G(log x) on positives. The local setting is a structural obstruction: any theorem claiming to force the Recognition Composition Law from the weak hypothesis ∃P must add at least one further nondegeneracy axiom.
proof idea
One-line wrapper that applies Cost.F_ofLog to Gquad.
why it matters
This definition supplies the quadratic counterexample used by Fquad_consistency to verify the weak additive combiner property and by Fquad_on_exp to relate values back to Gquad. It supports the module claim that an additional nondegeneracy axiom is required to force the RCL. It touches the open question of minimal axioms separating the Recognition Composition Law from weaker combiner hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.