HasBiAffineForm
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not apply to expressions containing repeated factors or higher powers.
- Does not address infinite series, branch choices, or non-counted-once syntax.
- Does not claim bi-affinity outside the counted-once normal form.
- Does not supply an algorithm for extracting the coefficients a,b,c,d.
formal statement (Lean)
39def HasBiAffineForm (e : CountedOnceResourceExpr) : Prop :=
proof body
Definition body.
40 ∃ a b c d : ℝ, ∀ u v, eval e u v = a + b*u + c*v + d*u*v
41
42/-- Every counted-once resource expression is bi-affine. -/