pith. sign in
module module high

IndisputableMonolith.Foundation.MultiChannelJCost

show as:
view Lean formalization →

The MultiChannelJCost module defines multi-channel J-cost as the sum of individual per-channel J-costs. Experimental validation teams cite it when aggregating costs across independent substrates. The module supplies the Jcost_n family of definitions and basic lemmas.

claim$J_n(\{x_i\}_{i=1}^n) = \sum_{i=1}^n J(x_i)$ where $J$ denotes the single-channel J-cost.

background

The module imports IndisputableMonolith.Cost, which supplies the base J-cost function obeying the Recognition Composition Law. Multi-channel J-cost extends this by summation to handle independent channels or substrates.

Sibling definitions cover Jcost_n together with non-negativity, the zero condition, and symmetry. These rest on the single-channel properties already established in the Cost module.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Definitions here are imported by ThreeSubstrateValidationCert, which certifies J-cost behavior across language-model, photonic-qubit, and magnetized-plasma substrates. The module supplies the aggregation step required for the RS Exp B summary.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)