referenceGap
plain-language theorem explainer
The baseline gap-to-capacity for polar codes at rung zero of the phi-ladder is fixed at the dimensionless value 1. Information theorists modeling finite-blocklength corrections within Recognition Science cite it to initialize the exponential decay sequence. The declaration is a direct constant assignment.
Claim. The reference gap-to-capacity at rung 0 of the phi-ladder equals $1$.
background
The module places polar code finite-length gaps on the phi-ladder, where adjacent rung gaps scale by the factor $1/phi$, matching the structure used for quantum-channel capacity corrections. The phi-ladder arises from the self-similar fixed point phi forced in the T0-T8 chain. Upstream rung definitions supply the same scaling index across mass anchors, asteroid spectroscopy, and athletic record models.
proof idea
This is a one-line definition that directly assigns the real number 1.
why it matters
It supplies the origin value for gapAt and gapAt_pos in the same module and for the parallel gapAtRung and gapAt functions in the athletic record and record-fit modules. The constant anchors the phi-ladder scaling for information gaps, consistent with the Recognition Composition Law and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.