error_bound_from_8_tick
plain-language theorem explainer
error_bound_from_8_tick fixes the majority voting threshold at exactly 3/8 for 8-tick phase codes. Information theorists deriving Recognition Science channel bounds would cite it when setting redundancy levels or comparing to Shannon capacity. The proof is a direct numerical normalization that equates the fraction to its decimal form.
Claim. The majority voting error threshold in the 8-tick structure satisfies $3/8 = 0.375$ in the reals.
background
The Information.ErrorCorrectionBounds module derives error correction limits from the 8-tick periodicity of Recognition Science. The tick is the fundamental time quantum, set to 1 in RS-native units. The eight phases are defined as $k pi/4$ for $k=0$ to 7, supplying natural redundancy by encoding each bit across correlated phases.
proof idea
The proof is a one-line wrapper that applies norm_num to reduce the rational equality 3/8 = 0.375 directly in the reals. No upstream lemmas beyond built-in arithmetic normalization are required.
why it matters
This supplies the concrete numerical cutoff for majority voting inside 8-tick redundancy schemes. It anchors the RS error-correction perspective that links the eight-tick octave to phase-based detection and correction. The bound supports later capacity calculations that incorporate the phi-ladder correction factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.