IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge
This module defines the inductive type of normal-form counted-once resource expressions for two costs u and v. Researchers formalizing no-hidden-state composition in the Recognition Science framework would cite it. The module restricts constructors to affine forms plus a single joint interaction term, excluding powers, roots, branches, and series.
claimExpressions of the form $a + b u + c v + d uv$, generated by constants and the bilinear constructor for the joint term $uv$.
background
The upstream CountOnceComparison module shows that counted-once comparisons are algebraically affine in each variable separately, yielding the combiner $a + b u + c v + d u v$. This module supplies the normal-form inductive type realizing that structure. The local setting is the formalization of logic as a functional equation, where resource expressions model comparisons that carry no hidden route memory.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
This module supplies the expressions required by the downstream NoHiddenState module to formalize no-hidden-state comparison composition. It fills the counted-once resource requirement in the Recognition framework's treatment of logic as functional equation, enforcing the absence of hidden states, branch choices, and reuse.
scope and limits
- Does not include constructors for squared terms $u^2$ or $v^2$.
- Does not permit square roots or infinite series.
- Does not allow branch choices in the expressions.
- Does not model reuse of a constituent comparison.