no_hidden_state_logic_forces_rcl
plain-language theorem explainer
A no-hidden-state operative comparison operator on positive reals forces the RCL family on its derived cost function. Researchers deriving physics from logic in the Recognition Science program would cite this as the terminal step linking finite comparison to the composition algebra. The proof is a one-line wrapper that invokes the upstream no-hidden-state comparison theorem.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. Assume $C$ satisfies the operative positive-ratio conditions (identity, non-contradiction, continuity, scale invariance, non-triviality) together with the no-hidden-state composition law. Then the derived cost $F(r) := C(r,1)$ lies in the RCL family: there exist $P : ℝ → ℝ → ℝ$ and $c ∈ ℝ$ such that $P(u,v) = 2u + 2v + c·u·v$ for all $u,v$ and $F$ satisfies multiplicative consistency with $P$.
background
ComparisonOperator is the type of maps ℝ → ℝ → ℝ that assign a real cost to any pair of positive quantities. derivedCost extracts the one-argument cost on positive ratios by fixing the second argument at the multiplicative identity 1. OperativePositiveRatioComparison packages the four Aristotelian constraints plus continuity and non-triviality into a single structure on such operators.
proof idea
The proof is a one-line wrapper that applies the theorem no_hidden_state_comparison_forces_rcl (itself a reduction to counted_once_combiner_forces_rcl) under the supplied operative and no-hidden-state hypotheses.
why it matters
This declaration closes the local chain in the LogicAsFunctionalEquation module: scale-free comparison factors through positive ratios, no-hidden-state finite comparison yields counted-once composition, and counted-once comparison forces the RCL family. It thereby supplies the algebraic content of the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) at the foundation level. The result is cited by any downstream derivation that begins from logical comparison and proceeds to the phi-ladder or physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.