IndisputableMonolith.Foundation.LogicAsFunctionalEquation.CountOnceComparison
The CountOnceComparison module defines the RCL family predicate for one-variable derived costs under the counted-once condition. Researchers tracing the LogicAsFunctionalEquation paper would cite it to connect reality structures to finite logical comparisons. The module organizes sibling definitions and lemmas that incorporate the analytic counterexample to enforce the one-variable restriction.
claimThe predicate RCLFamily(K) for a one-variable derived cost K satisfying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), where J is the standard cost function.
background
This module belongs to the LogicAsFunctionalEquation development and imports RealityStructure, which formalizes truth-evaluable comparison operators with trivial self-comparison and determinate finite pairwise combiners, and AnalyticCounterexample, which exhibits an analytic reparameterization f(s) = s + s^2 on K = cosh(t) - 1 that falsifies the polynomial-degree conjecture. The central object is the RCL family predicate specialized to one-variable derived costs, together with combiners that enforce the counted-once resource restriction.
proof idea
This is a definition module, no proofs. It declares the RCLFamily predicate along with CountedOnceCombiner, SymmetricCombiner, CountedOnceComposition and the supporting lemmas counted_once_to_finite_pairwise_polynomial, counted_once_combiner_forces_rcl, double_counting_not_allowed and analytic_reparameterization_not_counted_once.
why it matters in Recognition Science
The module supplies the counted-once predicate that FiniteLogicalComparison invokes to prove finite logical comparison on positive ratios forces the RCL family, and that LinearLogicBridge uses to restrict resource syntax to monomials 1, u, v, uv. It closes the analytic-counterexample gap in the sharpened theorem of the paper.
scope and limits
- Does not derive the full RCL from first principles.
- Does not treat multi-variable or infinite comparisons.
- Does not discharge the analytic counterexample.
- Does not address continuous logical comparison.