eightTickCadence
plain-language theorem explainer
The eight-tick cadence is defined as the fixed interval 8τ₀ required for one complete recognition cycle. Black-hole and holographic-information researchers cite it when the factor of 8 appears in Hawking temperature or entropy-bandwidth identities. The definition is introduced by direct assignment of eight times the base tick duration τ₀ with no further computation.
Claim. The eight-tick cadence is the duration of one full recognition cycle, equal to $8τ_0$, where $τ_0$ is the fundamental tick interval.
background
The RecognitionBandwidth module defines recognition bandwidth as the maximum rate of ledger events allowed inside a holographically bounded region. It links five previously separate elements: the holographic bound on information (area over 4 Planck areas), the per-bit recognition cost k_R = ln(φ), ILG parameters, the 8-tick cadence, and boundary coherence costs. The cadence supplies the processing-time denominator in the bandwidth formula R_max = A / (4ℓ_P² · k_R · 8τ₀).
proof idea
This is a direct definition that assigns eightTickCadence to the product 8 * τ₀. No lemmas or tactics are invoked; the value is set explicitly to encode the eight-tick octave.
why it matters
The definition supplies the 8τ₀ factor used in horizonBandwidth, hawking_contains_eight_tick, and entropy_is_bandwidth_capacity. It realizes the T7 eight-tick octave step of the forcing chain and closes the link between holographic capacity and the minimum time for one recognition event. Downstream results quote it to show that the 8 in Hawking temperature equals the recognition cycle time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.