IndisputableMonolith.Foundation.LogicAsFunctionalEquation.QuarticLogCounterexample
Exhibits an explicit quartic-in-log comparison that is symmetric and nonnegative on the positive quadrant yet fails the Recognition Composition Law family. Supplies the algebraic seed for the analytic reparameterisation counterexample one module up. The argument is direct: build the combiner, check the elementary symmetries and sign, then show a square-root term is not bilinear so the RCL identity fails.
claimThere is a comparison $C$ built from a quartic polynomial in $\log$ (equivalently a degree-4 expression in the hyperbolic cost coordinate $K=\cosh t-1$) that is symmetric, nonnegative for nonnegative arguments, yet is not a member of the Recognition Composition Law family: it fails bilinearity of the associated square-root term and therefore does not satisfy $C(xy)+C(x/y)=2C(x)C(y)+2C(x)+2C(y)$.
background
Recognition Science forces the cost functional $J$ from the Recognition Composition Law (RCL) $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, with unique continuous solution $J(x)=(x+x^{-1})/2-1=\cosh(\log x)-1$ (forcing step T5). The DirectProof module isolates the finite pairwise polynomial-closure regularity that forces the RCL family for operative positive-ratio comparisons, and treats the strict bi-affine counted-once subcase.
This module sits one layer below the analytic counterexample work. It manufactures a concrete quartic-log comparison (a combiner built from degree-4 polynomials in the log/hyperbolic coordinate) that looks like a legitimate cost comparison on the surface: it is symmetric and stays nonnegative on the nonnegative orthant. The point is to have an algebraic object that already escapes the RCL family before any analytic reparameterisation is applied.
proof idea
Definition-first module with short algebraic lemmas. Introduce the quartic-log comparison and the associated combiner. Verify symmetry of the combiner by direct expansion, and nonnegativity on the nonnegative orthant by elementary sign checks. Isolate a square-root term that would have to be bilinear for membership in the RCL family, then exhibit an explicit pair of arguments where bilinearity fails. Conclude that the combiner is not an RCL-family comparison. No heavy analysis; pure polynomial/identity algebra over the positive reals.
why it matters in Recognition Science
Feeds the AnalyticCounterexample module, whose doc-comment states that the corrected Phase 6 conjecture ("real-analytic combiner at the origin implies polynomial degree $\le 2$") is false. That parent starts from the standard RCL variable $K=\cosh t-1$ and reparameterizes the cost coordinate by $f(s)=s+s^2$; the quartic-log comparison constructed here is the algebraic core that survives the reparameterisation and supplies the concrete counterexample.
In the broader forcing chain the uniqueness of $J$ (T5) and the RCL itself are only as strong as the regularity hypotheses placed on admissible combiners. This module shows that mere symmetry-plus-nonnegativity is too weak: a quartic-log object already escapes the RCL family, so any theorem claiming "all reasonable comparisons are RCL" must impose a genuine degree or analyticity bound (and even then the parent module shows pure real-analyticity at the origin is insufficient).
scope and limits
- Does not claim the quartic-log comparison is real-analytic at the origin; that is handled upstream in AnalyticCounterexample.
- Does not refute RCL uniqueness under polynomial-closure or bi-affine hypotheses from DirectProof.
- Does not produce a physical cost functional; the object is a pure counterexample to over-broad regularity claims.
- Does not address discrete eight-tick or D=3 forcing steps; scope is the continuous comparison law only.