analytic_composition_not_enough
plain-language theorem explainer
Analytic reparameterization of a combiner diagonal fails to coincide with any member of the degree-two RCL family for all local coordinates. Researchers establishing the necessity of finite algebraic conditions in Recognition Science cite this boundary result. The proof is a direct one-line application of the explicit mismatch theorem between the reparameterized diagonal and quadratic RCL diagonals.
Claim. There does not exist a real number $c$ such that the diagonal of the analytically reparameterized combiner equals the diagonal of any degree-two RCL-family combiner (with boundary condition $Phi(a,0)=2a$) for every local coordinate $s$.
background
The module establishes that finite logical comparison on positive ratios forces the RCL family, while counterexamples demonstrate why the finite algebraic content of that comparison cannot be dropped. The reparameterized analytic combiner diagonal is defined in the local coordinate $a=s+s^2$ as the explicit quartic $4s+18s^2+16s^3+4s^4$. The degree-two RCL diagonal is the quadratic $4(s+s^2)+c(s+s^2)^2$ that arises from any RCL-family combiner satisfying the boundary $Phi(a,0)=2a$.
proof idea
One-line wrapper that applies the upstream theorem reparam_diagonal_not_degree_two, which itself proceeds by assuming an existential witness $c$, specializing to the concrete points $s=1$ and $s=2$, and deriving a numerical contradiction.
why it matters
This boundary theorem shows why analytic composition alone is insufficient to recover the RCL and therefore why the finite-pairwise-polynomial condition must be retained in the main result of the module. It directly supports the sharpened claim that finite logical comparison forces the RCL family. In the Recognition framework it illustrates the necessity of the finite algebraic content beyond mere analyticity or reparameterization, consistent with the derivation of the Recognition Composition Law from T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.