CountedOnceResourceExpr
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.