degreeTwoDiagonal
plain-language theorem explainer
The degree-two diagonal supplies the explicit algebraic form of the diagonal for any RCL-family combiner obeying the boundary Phi(a,0)=2a when rewritten in the reparameterized local coordinate a equals s plus s squared. Analysts examining the failure of the conjecture that real-analytic combiners at the origin must have polynomial degree at most two would cite this expression to test equality against the induced degree-four diagonal. The definition is obtained by direct substitution of the quadratic ansatz into the new coordinate and algebraic
Claim. For a degree-two RCL-family combiner satisfying the boundary condition $Phi(a,0)=2a$, the diagonal expressed in the local coordinate $a=s+s^2$ is $4(s+s^2)+c(s+s^2)^2$.
background
The AnalyticCounterexample module demonstrates that the corrected Phase 6 conjecture is false: a real-analytic combiner at the origin need not have polynomial degree at most two. It begins from the standard RCL variable K equals cosh(t) minus 1 and applies the analytic reparameterization f(s) equals s plus s squared to the cost coordinate. In the reparameterized variable a equals s plus s squared the induced diagonal becomes the degree-four polynomial 4s plus 18s squared plus 16s cubed plus 4s to the fourth.
proof idea
The definition is a direct algebraic expression obtained by substituting a equals s plus s squared into the quadratic form 4a plus c a squared and expanding the resulting powers of s. No external lemmas are invoked.
why it matters
This definition feeds directly into the theorems reparam_diagonal_not_degree_two and reparam_coefficients_obstruct_degree_two, which prove that no real coefficient c equates the reparameterized diagonal to any degree-two form for all s. It supplies the algebraic core of the counterexample showing that analytic reparameterization changes the polynomial degree of the combiner diagonal. In the Recognition framework it illustrates that analytic composition alone does not force the RCL degree-two structure and leaves open the question of which additional conditions would enforce it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.