pith. sign in
module module high

IndisputableMonolith.Foundation.DAlembert.RightAffineFromFactorization

show as:
view Lean formalization →

The module establishes that a bilinear combiner on cost functionals implies right-affine response in the second argument. Researchers tracing the algebraic steps of the B2 closure program in Recognition Science cite it after the factorization results. The structure imports ledger factorization and inevitability modules then reduces the bilinear case via algebraic identities to the affine form.

claimIf the combiner $C$ satisfies bilinearity then $C(x,y)=a(x)+b(x)y$ for functions $a,b$ (right-affine in the second slot).

background

The module sits inside the d'Alembert inevitability development. Cost and FunctionalEquation supply the T5 cost uniqueness helpers and the Recognition Composition Law. FactorizationForcing states that factorization plus three-way compatibility yields affine response in the second argument, after which the remaining steps are pure algebra. LedgerFactorization derives the factorization property from contextual substitutivity and ledger consistency.

proof idea

The module imports the six upstream modules and proves the listed sibling implications. Each sibling reduces the bilinear assumption to right-affine form by applying the factorization and inevitability lemmas already established in the imported files.

why it matters in Recognition Science

It supplies the affine response required by the B2 closure program. The result feeds the unconditional RCL inevitability theorem, which shows the d'Alembert equation holds with no assumption on the probability measure P. This completes the analytic passage described in the FactorizationForcing module doc-comment.

scope and limits

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (6)