Pith. sign in
module module moderate

IndisputableMonolith.Information.LDPCCodeRateFromPhi

show as:
view Lean formalization →

This module computes the gap to Shannon capacity for LDPC codes of block length N by applying the J-cost band. Information theorists working inside Recognition Science cite it when closing domain certificates in the B-tier chain. The module applies the six-clause template imported from CanonicalJBand to certify nonnegativity and related properties of the gap.

claimGap to Shannon capacity $\Delta(N)$ for an LDPC code of block length $N$, obtained by applying the J-cost-on-ratio template to the code rate.

background

The module resides in the Information domain and imports CanonicalJBand. That upstream module supplies the reusable six-clause J-cost-on-ratio template used across the master cert chain. The template proves J(1) = 0 and J(x) ≥ 0 for x > 0.

The local setting is the derivation of information rates inside Recognition Science, where the J function encodes the recognition cost on ratios and the phi-ladder supplies the underlying scale. The module therefore translates the general band into a concrete gap function for LDPC codes.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies one of the B-tier domain certificates in the master cert chain. It applies the Canonical J-Cost Band template to LDPC rates, thereby extending the J-band machinery into the information domain and supporting the overall forcing chain from the single functional equation to physical constants.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)