bandwidth_eq_bits_over_cost
plain-language theorem explainer
Recognition bandwidth for positive area A equals holographic bit capacity divided by the product of per-bit cost k_R and the eight-tick cadence. Workers deriving maximum ledger throughput from holographic bounds cite this identity. The proof reduces to unfolding the two definitions then applying ring normalization.
Claim. For $A > 0$, the recognition bandwidth satisfies $R(A) = S(A) / (k_R · 8 τ_0)$, where $S(A)$ is the holographic bit capacity, $k_R = ln φ$ the per-bit ledger cost, and $τ_0$ the fundamental tick.
background
The module connects the holographic bound (maximum information proportional to boundary area over four Planck areas), the recognition cost per bit $k_R = ln φ$, and the eight-tick cadence completing one cycle per $8 τ_0$. Recognition bandwidth is defined as the maximum rate of recognition events within a holographically bounded region, $R_max = S_holo / (k_R · 8 τ_0) = A / (4 ℓ_P² · ln φ · 8 τ_0)$. This theorem supplies the direct equality of bandwidth to holographicBits A over ($k_R$ times eightTickCadence), using the upstream tick definition as the RS time quantum and $k_R$ as the Boltzmann analog from Constants.BoltzmannConstant.
proof idea
Term-mode proof that unfolds the definitions of bandwidth and holographicBits, then applies the ring tactic to confirm the algebraic identity.
why it matters
It directly supports the rearrangement in bandwidth_times_cost_eq_rate, which recovers the bit capacity as bandwidth multiplied by cost. The result closes the core definition of recognition bandwidth as the hard ceiling on ledger throughput imposed by the holographic bound and per-bit cost, aligning with the T7 eight-tick octave. The module notes this supplies a hard ceiling on ledger throughput.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.