analytic_reparameterization_not_counted_once
plain-language theorem explainer
Analytic reparameterization of a combiner diagonal produces a degree-four polynomial that cannot match any degree-two RCL-family diagonal for all local coordinates s. Researchers deriving the algebraic form of counted-once comparisons cite this to exclude reparameterized candidates from the RCL family. The proof is a direct one-line application of the upstream non-equality theorem for the reparameterized diagonal.
Claim. There does not exist a real number $c$ such that for all real $s$, the reparameterized analytic combiner diagonal equals the degree-two RCL-family diagonal with parameter $c$.
background
The module formalizes counted-once comparisons: for two component costs the combiner must be affine in each variable separately, giving the form $a + b u + c v + d u v$. Identity and symmetry then force the RCL-family. Upstream definitions supply the diagonal of any degree-two RCL-family combiner with boundary condition Phi(a,0)=2a, expressed as $4(s + s^2) + c(s + s^2)^2$ in the local coordinate $a = s + s^2$, together with the diagonal of the analytically reparameterized combiner, $4s + 18s^2 + 16s^3 + 4s^4$. The prior theorem shows the reparameterized diagonal cannot equal any such degree-two form.
proof idea
This is a one-line wrapper that applies the theorem reparam_diagonal_not_degree_two, which establishes the non-equality by evaluating the assumed equality at two distinct points s=1 and s=2 and deriving a contradiction on the resulting system for c.
why it matters
The result rules out analytic reparameterization as a counted-once combiner, reinforcing that identity and symmetry force the RCL-family form in the LogicAsFunctionalEquation setting. It closes a potential loophole in the algebraic characterization of counted-once comparisons. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.