theorem proved term proof

`superposition_justified`

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

formal statement (Lean)

 123theorem superposition_justified : SuperpositionJustification where
 124  quadratic_regime := Jcost_one_plus_exact

proof body

Term-mode proof.

 125  gradient_additivity := gradient_superposition
 126  coherence_defect_additivity := coherence_defect_of_combined
 127
 128end IndisputableMonolith.Gravity.WeakFieldSuperposition

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

forcing_chain_complete in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
full_levitation_cert in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
levitation_unconditional in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use

depends on (4)

Lean names referenced from this declaration's body.

Jcost_one_plus_exact in IndisputableMonolith.Gravity.EnergyProcessingBridge decl_use
coherence_defect_of_combined in IndisputableMonolith.Gravity.WeakFieldSuperposition decl_use
gradient_superposition in IndisputableMonolith.Gravity.WeakFieldSuperposition decl_use
SuperpositionJustification in IndisputableMonolith.Gravity.WeakFieldSuperposition decl_use