boundaryArea_monotone
plain-language theorem explainer
The monotonicity of the boundary area function with linear extent follows from quadratic scaling of holographic capacity under positive prefactors. Researchers deriving critical extents for conscious boundaries in Recognition Science would cite this to confirm that available maintenance events grow with L. The proof is a short tactic sequence that unfolds the definition and applies monotonicity of squaring on positive reals together with nonnegativity of the constant multiplier.
Claim. Let $L_1, L_2 > 0$ be real numbers satisfying $L_1 ≤ L_2$. Then the boundary area function obeys boundaryArea$(L_1) ≤$ boundaryArea$(L_2)$, where boundaryArea$(L)$ measures the holographic capacity proportional to $L^2$ (scaled by factors including $π$ and Planck length).
background
The module treats a conscious boundary as a holographic surface whose information budget is limited by area. Boundary cost is $τ · J(L / λ_rec)$ while holographic capacity is $S_{holo} = L^2 / (4 ℓ_P^2)$. The function boundaryArea extracts the geometric contribution to this capacity; the maximum event count is then boundaryArea$(L)$ divided by $4 ℓ_P^2 · k_R$. Here $k_R = ln(φ)$ is the RS Boltzmann analog (positive by $φ > 1$). Upstream structures supply the $J$-cost definition and the ledger factorization that calibrate recognition events to ledger bits.
proof idea
The proof unfolds boundaryArea, then invokes mul_le_mul_of_nonneg_left. The left factor is the squared-length inequality obtained from sq_le_sq' (valid because $L_1 ≤ L_2$ and $L_1 > 0$). The right factor is shown nonnegative by mul_nonneg applied to a linarith-derived bound and the positivity of $π$.
why it matters
This monotonicity is required to compare maintenance budgets across different boundary sizes inside the holographic constraint argument. It supports the downstream claim that bandwidth constrains extent: larger $L$ increases both available events (via area) and demand (via $J$-cost). The result sits inside the derivation of critical extent and the 360-tick barrier period, linking the phi-ladder and eight-tick octave to the information bound on conscious extent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.