theorem proved term proof

`quadratic1D_zero_valid`

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

formal statement (Lean)

  67theorem quadratic1D_zero_valid : quadratic1DStrainLedger.isValid 0 :=

proof body

Term-mode proof.

  68  ⟨quadratic1D_equilibrium, quadratic1D_ledger_closed 0⟩
  69
  70/-! ## Quadratic Octave -/
  71
  72/-- Observation channel: identity observation, quality = strain. -/

depends on (7)

Lean names referenced from this declaration's body.

identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
Octave in IndisputableMonolith.RRF.Core.Octave decl_use
isValid in IndisputableMonolith.RRF.Core.Strain decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use
quadratic1D_equilibrium in IndisputableMonolith.RRF.Models.Quadratic decl_use
quadratic1D_ledger_closed in IndisputableMonolith.RRF.Models.Quadratic decl_use
quadratic1DStrainLedger in IndisputableMonolith.RRF.Models.Quadratic decl_use