HasBiAffineForm
plain-language theorem explainer
HasBiAffineForm encodes the property that a counted-once resource expression evaluates to a function of the form a + b u + c v + d u v. Researchers formalizing resource-sensitive linear logic or mechanism design cite it when they need the normal-form restriction to monomials of total degree at most two. The definition directly states the existential quantification over the four real coefficients that the evaluation map must match.
Claim. A counted-once resource expression $e$ has bi-affine form when there exist real numbers $a,b,c,d$ such that, for all real $u,v$, the evaluation satisfies $eval(e,u,v)=a+bu+cv+duv$.
background
The module formalizes the normal-form version of counted-once resource syntax. Each constituent comparison appears at most once, so the permitted scalar monomials are only 1, u, v, and uv. The inductive type CountedOnceResourceExpr supplies the constructors const, atomU, atomV, both, add, and scale; its doc-comment states that the both constructor represents the joint interaction uv and that no constructors exist for u^2, v^2, square roots, or infinite series.
proof idea
This is the direct definition of the bi-affine evaluation property. It is invoked by the downstream theorem counted_once_expr_biaffine, which discharges the existential by induction on the structure of e, and by the alias resource_linearity_gives_biaffinity.
why it matters
HasBiAffineForm supplies the target predicate for the theorem that every counted-once resource expression is bi-affine. It therefore supports the alias resource_linearity_gives_biaffinity and sits inside the linear-logic bridge that converts counted-once comparisons into affine algebraic forms. In the Recognition framework this normal form is required for subsequent mechanism-design and scalar-field evaluations that rely on linearity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.