Pith. sign in
module module moderate

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.AnalyticCounterexample

show as:
view Lean formalization →

Analytic counterexample module: after a local reparameterization a = s + s^2 of the cost coordinate, the diagonal of the quartic-log combiner is not a degree-two polynomial. Anyone arguing that continuous reparameterization could restore the counted-once (bilinear) form would cite it. The argument is coefficient comparison of explicit power series on the diagonal.

claimIn the local coordinate $s$ with cost $a = s + s^2$, the diagonal $D(s) := C_\mathrm{reparam}(s,s)$ of the analytically reparameterized quartic-log combiner is not equal to any degree-$\le 2$ polynomial. Explicit coefficient mismatch obstructs reduction to the counted-once form $A + B u + C v + D u v$.

background

Recognition Science forces the cost combiner through a functional equation whose continuous solutions are tightly constrained. The upstream quartic-log module supplies the algebraic heart of a counterexample: $C(x,y) = (\log(x/y))^4$ admits a continuous symmetric combiner on the nonnegative range, yet fails the structural demands placed on legitimate recognition costs.

This module works in a local analytic chart. The cost coordinate $a$ is reparameterized by $a = s + s^2$, and one studies the diagonal of the pulled-back combiner in the $s$-coordinate. The sibling objects are that reparameterized diagonal, the model degree-two diagonal, and two comparison lemmas that record the obstruction.

Downstream, the counted-once comparison module formalizes the phrase "each constituent comparison is counted once" as affinity in each argument separately: combiners of the shape $a + b u + c v + d u v$. The analytic diagonal is the natural place to test whether a smooth change of cost coordinate could restore that form.

proof idea

Definition layer first: introduce the reparameterized diagonal in the $s$-chart $a = s+s^2$, and the comparison object that would be degree two if counted-once held after reparameterization. Two lemmas then compare coefficients (or leading terms) of the explicit series for the reparameterized diagonal against any quadratic polynomial, obtaining a concrete mismatch. The module is therefore a short algebraic obstruction package sitting on top of the quartic-log counterexample import; no deep analysis beyond power-series coefficient comparison is required.

why it matters in Recognition Science

Closes a natural escape hatch in the Logic-as-Functional-Equation program: that a continuous or analytic reparameterization of the cost might turn the quartic-log combiner into a counted-once (bilinear) form. By exhibiting an explicit diagonal that is not degree two in the local chart $a = s+s^2$, the module feeds the counted-once comparison development, which needs a clean negative example before forcing the affine-in-each-variable shape $a + b u + c v + d u v$.

In the broader foundation chain this supports uniqueness pressure on the J-cost and the Recognition Composition Law: counterexamples that survive continuous reparameterization strengthen the case that only the forced $J$ (and its discrete eight-tick, $D=3$ consequences) survive the functional equation. Parent consumer is the CountOnceComparison module via import.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)