pith. machine review for the scientific record. sign in
def definition def or abbrev high

holographicBits

show as:
view Lean formalization →

holographicBits computes the total information capacity in bits for a surface of area A under the holographic principle. Workers deriving recognition rates or information bounds in quantum gravity cite it when linking boundary area to ledger throughput. The definition is a direct one-line algebraic division of area by four Planck areas.

claimThe total holographic capacity in bits of a surface with area $A$ is $A/(4 ell_P^2)$, where $ell_P^2$ is the Planck area.

background

Recognition Science connects the holographic bound (maximum information proportional to boundary area over four Planck areas) to the per-bit recognition cost and the eight-tick cadence. The module defines recognition bandwidth as the maximum rate of recognition events inside a holographically bounded region, given by $R_max = S_holo / (k_R · 8 tau_0)$. Upstream, k_R is defined as the natural logarithm of phi, the fundamental cost per ledger bit, while planckArea is the square of the Planck length.

proof idea

This is a one-line definition that directly implements the holographic entropy formula by dividing the input area by four times the Planck area.

why it matters in Recognition Science

This definition supplies the numerator for the bandwidth theorems that equate bandwidth to holographic bits divided by (k_R times eight-tick cadence) and that show bandwidth times cost equals the bit count. It fills the holographic capacity step in the Recognition Bandwidth module, linking the Bekenstein-Hawking entropy formula to the per-bit cost k_R and the eight-tick octave from the forcing chain.

scope and limits

formal statement (Lean)

 115noncomputable def holographicBits (area : ℝ) : ℝ :=

proof body

Definition body.

 116  area / (4 * planckArea)
 117
 118/-- Bandwidth equals holographic bits divided by (k_R · 8τ₀). -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.