IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge
This module introduces normal-form counted-once resource expressions that realize bi-affine cost combiners. It supplies the inductive type whose only interaction constructor is the product term for joint u*v costs. Researchers formalizing comparison composition in functional equations cite it to enforce the counted-once rule. The module is purely definitional and contains no theorems.
claimThe module defines the inductive type of counted-once resource expressions whose normal form is $a + b u + c v + d uv$ for component costs $u,v$, with no constructors for $u^2$, $v^2$, roots, branches or series.
background
The module belongs to the LogicAsFunctionalEquation section of the Recognition Science foundation. It imports CountOnceComparison, whose doc-comment states that each constituent comparison is counted once, so the combiner must be affine in each variable separately: $a + b u + c v + d u v$ for component costs $u$ and $v$ (UPSTREAM). The sibling definitions CountedOnceResourceExpr, eval, HasBiAffineForm and the lemmas counted_once_expr_biaffine, expr_induces_counted_once_combiner, resource_linearity_gives_biaffinity implement this algebraic restriction.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the concrete expressions required by the downstream NoHiddenState module (DOWNSTREAM), whose doc-comment describes no-hidden-state composition as the composite cost being supplied by a counted-once resource expression. It thereby closes the formal version of no hidden route memory, no branch choice, no infinite series and no reuse of a constituent comparison.
scope and limits
- Does not admit constructors for squares, roots or infinite series.
- Does not encode branch choice or hidden state in the combiner.
- Does not relax the counted-once restriction to allow reuse of a constituent comparison.