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 per-channel J-costs and supplies basic properties such as non-negativity and symmetry. Researchers extending single-channel Recognition Science cost to multiple independent substrates cite it when aggregating costs across channels. The module is definitional, importing the base J-cost from the Cost module and exporting lemmas used in validation certificates.

claimMulti-channel J-cost is $J_n(\{x_i\}_{i=1}^n) = \sum_{i=1}^n J(x_i)$, where $J$ is the single-channel J-cost, together with lemmas establishing $J_n \ge 0$, $J_n = 0$ iff all $x_i = 1$, and symmetry under permutation.

background

The module imports the Cost module, which supplies the base J-cost function central to Recognition Science. J-cost quantifies deviation from the self-similar fixed point on the phi-ladder. MultiChannelJCost extends this to multiple channels by summation, enabling aggregation across independent substrates. It also defines MultiChannelJCostCert as a certificate object for the summed cost.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the multi-channel J-cost definition and lemmas required by ThreeSubstrateValidationCert. That certificate summarizes RS Exp B results across language models (96.4% of MLP layers), photonic qubits (code rate 7/8), and magnetized plasma (convergence to x=1.036), all sharing the same J-cost predictions.

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)