eval
plain-language theorem explainer
The definition supplies a recursive map that interprets normal-form counted-once resource expressions as real-valued functions of two parameters u and v. Circuit-modeling and constant-derivation work in Recognition Science cites it to convert syntactic resource expressions into numerical values under the counted-once restriction. The map is realized by direct pattern matching on the six constructors of the inductive type, applying identity, multiplication, addition, or scaling in each case.
Claim. Let $e$ be a counted-once resource expression. The evaluation function assigns to each $e$ and real numbers $u,v$ a real number by the rules: constant $a$ yields $a$; atom for $u$ yields $u$; atom for $v$ yields $v$; joint product yields $u v$; sum of subexpressions yields the sum of their evaluations; and scaling by $k$ multiplies the subexpression evaluation by $k$.
background
The module supplies the normal-form syntax for counted-once comparisons in which each factor appears at most once. The inductive type therefore contains only constants, the distinguished atom for the first variable, the atom for the second variable, their product constructor, binary addition, and real scaling; squares, roots, and series are excluded by construction. Evaluation interprets any such expression as a function of the two real parameters that label the atoms.
proof idea
The definition is given directly by pattern matching on the constructors of the inductive type. The constant case returns the stored real, the two atom cases return the corresponding parameter, the product case multiplies the two parameters, the addition case recurses and adds, and the scaling case multiplies the recursive value by the coefficient.
why it matters
The definition is invoked by BooleanCircuitWithEval, CircuitDecides, and CircuitWithEvalDecides to supply concrete evaluation functions for resource-sensitive circuits. It also appears in the status summaries for constant derivation, dimension analysis, and RS-native units. Within the framework it supplies the semantic bridge that lets linear resource expressions be evaluated consistently with the Recognition Composition Law and the phi-ladder scaling used throughout the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.