no_hidden_state_implies_counted_once
plain-language theorem explainer
No-hidden-state composition for a comparison operator implies counted-once composition. Researchers deriving the Recognition Composition Law from the functional equation would cite this to remove hidden-state assumptions before invoking RCL. The proof is a direct term construction that supplies the combiner via evaluation of the resource expression and checks the three required properties.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. If there exists a counted-once resource expression $e$ such that the derived cost satisfies $derivedCost_C(xy) + derivedCost_C(x/y) = eval(e, derivedCost_C x, derivedCost_C y)$ together with symmetry of the evaluation, then there exists a function $P$ that is a counted-once combiner, symmetric, and obeys the same composition identity for the derived cost of $C$.
background
A comparison operator $C$ maps pairs of positive reals to a real cost and satisfies the four Aristotelian structural constraints. The derived cost fixes the second argument at the multiplicative identity. NoHiddenStateComposition is the structure whose fields are a CountedOnceResourceExpr, a symmetry statement on its evaluation, and the explicit composition equation that equates the sum of derived costs on product and quotient to the evaluation of that expression. CountedOnceComposition is the proposition that such a combiner $P$ exists and is bi-affine, symmetric, and reproduces the composition law. The module establishes that no-hidden-state comparisons force the RCL family; upstream, ComparisonOperator encodes well-posed comparison and CountedOnceResourceExpr normalizes expressions without reuse, branches, or infinite series.
proof idea
The proof is a term-mode construction. It builds the required combiner as the evaluation map of the resource expression supplied by the hypothesis. It then invokes the upstream lemma that every counted-once resource expression induces a counted-once combiner, and directly supplies the symmetry and composition fields already present in the NoHiddenStateComposition hypothesis.
why it matters
This result supplies the intermediate step that lets a no-hidden-state operative comparison force the RCL family in the downstream theorem no_hidden_state_comparison_forces_rcl. Within Recognition Science it supports passage from the functional equation to the Recognition Composition Law without hidden memory, consistent with J-uniqueness (T5) and the eight-tick octave (T7). It closes one link in the chain from the no-hidden-state assumption to the phi-ladder and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.