NoHiddenStateComposition
NoHiddenStateComposition is a structure that encodes the no-hidden-state composition property for a comparison operator C. It packages an expression in the counted-once resource language together with symmetry and the exact identity that reproduces the sum of derived costs under multiplication and division. Researchers tracing the logic-to-RCL step in Recognition Science cite this definition when showing that operative comparisons without hidden states force the full RCL family. The declaration is a direct structure definition with three fields
claimLet $C$ be a comparison operator. A no-hidden-state composition for $C$ consists of a counted-once resource expression $e$ such that evaluation of $e$ is symmetric in its two arguments and satisfies derivedCost$_C(xy) +$ derivedCost$_C(x/y) = e($derivedCost$_C x,$ derivedCost$_C y)$ for all positive reals $x,y$, where derivedCost$_C(r) := C(r,1)$.
background
The module defines no-hidden-state composition to mean that the composite cost is supplied exactly by a counted-once resource expression evaluated on the two constituent costs. This is the formal counterpart of the statement that comparison carries no hidden route memory, branch choice, infinite series, or reuse of a constituent comparison. A ComparisonOperator is a map from pairs of positive reals to a real-valued cost obeying the four Aristotelian constraints. The derivedCost function extracts the cost relative to the unit: derivedCost C r := C r 1. CountedOnceResourceExpr is the inductive type whose constructors are const, atomU, atomV, both (representing the product), and add; its eval substitutes the arguments to produce the corresponding combination, with both yielding the product of the two inputs.
proof idea
This declaration is a structure definition. It directly assembles the three required components: the resource expression, the symmetry axiom on its evaluation, and the composition identity relating the sum of derived costs to the evaluated expression.
why it matters in Recognition Science
NoHiddenStateComposition supplies the key hypothesis for the theorem no_hidden_state_logic_forces_rcl, which concludes that an operative positive-ratio comparison satisfying this property forces the RCL family on its derived cost. It thereby completes the bridge from the linear-logic constraints to the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The definition therefore sits at the foundation step that later yields J-uniqueness and the phi-ladder mass formula.
scope and limits
- Does not prove existence of the counted-once expression for a given C.
- Does not impose the four Aristotelian constraints on the comparison operator.
- Does not derive numerical values for constants such as alpha or G.
- Does not address spatial dimension D=3 or the eight-tick octave.
formal statement (Lean)
20structure NoHiddenStateComposition (C : ComparisonOperator) where
21 expr : CountedOnceResourceExpr
22 symmetric_expr : ∀ u v, CountedOnceResourceExpr.eval expr u v =
23 CountedOnceResourceExpr.eval expr v u
24 composition : ∀ x y : ℝ, 0 < x → 0 < y →
25 derivedCost C (x * y) + derivedCost C (x / y) =
26 CountedOnceResourceExpr.eval expr (derivedCost C x) (derivedCost C y)
27
28/-- No-hidden-state composition implies counted-once composition. -/