reparamDiagonal
plain-language theorem explainer
reparamDiagonal defines the explicit quartic that gives the diagonal of an RCL combiner after the analytic change of coordinate a = s + s². Researchers examining whether real-analytic solutions to the Recognition Composition Law must remain quadratic would cite this expression when constructing counterexamples. The definition is supplied directly by substituting the reparameterization into the combiner diagonal and expanding the resulting polynomial.
Claim. $d(s) = 4s + 18s^{2} + 16s^{3} + 4s^{4}$, the diagonal of the analytically reparameterized combiner expressed in the local coordinate $s$ satisfying $a = s + s^{2}$.
background
The AnalyticCounterexample module constructs an algebraic counterexample to the claim that a real-analytic combiner at the origin must have polynomial degree at most two. It starts from the standard RCL variable K = cosh(t) - 1 and reparameterizes the cost coordinate by the map f(s) = s + s², so that the new variable satisfies a = s + s². The induced combiner then possesses the diagonal given by this definition.
proof idea
The definition is a direct algebraic expansion obtained by substituting a = s + s² into the diagonal of the degree-two RCL-family combiner and collecting powers of s. No external lemmas are invoked; the quartic coefficients arise immediately from the substitution.
why it matters
This definition supplies the concrete diagonal required by the theorems reparam_diagonal_not_degree_two and reparam_coefficients_obstruct_degree_two, which together prove that no real number c satisfies the identity for all s. It thereby falsifies the corrected Phase 6 conjecture that analyticity at the origin forces quadratic RCL form. The construction sits inside the Recognition Composition Law and the forcing chain T0–T8, showing that analytic reparameterization alone does not recover the quadratic boundary condition Phi(a,0) = 2a.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.