maintenanceDemand_nonneg
plain-language theorem explainer
Maintenance demand for a conscious boundary of positive extent L is shown to be nonnegative. Researchers deriving holographic bounds on conscious scale cite it to ensure demand stays below information budget. The proof is a term-mode reduction that multiplies the positive barrier period by the nonnegative J-cost.
Claim. Let $L > 0$. The maintenance demand of a boundary of extent $L$ satisfies $0$ ≤ maintenance demand of $L$.
background
The Consciousness Bandwidth module sets a holographic limit on conscious extent. A boundary of extent L persists for the 360-tick barrier period whose maintenance cost is the product of that period and the J-cost of the scaled extent. The J-cost function is nonnegative for positive arguments by the AM-GM inequality, as stated in the upstream Cost.Jcost_nonneg lemma: J(x) ≥ 0 for positive x (AM-GM inequality).
proof idea
The term proof unfolds the definition of maintenance demand then applies mul_nonneg to the result of le_of_lt barrierPeriod_pos and the Jcost_nonneg lemma at hypothesis hL.
why it matters
This nonnegativity is invoked inside complexDemand_ge to show complex demand is at least simple maintenance demand for any integer Z. It supplies the required sign step when comparing demand against the holographic budget L² / (4ℓ_P²) and thereby supports the existence of a critical coherent extent within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.