IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge
This module defines normal-form counted-once resource expressions to capture joint interactions between two costs. Researchers formalizing comparison composition cite it to enforce the counted-once condition without reuse. The central inductive type uses a both constructor for the product term while excluding squares, roots, and series. It realizes the bi-affine combiner a + b u + c v + d u v directly from the upstream count-once formalization.
claimExpressions take the normal form $a + b u + c v + d u v$, where $u$ and $v$ are constituent costs and $a,b,c,d$ are constants. The inductive type admits a both constructor for the joint term $u v$ but no constructors for $u^2$, $v^2$, square roots, branch choices, or infinite series.
background
The module belongs to the LogicAsFunctionalEquation development and imports CountOnceComparison, whose doc-comment states that each constituent comparison is counted once. This algebraic requirement forces the combiner to be affine in each variable separately, producing the form a + b u + c v + d u v.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the counted-once expressions required by the downstream NoHiddenState module to formalize no-hidden-state comparison composition. Its doc-comment describes this as ruling out hidden route memory, branch choice, infinite series, and reuse of a constituent comparison, thereby advancing the formalization of logic as a functional equation.
scope and limits
- Does not include constructors for squared terms u^2 or v^2.
- Does not permit infinite series or branch choices.
- Does not model hidden states or reuse of comparisons.