IndisputableMonolith.Foundation.LogicAsFunctionalEquation.CountOnceComparison
Module isolating the count-once discipline on binary cost combiners: each leaf comparison enters a composite at most once. It defines the RCL family of one-variable derived costs and proves that a counted-once symmetric combiner forces RCL membership, while double-counting and analytic reparameterizations fall outside. Downstream finite-logical-comparison and linear-logic-bridge modules import this package. The argument reduces counted-once form to finite pairwise polynomials, then to RCL.
claimA binary combiner $C$ on positive cost coordinates is counted-once when every composite expands with each leaf factor at most once (scalar monomials among $1$, $u$, $v$, $uv$). The RCL family is the class of one-variable derived costs $J$ obeying $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Counted-once symmetric combiners force $J$ into that family; double-counting schemes and analytic reparameterizations of $K=\cosh t-1$ do not qualify as counted-once.
background
The Logic-as-Functional-Equation development treats comparison of positive ratios as a truth-evaluable reality structure: self-comparison is trivial, reordering is single-valued, every positive pair has a determinate continuous comparison, and composites admit a determinate finite pairwise combiner (RealityStructure module).
The Recognition Composition Law (RCL) is the identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, which forces the unique cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) at forcing step T5. Combiners that assemble leaf costs into composites may or may not obey a resource discipline on how often each leaf appears.
The AnalyticCounterexample module shows that real-analyticity of a combiner at the origin does not force polynomial degree $\le 2$: starting from $K=\cosh t-1$ and reparameterizing by $f(s)=s+s^2$ yields a counterexample. Count-once comparison is the stricter algebraic filter that excludes that pathology.
proof idea
Definition layer first: predicates for the RCL family of one-variable derived costs, counted-once combiners, symmetric combiners, and counted-once composition. The main positive theorems reduce counted-once form to a finite pairwise polynomial shape, then show that a counted-once symmetric combiner forces the cost into the RCL family. Two negative results close the gap with prior conjectures: double-counting is excluded by the counted-once predicate, and the analytic reparameterization counterexample is shown not to be counted-once, so it does not threaten the forcing.
why it matters in Recognition Science
This module is the algebraic core that FiniteLogicalComparison packages as the sharpened theorem "finite logical comparison on positive ratios forces the RCL family." That downstream module keeps the finite-pairwise-polynomial condition explicitly, naming it as the finite algebraic content of logical comparison; the counterexamples here explain why a purely analytic degree bound fails.
It also feeds LinearLogicBridge, which formalises resource-sensitive syntax for counted-once comparison: each constituent may appear at most once, so the only scalar monomials are $1$, $u$, $v$, and $uv$. Together these close the Reality ⇒ Logic leg toward RCL uniqueness (T5) without relying on the false Phase-6 analytic-degree conjecture.
scope and limits
- Does not drop the finite-pairwise-polynomial condition; it identifies that condition with counted-once form.
- Does not claim every real-analytic combiner is counted-once; the imported counterexample shows otherwise.
- Does not treat non-symmetric or unbounded-arity combiners beyond the stated predicates.
- Does not derive later forcing landmarks (eight-tick octave, D=3, alpha band).
- Does not itself re-prove J-uniqueness; it only forces membership in the RCL family.