IndisputableMonolith.Foundation.LogicAsFunctionalEquation.CountOnceComparison
CountOnceComparison defines the RCL family predicate specialized to one-variable derived costs. Researchers working on the sharpened finite logical comparison theorem or the counted-once resource syntax would cite it. The module assembles supporting definitions from analytic counterexamples and reality structures.
claimLet $K$ be a one-variable derived cost. The predicate RCLFamily$(K)$ asserts that $K$ belongs to the Recognition Composition Law family.
background
RealityStructure formalizes the Reality to Logic leg: a comparison operator whose values are truth-evaluable, with self-comparison trivial, reordering single-valued, and every positive pair admitting a determinate continuous comparison whose composites admit a determinate finite pairwise combiner. AnalyticCounterexample supplies the algebraic core of the corrected Phase 6 counterexample: starting from the standard RCL variable $K=\cosh(t)-1$ and reparameterizing the cost coordinate by $f(s)=s+s^2$ shows that real-analytic combiners at the origin need not be polynomials of degree at most 2.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the counted-once RCL predicate required by FiniteLogicalComparison, which packages the sharpened theorem that finite logical comparison on positive ratios forces the RCL family, and by LinearLogicBridge, which formalizes the normal-form counted-once resource syntax in which each constituent comparison appears at most once.
scope and limits
- Does not prove the RCL family from finite comparisons.
- Does not treat multi-variable derived costs.
- Does not reproduce the full analytic counterexample construction.
- Does not address the eight-tick octave or spatial dimension forcing.