higher_Z_more_demand
plain-language theorem explainer
Higher atomic number Z strictly raises complex demand for any fixed positive boundary length L not equal to 1. Researchers bounding holographic extent of conscious systems cite the monotonicity to show that greater Z-complexity forces smaller critical L. The tactic proof unfolds the demand definition, establishes positivity of the maintenance factor from J-cost non-negativity and the barrier period, then reduces the inequality via left-multiplication by that positive factor and right-multiplication by the positive recognition constant k_R.
Claim. For $0 < L$ with $L ≠ 1$ and integers $Z_1, Z_2$ satisfying $|Z_1| < |Z_2|$, the Z-dependent demand satisfies $D(L, Z_1) < D(L, Z_2)$, where $D(L, Z)$ scales the maintenance demand $M(L) = 360 · J(L/λ_rec)$ by the factor $|Z| · k_R$ and $J(x) = (x + x^{-1})/2 - 1$.
background
The Consciousness Bandwidth module imposes a holographic information budget on the maximum spatial extent of a conscious boundary. Maintenance demand over the 360-tick barrier period equals barrierPeriod times J-cost of the normalized length L, with J-cost nonnegative by the AM-GM inequality and vanishing only at L = 1. The recognition constant k_R = ln(φ) > 0 converts the bit capacity of the boundary area into the cost scale. Upstream lemmas Jcost_nonneg, Jcost_eq_zero_iff and k_R_pos supply the required positivity and zero-equivalence facts.
proof idea
Unfold complexDemand to expose the product of maintenanceDemand L and the |Z| · k_R term. Prove 0 < maintenanceDemand L by barrierPeriod_pos together with Jcost L > 0, the latter obtained from Jcost_eq_zero_iff, hL1 and Jcost_nonneg. Apply mul_lt_mul_of_pos_left to reduce to the Z-factor inequality. Cast |Z1| < |Z2| to reals, invoke mul_lt_mul_of_pos_right with k_R_pos, and close with linarith.
why it matters
The result supplies the monotonicity step underlying the module claim that higher Z reduces critical extent under the holographic budget. It sits inside the Recognition Science unification of consciousness constraints and relies on the phi-derived J-cost together with the eight-tick structure of the barrier period. No downstream uses are recorded; the theorem closes a local monotonicity obligation without touching open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.