gap_decreasing
The theorem shows that the gap to Shannon capacity for an LDPC code of block length N decreases strictly as N grows under the phi-suppression model. Coding theorists analyzing finite-length LDPC performance bounds would cite this monotonicity when comparing codes at different block sizes. The proof is a term-mode reduction that unfolds the gap definition and applies positivity and reciprocal inequalities from the real numbers.
claimLet $N_1, N_2$ be positive reals with $N_1 < N_2$. Then the gap to capacity satisfies $1/ (phi N_2) < 1/(phi N_1)$, where the gap is $g(N) = 1/(phi N)$ and $phi$ denotes the golden ratio.
background
In this module the gap to capacity is defined by gapToCapacity N := 1/(phi * N), the finite-N correction to Shannon capacity under the phi-suppression law for LDPC codes. The module documentation states that LDPC codes achieve this gap when variable-node degree is at least 3, check-node degree at least 4, and Tanner-graph girth at least 6. Upstream, lt_trans from ArithmeticFromLogic supplies order transitivity (adapted from LogicNat to reals), while gapToCapacity supplies the explicit functional form.
proof idea
The term proof first unfolds gapToCapacity. It obtains 0 < N2 by lt_trans on the hypotheses, then uses phi_pos together with mul_pos to secure positivity of phi * N1 and phi * N2. The scaled inequality phi * N1 < phi * N2 follows from mul_lt_mul_of_pos_left, after which one_div_lt_one_div_of_lt delivers the reciprocal comparison.
why it matters in Recognition Science
The result is assembled into the LDPCRateCert record as the gap_monotone field, alongside gap_pos, gap_doubling_halves and gap_times_N_invariant. It completes the monotone-decreasing clause of the phi-suppression law g(N) = 1/(phi N) described in the module documentation. Within the Recognition framework it supports the T5 J-uniqueness and phi fixed-point structure that generate the 1/(phi N) scaling, and it bears on the empirical falsifier of stable gaps outside this law for corpora of at least 100 LDPC codes.
scope and limits
- Does not derive the explicit gap formula 1/(phi N).
- Does not treat non-LDPC error-correcting codes.
- Does not convert the gap into decibel units.
- Does not bound decoder convergence speed.
Lean usage
have h_dec : gapToCapacity N2 < gapToCapacity N1 := gap_decreasing h1 h_ltformal statement (Lean)
58theorem gap_decreasing {N₁ N₂ : ℝ} (h₁ : 0 < N₁) (h_lt : N₁ < N₂) :
59 gapToCapacity N₂ < gapToCapacity N₁ := by
proof body
Term-mode proof.
60 unfold gapToCapacity
61 have h₂ : 0 < N₂ := lt_trans h₁ h_lt
62 have hp : 0 < phi := phi_pos
63 have hphi_N1 : 0 < phi * N₁ := mul_pos hp h₁
64 have hphi_N2 : 0 < phi * N₂ := mul_pos hp h₂
65 -- 1 / (phi * N₂) < 1 / (phi * N₁) since phi * N₁ < phi * N₂
66 have h_lt' : phi * N₁ < phi * N₂ := mul_lt_mul_of_pos_left h_lt hp
67 exact one_div_lt_one_div_of_lt hphi_N1 h_lt'
68
69/-- Doubling N halves the gap. -/