pith. sign in
module module high

IndisputableMonolith.Foundation.DAlembert.RightAffineFromFactorization

show as:
view Lean formalization →

The module proves that bilinearity of a cost functional implies it is right-affine in the second argument. Researchers closing the algebraic core of the B2 program in Recognition Science cite this step after factorization is established. The argument consists of direct algebraic expansions that apply the Recognition Composition Law to reduce the bilinear assumption to the affine form.

claimIf the cost combiner $C$ is bilinear then $C(x, yz)$ is affine in the second variable, i.e., there exist functions $a$ and $b$ such that $C(x, y) = a(x) + b(x) g(y)$ for an appropriate $g$.

background

This module belongs to the D'Alembert series that derives the functional equation as the unique multiplicative form for cost consistency. It imports the Recognition Composition Law from Cost.FunctionalEquation and the factorization-plus-compatibility core from FactorizationForcing. The upstream LedgerFactorization module supplies the passage from contextual substitutivity to the RCL, while Inevitability and Unconditional establish that the d'Alembert equation follows once the affine response is available.

proof idea

The module organizes four main results. bilinear_implies_right_affine performs the direct algebraic reduction from the bilinear hypothesis to the right-affine conclusion using the RCL identity. rcl_right_affine specializes the result to the Recognition Composition Law case. polynomial_consistency_implies_right_affine and gate_from_polynomial_consistency handle the polynomial route, while polynomial_consistency_forces_rcl and rcl_without_gate close the remaining implications.

why it matters in Recognition Science

The result supplies the missing algebraic step identified in FactorizationForcing: once factorization and three-way compatibility are in hand, the combiner must be affine on the right. This feeds directly into Unconditional, which proves RCL inevitability with no assumption on the probability measure P. The module therefore closes the pure-algebra portion of the chain from ledger properties to the d'Alembert equation.

scope and limits

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (6)