IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge
Defines normal-form counted-once resource expressions whose only joint constructor is the product interaction u·v. The module proves these expressions evaluate to bi-affine combiners a + b u + c v + d u v, and conversely that resource linearity yields bi-affinity. Anyone citing the no-hidden-state composition law uses this bridge. The argument is inductive on the expression grammar plus direct algebraic expansion.
claimA counted-once resource expression in costs $u,v$ is built from constants and the single joint constructor $\mathrm{both}(u,v)=u\cdot v$ (no $u^2$, $v^2$, roots, branches, or series). Every such expression evaluates to a bi-affine form $a + b u + c v + d u v$. Conversely, any combiner that is resource-linear (affine in each argument separately) arises from such an expression.
background
Recognition Science treats logical composition of comparisons as a cost-combiner problem. Upstream, CountOnceComparison fixes the algebraic meaning of "each constituent comparison is counted once": for component costs $u$ and $v$, the combiner must be affine in each variable separately, i.e. of the shape $a + b u + c v + d u v$.
This module supplies the corresponding expression language. The inductive type of counted-once resource expressions admits constants and a single binary constructor for the joint interaction $u\cdot v$. There are deliberately no constructors for squares, square roots, nondeterministic branch choice, or infinite series, so the grammar itself enforces the counted-once discipline.
Evaluation of an expression is the obvious fold into the reals (or the ambient cost semiring). Bi-affinity is the predicate that a binary function has the four-coefficient shape above. The module sits in the Logic-as-Functional-Equation layer of the Foundation stack, between the raw counted-once comparison algebra and the no-hidden-state composition law.
proof idea
This is primarily a definition-and-bridge module. The expression type and its evaluator are introduced by induction on a small grammar. Bi-affinity of every evaluated expression is proved by structural induction: constants are bi-affine, and the product constructor preserves the four-coefficient shape under expansion. The converse direction (resource linearity implies existence of a counted-once expression) is a direct coefficient extraction: read off $a,b,c,d$ from the affine-in-each-variable hypothesis and assemble the matching expression. Named siblings package these directions as the biaffine theorem, the induced-combiner map, and the linearity-to-biaffinity lemma.
why it matters in Recognition Science
Downstream, NoHiddenState imports this module and defines no-hidden-state composition to mean: the composite cost is exactly a counted-once resource expression in the two constituent costs. That is the formal reading of "no hidden route memory, no branch choice, no infinite series, and no reuse of a constituent comparison."
Without the expression grammar and the bi-affinity bridge, the no-hidden-state claim would be only informal English. The module therefore closes the gap between the algebraic CountOnceComparison law and the logical composition principle used later in the forcing chain. In the broader Recognition framework it keeps cost composition inside the same J-cost / functional-equation discipline that forces $\varphi$, the eight-tick octave, and $D=3$, by forbidding combinators that would smuggle extra state or nonlinear reuse into the comparison.
scope and limits
- Does not derive the J-cost functional equation or force $\varphi$; it only classifies combiners.
- Does not treat multi-way (n>2) composition; the grammar is binary in two constituent costs.
- Does not allow or analyze squares, roots, branches, or series; those are excluded by construction.
- Does not prove physical no-hidden-variables theorems; it only formalizes cost-expression linearity.
- Does not itself state the no-hidden-state law; that lives in the downstream module.