Pith. sign in
module module moderate

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.AnalyticCounterexample

show as:
view Lean formalization →

Analytic counterexample module for the logic functional equation: after reparameterizing the combiner into a local coordinate s with a = s + s^2, the diagonal fails to be quadratic. It supplies the diagonal objects and the coefficient obstruction that the quartic-log combiner is not degree two. Downstream counted-once comparison cites it to separate genuine affine combiners from analytic impostors. The argument is algebraic comparison of power-series coefficients on the diagonal.

claimIn the local coordinate $s$ with $a = s + s^2$, the diagonal of the analytically reparameterized combiner is not a degree-two polynomial: its power-series coefficients obstruct any identification with a quadratic $A + B a + C a^2$.

background

The parent thread is the Logic Functional Equation program: which continuous symmetric combiners $C(u,v)$ can arise as cost aggregators. The upstream quartic-log module isolates the algebraic heart of one counterexample, $C(x,y) = (\log(x/y))^4$, which still admits a continuous symmetric combiner on the nonnegative range.

This module moves to an analytic chart. The local coordinate $s$ is tied to the cost variable by $a = s + s^2$. Inside that chart one forms the diagonal of the reparameterized combiner (the restriction $u = v$) and compares it to the genuine degree-two diagonal that would arise from an affine-in-each-slot combiner $a + b u + c v + d u v$.

The sibling objects are exactly those two diagonals and the two obstruction lemmas: the reparameterized diagonal is not degree two, and its coefficients forbid any degree-two match.

proof idea

Definition layer first: introduce the reparameterized diagonal and the model degree-two diagonal in the $s$-chart. Then two comparison lemmas. The first shows the reparameterized diagonal is not identical to any quadratic in $a$. The second extracts explicit coefficient mismatches (power-series or polynomial expansion in $s$) that rule out degree two. No external analytic machinery beyond the algebraic identities already in the quartic-log import; the work is coefficient chasing on the diagonal.

why it matters in Recognition Science

Counted-once comparison (the sole direct downstream import) needs a sharp negative example: a continuous symmetric combiner that is not affine in each argument separately. The phrase formalized there is that each constituent comparison is counted once, algebraically $a + b u + c v + d u v$. This module supplies the analytic obstruction that the quartic-log family, after reparameterization, fails that degree-two test on the diagonal.

In the broader Recognition forcing chain the point is defensive: the J-cost uniqueness (T5) and the Recognition Composition Law are not accidental among continuous combiners; analytic look-alikes such as $(\log(x/y))^4$ are excluded by precisely this coefficient obstruction. Without the module, CountOnceComparison would lack a concrete separator between affine combiners and higher-order analytic impostors.

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)