IndisputableMonolith.Foundation.LogicAsFunctionalEquation.CountOnceComparison
CountOnceComparison defines the RCL-family predicate specialized to one-variable derived costs under counted-once comparison. Researchers on the Logic Functional Equation paper cite it when moving from truth-evaluable reality structures to finite logical comparison. The module imports AnalyticCounterexample and RealityStructure and assembles the predicate without new theorems.
claimThe predicate that a one-variable derived cost $K$ belongs to the RCL family, i.e., satisfies $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ for the Recognition Composition Law.
background
RealityStructure formalises truth-evaluable reality structures: a comparison operator whose values are truth-evaluable, self-comparison is trivial, reordering is single-valued, every positive pair has a determinate continuous comparison, and composite comparisons have 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 reparameterising the cost coordinate by $f(s)=s+s^2$ shows that real-analytic combiners at the origin need not be quadratic. The present module specialises the RCL-family predicate to the one-variable derived-cost case that arises under counted-once resource syntax.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the RCL-family predicate required by FiniteLogicalComparison, whose sharpened theorem states that finite logical comparison on positive ratios forces the RCL family, and by LinearLogicBridge, which formalises the normal-form counted-once resource syntax in which each constituent comparison appears at most once. It therefore closes the definitional gap between the RealityStructure axioms and the finite-pairwise-polynomial content of logical comparison.
scope and limits
- Does not contain the analytic counterexamples themselves.
- Does not prove that finite comparison forces the RCL family.
- Does not define the full multi-variable RCL family.
- Does not address the eight-tick octave or spatial dimension D=3.