theorem proved term proof

`maintenanceDemand_zero_iff`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 133theorem maintenanceDemand_zero_iff {L : ℝ} (hL : 0 < L) :
 134    maintenanceDemand L = 0 ↔ L = 1 := by

proof body

Term-mode proof.

 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. -/

depends on (19)

Lean names referenced from this declaration's body.

Jcost_eq_zero_iff in IndisputableMonolith.Cost decl_use
Jcost_unit0 in IndisputableMonolith.Cost decl_use
Jcost_unit0 in IndisputableMonolith.Cost.JcostCore decl_use
mul_zero in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
mul_eq_zero in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
Jcost_eq_zero_iff in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
barrierPeriod_pos in IndisputableMonolith.Unification.ConsciousnessBandwidth decl_use
maintenanceDemand in IndisputableMonolith.Unification.ConsciousnessBandwidth decl_use
bandwidth in IndisputableMonolith.Unification.RecognitionBandwidth decl_use