maintenanceBudget_pos
plain-language theorem explainer
maintenanceBudget_pos establishes that the holographic maintenance budget for any positive boundary extent L is strictly positive. Researchers deriving maximum coherent conscious extents from demand-budget balance in Recognition Science cite it to confirm the budget side is well-defined. The proof is a term-mode positivity argument that unfolds the definition and chains div_pos with mul_pos applications on boundaryArea_pos, planckArea_pos, and k_R_pos.
Claim. For every real number $L > 0$, the maintenance budget $B(L)$, defined as the ratio of boundary area to the product of Planck area squared and the recognition constant $k_R = ln(φ)$, satisfies $B(L) > 0$.
background
The ConsciousnessBandwidth module models the holographic constraint on conscious extent. A boundary of extent L has area supplied by boundaryArea, whose positivity for L > 0 follows from separate results. The maintenance budget is this area divided by the product of two Planck areas and the recognition constant k_R. Upstream, k_R_pos proves k_R > 0 by Real.log_pos applied to Constants.one_lt_phi, while planckArea_pos comes from Planck scale definitions in the imported constants.
proof idea
The proof is a term-mode positivity argument. It unfolds maintenanceBudget to expose a division, applies div_pos to boundaryArea_pos hL, and builds denominator positivity via two nested mul_pos calls: the inner combines planckArea_pos with itself, the outer combines the result with k_R_pos. A linarith tactic discharges one planckArea_pos instance.
why it matters
This result is invoked by the downstream theorem identity_viable to show that the identity scale L = 1 is viable, since demand vanishes while budget stays positive. It completes the budget-positivity step required for the module's derivation of critical extent L_crit by equating demand 360 · J(L) to the holographic budget. In the Recognition Science framework it anchors the information budget S_holo / k_R against J-cost demand, consistent with the 360-tick consciousness barrier arising from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.