CountedOnceResourceExpr
plain-language theorem explainer
CountedOnceResourceExpr is the inductive type of normal-form counted-once resource expressions generated by constants, atoms u and v, their product, addition, and scaling. Researchers formalizing resource-sensitive comparisons or bi-affine evaluations in the linear logic bridge cite this definition when proving that evaluation maps remain linear in each argument separately. The declaration is supplied directly as an inductive definition whose six constructors enforce the counted-once restriction by excluding higher powers and branches.
Claim. The inductive type of normal-form counted-once resource expressions, generated by constants $a$, atoms $u$ and $v$, the joint product $u v$, sums, and real scalings, with the only scalar monomials being $1$, $u$, $v$, and $u v$.
background
The module formalises the normal-form version of counted-once resource syntax for the linear logic bridge. Each constituent comparison may appear at most once, so the only scalar monomials are $1$, $u$, $v$, and $u v$. The doc-comment states that the constructor both represents the joint interaction $u v$ and that there are no constructors for $u^2$, $v^2$, square roots, branch choices, or infinite series.
proof idea
This is the inductive definition of the type CountedOnceResourceExpr with the six listed constructors.
why it matters
The type supplies the domain for the downstream theorems counted_once_expr_biaffine and expr_induces_counted_once_combiner, which establish that every such expression is bi-affine, and for NoHiddenStateComposition, which requires a counted-once resource expression whose evaluation recovers the composite cost. It therefore bridges the Recognition Composition Law to resource-linear representations without hidden states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.