complexDemand_ge
plain-language theorem explainer
The inequality shows that for positive boundary extent L and any integer complexity Z the base maintenance demand is bounded above by the Z-adjusted complex demand. Researchers modeling holographic limits on conscious extent cite this to tighten the maximum coherent L when internal complexity rises. The tactic proof unfolds complexDemand, verifies the factor 1 + |Z| k_R exceeds one via k_R positivity, and applies left-multiplication monotonicity.
Claim. For $L > 0$ and $Z$ any integer, let $D(L)$ be the simple maintenance demand for a boundary of extent $L$ and let $D_Z(L)$ be the demand that includes the extra recognition cost from complexity $Z$. Then $D(L) ≤ D_Z(L)$.
background
The module treats consciousness as a holographic information budget. A boundary of extent L persists for the 360-tick barrier period and incurs maintenance demand proportional to the J-cost integrated over that interval. The available budget is the holographic entropy of the boundary area divided by k_R = ln(φ), the per-event recognition cost. The theorem compares the base demand to the version that multiplies by an extra factor 1 + |Z| k_R, where Z is the integer anchor complexity appearing in the mass formula. Upstream results supply the definition k_R := ln(φ) together with its positivity theorem k_R_pos.
proof idea
The proof unfolds the definition of complexDemand. It obtains nonnegativity of maintenanceDemand from the hypothesis 0 < L. It then proves 1 ≤ 1 + |Z| k_R by nonnegativity of |Z| k_R (using k_R_pos and mul_nonneg) followed by linarith. Finally it rewrites maintenanceDemand L as maintenanceDemand L · 1 via mul_one and applies mul_le_mul_of_nonneg_left to obtain the desired inequality.
why it matters
The result supports the module claim that higher Z-complexity reduces critical extent L_crit, because larger demand for fixed holographic budget forces smaller L. It forms part of the Recognition Science argument that conscious extent is limited by the recognition cost k_R and the phi-based constants. No downstream uses appear yet, but the declaration closes the z_complexity_reduces_extent step in the holographic-constraint chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.