pith. sign in
module module high

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.AnalyticCounterexample

show as:
view Lean formalization →

The AnalyticCounterexample module supplies the diagonal of an analytically reparameterized combiner in the local coordinate s where a equals s plus s squared. It builds on the quartic-log counterexample to produce a continuous symmetric combiner on the nonnegative reals. Researchers examining obstructions to the logic functional equation cite this construction when testing analytic reparameterizations. The module organizes its content through direct import of the quartic case and sibling definitions of reparametrized diagonals.

claimLet $C(x,y)= (log(x/y))^4$. The reparameterized diagonal is the function obtained by substituting the analytic change of variables with local coordinate $s$ satisfying $a=s+s^2$.

background

The module belongs to the LogicAsFunctionalEquation development and imports the quartic-log counterexample. That upstream result states that $C(x,y)=(log(x/y))^4$ defines a continuous symmetric combiner on the nonnegative range. The present module isolates the diagonal of the analytically reparameterized version of this combiner. The reparameterization uses the local coordinate $s$ defined by the quadratic relation $a=s+s^2$, which converts the original combiner into a form convenient for degree analysis.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the CountOnceComparison module, which requires that each constituent comparison is counted once and therefore demands a combiner affine in each variable separately (of the form $a + b u + c v + d u v$). It supplies the analytic reparameterized diagonal needed to test whether the quartic-log counterexample satisfies or obstructs that affine condition.

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)