pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.MultiChannelJCost

show as:
view Lean formalization →

The module defines multi-channel J-cost as the sum of per-channel J-costs to aggregate costs across independent substrates. Researchers validating Recognition Science predictions in language models, photonic systems, and plasma would cite it for shared J-cost behavior. It supplies basic properties such as non-negativity and symmetry through direct definitions and short lemmas.

claimThe multi-channel J-cost is $J_n(x_1, x_2, ..., x_n) = J(x_1) + J(x_2) + ... + J(x_n)$, where each $J(x_i)$ satisfies the single-channel functional equation from the Cost module.

background

J-cost is introduced in the upstream Cost module via the Recognition Composition Law: $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. The present module extends this to multiple channels by defining Jcost_n and its variants (Jcost_n_nonneg, Jcost_n_symm, Jcost_n_zero_iff). These support simultaneous application across distinct physical or computational substrates without altering the underlying J function.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the aggregate cost object required by the downstream ThreeSubstrateValidationCert, which records 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). It thereby enables the claim that all three substrates obey 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)