gapAt
GapAt(k) equals the reference gap of 1 scaled by phi to the power minus k on the phi-ladder. Information theorists modeling finite-length polar code performance in Recognition Science cite this definition, which mirrors the athletic record gap model. It is introduced as a direct algebraic expression with no additional computation.
claimThe gap-to-capacity at rung $k$ on the phi-ladder is $1 · ϕ^{-k}$ for natural number $k$, where the reference gap at rung 0 is normalized to 1.
background
The PolarCodeGapFromPhi module places polar-code gap-to-capacity on the phi-ladder, where adjacent gaps stand in ratio 1/phi. This matches the structure already used for athletic-record gaps in RecordProgressionFit. referenceGap is defined as the RS-native dimensionless value 1 at the base rung.
proof idea
One-line definition that substitutes referenceGap := 1 and applies the integer power phi ^ (-(k : ℤ)).
why it matters in Recognition Science
This definition supplies the base object for PolarCodeCert and the ratio theorems gapAt_pos, gapAt_succ_ratio, gapAt_adjacent_ratio. It places polar-code gaps in the same phi-ladder used by RecordProgressionFit, consistent with the self-similar fixed point of T6. No open scaffolding remains in the module.
scope and limits
- Does not derive the phi-ladder ratio from the Recognition Composition Law.
- Does not map block length N to a concrete rung k.
- Does not recover the O(2^{-N^{0.5}}) decay rate of polar codes.
- Does not compute explicit numerical gaps for finite N.
formal statement (Lean)
29def gapAt (k : ℕ) : ℝ := referenceGap * phi ^ (-(k : ℤ))
proof body
Definition body.
30