expr_induces_counted_once_combiner
A counted-once resource expression built from constants, single atoms u or v, their product, and sums induces a combiner that is affine in each argument separately. Researchers formalizing resource-sensitive comparisons or no-hidden-state principles cite this to connect syntactic normal forms to the functional equation side of the framework. The proof is a one-line wrapper that invokes the bi-affinity result for such expressions.
claimLet $e$ be a counted-once resource expression. Then the map $(u,v)mapsto eval(e,u,v)$ satisfies the counted-once combiner property: there exist real numbers $a,b,c,d$ such that $eval(e,u,v)=a+bu+cv+duv$ for all real $u,v$.
background
CountedOnceResourceExpr is the inductive type of normal-form expressions whose constructors are constants, the atom for $u$, the atom for $v$, the joint term for $u v$, binary addition, and scaling by a real constant. No constructors exist for repeated factors, roots, or series, enforcing the counted-once discipline. CountedOnceCombiner is the predicate asserting that a binary function $P$ is affine in each argument separately, i.e., $P(u,v)=a+bu+cv+duv$ for some reals $a,b,c,d$. The module sets up resource-sensitive syntax for counted-once comparison, restricting scalar monomials to $1$, $u$, $v$, and $u v$. The upstream result counted_once_expr_biaffine states that every such expression is bi-affine, which is the direct source of the present claim.
proof idea
The proof is a one-line wrapper that applies the theorem counted_once_expr_biaffine to the given expression $e$. That upstream theorem proceeds by induction on the structure of $e$, handling the constant, atom, both, add, and scale cases by exhibiting the four coefficients explicitly and verifying the affine identity.
why it matters in Recognition Science
This declaration supplies the missing link that lets a syntactic counted-once expression be treated as a counted-once combiner. It is invoked inside no_hidden_state_implies_counted_once to convert a NoHiddenStateComposition hypothesis into a CountedOnceComposition statement. In the broader Recognition Science setting the result supports the passage from resource-sensitive logic to the functional equation side, where bi-affine forms are the normal objects that satisfy the Recognition Composition Law.
scope and limits
- Does not assert that arbitrary expressions outside this normal form are counted-once combiners.
- Does not address expressions containing repeated factors, roots, or infinite series.
- Does not claim uniqueness of the coefficients $a,b,c,d$.
- Does not extend the result to non-real scalars or higher-dimensional inputs.
Lean usage
refine ⟨fun u v => CountedOnceResourceExpr.eval h.expr u v, ?_, ?_, ?_⟩; exact CountedOnceResourceExpr.expr_induces_counted_once_combiner h.exprformal statement (Lean)
78theorem expr_induces_counted_once_combiner
79 (e : CountedOnceResourceExpr) :
80 CountedOnceCombiner (fun u v => eval e u v) := by
proof body
Term-mode proof.
81 exact counted_once_expr_biaffine e
82
83/-- Searchable alias: resource-linearity gives bi-affinity. -/