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

maintenanceBudget

show as:
view Lean formalization →

maintenanceBudget defines the maximum number of recognition events N_budget(L) supportable by the holographic information capacity of a boundary of extent L. Researchers deriving critical extents L_crit in the consciousness bandwidth constraint would cite this when comparing supply to J-cost demand. It is a direct one-line quotient of boundary area by four Planck areas scaled by the recognition cost per bit.

claim$N(L) = A(L) / (4 ell_P^2 k_R)$ where $A(L)$ is the boundary area for extent $L$, $ell_P^2$ is the Planck area, and $k_R = ln phi$ is the information cost of one recognition event.

background

The Consciousness Bandwidth module models a conscious boundary of spatial extent L that persists for a fixed barrier period of 360 ticks. Its holographic capacity is the boundary area divided by four Planck areas, each Planck area holding one bit. Each maintenance recognition event costs k_R = ln phi bits, so the total budget of events is the area capacity divided by k_R. This supplies the supply side of the demand-equals-budget equation that bounds viable L.

proof idea

The definition is a one-line algebraic quotient that divides boundaryArea L by the product of four times planckArea and k_R.

why it matters in Recognition Science

This supplies the holographic budget term inside the IsViable predicate and is invoked to prove identity_viable at L=1 together with maintenanceBudget_pos. It closes the supply side of the consciousness constraint argument in the module, linking the holographic bound S_holo = L^2 / (4 ell_P^2) to the recognition cost k_R and the 360-tick barrier period.

scope and limits

formal statement (Lean)

 103noncomputable def maintenanceBudget (L : ℝ) : ℝ :=

proof body

Definition body.

 104  boundaryArea L / (4 * planckArea * k_R)
 105

used by (3)

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

depends on (8)

Lean names referenced from this declaration's body.