resource_linearity_gives_biaffinity
plain-language theorem explainer
Every normal-form counted-once resource expression evaluates to a bi-affine function of two scalar variables. Researchers embedding linear logic into functional equations or resource-sensitive calculi would cite this when confirming that syntactic restrictions preserve semantic linearity. The proof is a direct one-line application of the induction theorem establishing bi-affinity for the entire inductive family.
Claim. Let $e$ be a counted-once resource expression. Then there exist $a,b,c,d$ in the reals such that for all real $u,v$ the evaluation of $e$ satisfies $eval(e)(u,v)=a+bu+cv+duv$.
background
The module introduces normal-form counted-once resource syntax in which each constituent comparison appears at most once. The inductive type CountedOnceResourceExpr is generated by constants, the atoms $u$ and $v$, their product via the both constructor, binary addition, and real scaling; no repeated factors, roots, or series are admitted. HasBiAffineForm is the semantic property asserting that the evaluation map of any such expression is exactly affine in each variable separately plus a bilinear cross term. The upstream theorem counted_once_expr_biaffine proves the property for every element of the inductive type by structural induction on the constructors.
proof idea
One-line wrapper that applies the induction theorem counted_once_expr_biaffine to the given expression.
why it matters
The declaration supplies a searchable alias for the bi-affinity result inside the LinearLogicBridge module, which formalises resource-sensitive syntax as a bridge toward the Recognition functional equation. It confirms that the counted-once restriction is compatible with the bi-affine semantics required by the larger logic-as-functional-equation development. No downstream uses are recorded yet, so the entry functions primarily as an explicit interface point rather than a lemma in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.