lemma proved term proof

`pathWeight_pos`

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

formal statement (Lean)

  37lemma pathWeight_pos (γ : RecognitionPath) : 0 < pathWeight γ := by

Term-mode proof.

  38  unfold pathWeight
  39  exact Real.exp_pos _
  40
  41/-- Amplitude modulus squared equals weight. -/

Lean names referenced from this declaration's body.

modulus in IndisputableMonolith.Foundation.ModularLogicRealization decl_use
pathWeight in IndisputableMonolith.Measurement.PathAction decl_use
RecognitionPath in IndisputableMonolith.Measurement.PathAction decl_use
Amplitude in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use