counted_once_expr_biaffine
plain-language theorem explainer
Every normal-form counted-once resource expression evaluates to a bi-affine function of two variables. Workers on resource-sensitive linear logic or the functional-equation bridge in Recognition Science cite it to keep expressions inside the span of 1, u, v, uv. The proof is structural induction on the six constructors of CountedOnceResourceExpr, exhibiting coefficients for each base case and closing under addition and scaling by ring arithmetic.
Claim. For every counted-once resource expression $e$, 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 supplies a normal-form syntax for counted-once resource comparisons in which each constituent may appear at most once; the only scalar monomials permitted are therefore 1, u, v and uv. CountedOnceResourceExpr is the inductive type generated by const (a real constant), atomU, atomV, both (the product term), add and scale. The predicate HasBiAffineForm asserts that the evaluation map of such an expression lies in the four-dimensional vector space spanned by those monomials. The evaluation function is defined by structural recursion: constants ignore the variables, atomU returns u, atomV returns v, both returns the product, and add and scale distribute in the obvious way.
proof idea
The proof proceeds by induction on the structure of e. Base cases const, atomU, atomV and both each supply explicit coefficients (a,0,0,0), (0,1,0,0), (0,0,1,0) and (0,0,0,1) respectively and discharge the universal quantifier by simp on eval. The add case combines the four-tuples from the two inductive hypotheses and invokes ring to verify the summed expression. The scale case multiplies the coefficient tuple by the scalar k and again uses ring after simp on eval.
why it matters
The result is invoked directly by expr_induces_counted_once_combiner and by the alias resource_linearity_gives_biaffinity, both of which sit inside the same LinearLogicBridge module. It therefore supplies the semantic guarantee that every counted-once expression remains bi-affine, a prerequisite for embedding the resource syntax into the larger functional-equation framework that derives the Recognition Composition Law and the eight-tick octave. No open scaffolding is closed here; the theorem is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.