theorem proved term proof

`detect_vs_correct`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 185theorem detect_vs_correct :
 186    (eightTickCode.d - 1 = 7) ∧ ((eightTickCode.d - 1) / 2 = 3) := by

proof body

Term-mode proof.

 187  constructor <;> rfl
 188
 189/-! ## Bounds from 8-Tick -/
 190
 191/-- The 8-tick structure implies natural bounds:
 192
 193    **Rate bound**: R ≤ 7/8 for single-error correction
 194    (Need 1 redundant bit per 8 for parity)
 195
 196    **Error bound**: p < 3/8 = 37.5% for majority voting
 197    (Need majority of 8 to be correct)
 198
 199    These match classical coding theory! -/

depends on (16)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Tick in IndisputableMonolith.Foundation.TimeEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
eightTickCode in IndisputableMonolith.Information.ErrorCorrectionBounds decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
correction in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi decl_use
parity in IndisputableMonolith.LedgerPostingAdjacency decl_use
Tick in IndisputableMonolith.Masses.Ribbons decl_use
Tick in IndisputableMonolith.Masses.Ribbons.Tick decl_use
Tick in IndisputableMonolith.Measurement.RSNative.Core decl_use