IndisputableMonolith.Foundation.LogicAsFunctionalEquation.CountOnceComparison
This module defines the RCL family predicate specialized to one-variable derived costs. Researchers formalizing finite logical comparison or resource-sensitive syntax cite it to isolate the counted-once case. The module supplies supporting definitions that connect reality structures to analytic counterexamples but contains no theorems.
claimThe predicate stating that a one-variable cost function $K$ belongs to the RCL family under counted-once composition, where comparisons are truth-evaluable and each constituent appears at most once.
background
RealityStructure formalises truth-evaluable reality structures: 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 shows that the corrected Phase 6 conjecture (real-analytic combiner at the origin implies polynomial degree ≤ 2) is false, via reparameterisation of the standard RCL variable $K = cosh(t)-1$ by $f(s) = s + s^2$. CountOnceComparison assembles these into the one-variable RCL predicate for derived costs.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the RCL-family predicate for counted-once costs that FiniteLogicalComparison uses to package the sharpened theorem that finite logical comparison on positive ratios forces the RCL family. It also supplies the algebraic content required by LinearLogicBridge to formalise normal-form counted-once resource syntax whose only scalar monomials are 1, u, v, and u*v.
scope and limits
- Does not prove any forcing theorem from finite comparison to RCL.
- Does not treat multi-variable or higher-degree combiners.
- Does not reproduce the analytic reparameterisation counterexample.
- Does not define the full finite pairwise polynomial condition.