maintenanceDemand
open lean source
IndisputableMonolith.Unification.ConsciousnessBandwidth on GitHub at line 123.
browse module
All declarations in this module, on Recognition.
plain-language theorem explainer
maintenanceDemand defines the recognition cost of sustaining a boundary of spatial extent L across the 360-tick consciousness barrier. Researchers bounding conscious extent by holographic information budget cite it when deriving viability constraints. The definition is a direct product of the barrier period and the J-cost function in RS-native units.
Claim. The maintenance demand for a boundary of extent $L$ is $360 · J(L)$, where $J$ is the J-cost function and 360 is the consciousness barrier period in ticks.
background
In the ConsciousnessBandwidth module a conscious boundary persists for the fixed barrier period of 360 ticks, obtained as 45 times the eight-tick octave. The J-cost function, imported from the Recognition module, supplies the per-unit recognition cost; Cost.Jcost is the canonical cost measure from RSNative.Core. The module sets demand equal to barrierPeriod multiplied by J(L) under the convention λ_rec = ℓ_P = 1.
proof idea
One-line definition that multiplies barrierPeriod by Cost.Jcost L, implementing the BoundaryCost formula stated in the module documentation.
why it matters
This definition supplies the core demand quantity used by IsViable to enforce the holographic viability constraint and by complexDemand to incorporate Z-complexity scaling. It fills the maintenance-demand step in the argument that bandwidth constrains conscious extent, linking directly to the eight-tick octave via the 360-tick period. It touches the open question of the maximum coherent extent L_crit.
depends on
used by
formal source
120 Uses the canonical J-cost: BoundaryCost = τ · J(L/λ_rec).
121 In RS-native units with λ_rec = ℓ_P = 1:
122 demand = 360 · J(L). -/
123noncomputable def maintenanceDemand (L : ℝ) : ℝ :=
124 barrierPeriod * Cost.Jcost L
125
126/-- Maintenance demand is nonneg for positive extent. -/
127theorem maintenanceDemand_nonneg {L : ℝ} (hL : 0 < L) :
128 0 ≤ maintenanceDemand L := by
129 unfold maintenanceDemand
130 exact mul_nonneg (le_of_lt barrierPeriod_pos) (Cost.Jcost_nonneg hL)
131
132/-- Maintenance demand is zero only when L = 1 (identity scale). -/
133theorem maintenanceDemand_zero_iff {L : ℝ} (hL : 0 < L) :
134 maintenanceDemand L = 0 ↔ L = 1 := by
135 unfold maintenanceDemand
136 constructor
137 · intro h
138 have hb := barrierPeriod_pos
139 have := (mul_eq_zero.mp h).resolve_left (ne_of_gt hb)
140 exact (Cost.Jcost_eq_zero_iff L hL).mp this
141 · intro h
142 rw [h, Cost.Jcost_unit0, mul_zero]
143
144/-! ## §5. Critical Extent -/
145
146/-- A boundary is **holographically viable** if its maintenance demand
147 does not exceed its holographic budget.
148
149 This is the bandwidth constraint on consciousness. -/
150def IsViable (L : ℝ) : Prop :=
151 maintenanceDemand L ≤ maintenanceBudget L
152
153/-- The identity scale L = 1 is always viable (zero demand). -/