CountedOnceResourceExpr
plain-language theorem explainer
Normal-form counted-once resource expressions supply the syntax for resource-sensitive comparisons inside the linear logic bridge. Researchers formalizing bi-affine evaluation maps and no-hidden-state composition laws cite this inductive definition. The definition is introduced directly via six constructors that restrict monomials to 1, u, v, and uv.
Claim. The inductive type of normal-form counted-once resource expressions generated by constants $a$, atoms $u$ and $v$, their product interaction, addition, and real scaling, with no constructors for squares, roots, or series.
background
The module formalises the normal-form version of counted-once resource syntax. Each constituent comparison appears at most once, so the only scalar monomials permitted are 1, u, v, and uv. The constructor both encodes the joint interaction uv.
proof idea
This is a definition of an inductive type. It introduces the six constructors const, atomU, atomV, both, add, and scale with no proof obligations or computational content.
why it matters
The definition supplies the syntax required by the theorem that every counted-once resource expression is bi-affine and by the structure NoHiddenStateComposition. It fills the resource-sensitive syntax step that connects the Recognition Composition Law to linear logic bridges in the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.