Pith. sign in
module module high

IndisputableMonolith.Information.ErrorCorrectionCodesFromJCost

show as:
view Lean formalization →

Module defines error correction code families derived from the J-cost on the phi-ladder in Recognition Science. It introduces ECCFamily together with thresholdGap(r) = 1-r and proves that deeper families produce strictly smaller gaps. Information theorists working in the RS framework would cite these objects when constructing phi-parameterized codes. The module consists of definitions plus short lemmas on counts, positivity, and monotonicity.

claimIntroduces the family $\mathrm{ECCFamily}$ of error-correcting codes indexed by depth on the $\phi$-ladder, together with the threshold-gap function satisfying $\mathrm{thresholdGap}(r)=1-r$ and the strict decrease $\mathrm{thresholdGap}_{k+1}<\mathrm{thresholdGap}_k$ for successive depths $k$.

background

The module lies in the Information domain and imports the RS time quantum $\tau_0=1$ tick from Constants. It operates with the J-cost $J(x)$ defined in the forcing chain (T5) and the phi-ladder mass formula. The supplied doc-comment states the central claim: decoding threshold gap $1-r$ on the $\phi$-ladder decreases for deeper families.

proof idea

This is a definition module. It declares ECCFamily, eccFamily_count, thresholdGap, ECCCert and eccCert, then supplies three short lemmas (thresholdGap_pos, thresholdGap_strictDecr) that verify positivity and strict decrease by direct comparison on the phi-ladder.

why it matters in Recognition Science

Supplies the error-correction constructions required by any later information-theoretic results in Recognition Science. It directly realizes the decoding-threshold statement given in the module doc-comment and connects to the J-cost and phi-ladder landmarks of the T0-T8 chain. No downstream uses are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)