CountedOnceResourceExpr
CountedOnceResourceExpr supplies the inductive syntax for normal-form resource expressions restricted to constants, the atoms u and v, their product, sums, and scalings. Researchers formalizing resource-sensitive linear logic or the Recognition Composition Law cite it when proving that evaluations remain bi-affine. The definition is introduced directly via six constructors that exclude squares, roots, and higher-order terms.
claimThe inductive type of counted-once resource expressions is generated by the constructors const(a) for a real constant a, atomU, atomV, both (representing the product u v), add(e1, e2), and scale(r, e) for real r. Its evaluations are exactly the functions of the form a + b u + c v + d u v.
background
The module formalizes resource-sensitive syntax for counted-once comparisons. Each constituent comparison appears at most once, so the only scalar monomials are 1, u, v, and u v. This syntax bridges resource expressions to bi-affine forms while respecting the counted-once restriction stated in the module documentation.
proof idea
This is an inductive definition. It introduces the six constructors directly: const for real constants, atomU and atomV for the two atoms, both for the joint product, add for sums, and scale for real multiples. No lemmas or tactics are invoked; the type itself encodes the normal form.
why it matters in Recognition Science
The definition feeds the theorems counted_once_expr_biaffine and expr_induces_counted_once_combiner, which establish bi-affinity for every such expression. It supplies the syntax for NoHiddenStateComposition, ensuring composite costs arise from a single counted-once resource expression without hidden state. In the Recognition framework it supports the Recognition Composition Law by limiting terms to those compatible with the phi-ladder and the eight-tick octave.
scope and limits
- Does not include constructors for u squared or v squared.
- Does not permit roots, infinite series, or branch choices.
- Does not represent general nonlinear resource interactions.
- Does not encode persistent state across multiple comparisons.
formal statement (Lean)
19inductive CountedOnceResourceExpr where
20 | const : ℝ → CountedOnceResourceExpr
21 | atomU : CountedOnceResourceExpr
22 | atomV : CountedOnceResourceExpr
23 | both : CountedOnceResourceExpr
24 | add : CountedOnceResourceExpr → CountedOnceResourceExpr → CountedOnceResourceExpr
25 | scale : ℝ → CountedOnceResourceExpr → CountedOnceResourceExpr
26
27namespace CountedOnceResourceExpr
28
29/-- Evaluation of a counted-once resource expression. -/