Pith. sign in
module module high

IndisputableMonolith.Foundation.DAlembert.FactorizationForcing

show as:
view Lean formalization →

The FactorizationForcing module packages the combiner gate that bridges factorization and associativity in the ledger framework. It defines the FactorizationAssociativityGate with symmetry, right-affine, zero-boundary and unit-diagonal properties, and proves that these force the combiner to the RCL polynomial. Downstream modules cite it to derive the Recognition Composition Law from contextual substitutivity.

claimThe FactorizationAssociativityGate (symmetry + right-affine + zero-boundary + unit-diagonal) forces the combiner $P(u,v)$ to equal the RCL polynomial $2uv + 2u + 2v$.

background

This module sits in the DAlembert factorization layer and packages the bridge between ledger substitutivity and the Recognition Composition Law. It introduces the FactorizationAssociativityGate as the packaged object whose axioms (symmetric, right-affine, zero-boundary, unit-diagonal) are used to force the combiner form.

Downstream documentation states: 'This module proves that the factorization property—and hence the Recognition Composition Law—follows from two primitive ledger properties: Contextual substitutivity'. The same gate is invoked to close Gap 4 by showing the combiner must match the RCL polynomial.

proof idea

The module defines the FactorizationAssociativityGate as the conjunction of the four listed properties. It then proves gate_forces_bilinear_family and gate_forces_rcl by algebraic reduction from those axioms to the target polynomial form.

why it matters in Recognition Science

This module supplies the packaged gate that feeds LedgerFactorization (deriving RCL from substitutivity) and RightAffineFromFactorization (closing Gap 4 by confirming the gate forces $P(u,v) = 2uv + 2u + 2v$). It advances the factorization/associativity bridge toward the full Recognition Composition Law.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (3)