maintenanceDemand_zero_iff
plain-language theorem explainer
Maintenance demand for positive extent L vanishes exactly at the identity scale L=1. Researchers modeling holographic bounds on conscious extent cite this to locate the zero-cost point before comparing demand against budget. The term proof unfolds the definition as barrierPeriod times Jcost L, then reduces the product via the positive barrier factor and the J-cost zero lemma.
Claim. For $L > 0$, the maintenance demand of a boundary of extent $L$ equals zero if and only if $L = 1$.
background
The Consciousness Bandwidth module treats a conscious boundary of extent L as persisting for a fixed barrier period of 360 ticks. Maintenance demand is defined as that period multiplied by the J-cost of L, where J-cost is the recognition cost function. Upstream, Jcost_eq_zero_iff states that J(x) = 0 if and only if x = 1 for x > 0, and Jcost_unit0 records the base case Jcost(1) = 0. The local setting is the holographic constraint: boundary area supplies an information budget S_holo = L² / (4 ℓ_P² ln φ) while demand integrates J-cost over the barrier ticks.
proof idea
The term proof first unfolds maintenanceDemand to expose the product with barrierPeriod. The forward direction applies mul_eq_zero, discards the positive barrierPeriod factor using barrierPeriod_pos, then invokes Jcost_eq_zero_iff. The reverse direction substitutes L = 1, replaces Jcost with zero via Jcost_unit0, and concludes with mul_zero.
why it matters
This pins the zero of maintenance demand at the identity scale, directly supporting the holographic viability definition and the critical_extent_exists result in the same module. It aligns with the J-uniqueness property (T5) of the forcing chain and supplies the baseline for bandwidth_constrains_extent. No downstream uses are recorded yet, leaving its role as a foundational lemma for later comparisons of demand against holographic budget.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.