def definition def or abbrev

`pathWeight`

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

formal statement (Lean)

  29noncomputable def pathWeight (γ : RecognitionPath) : ℝ :=

Definition body.

  30  Real.exp (- pathAction γ)
  31
  32/-- Amplitude bridge 𝒜[γ] = exp(-C[γ]/2) · exp(i φ). -/

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

born_rule_from_C in IndisputableMonolith.Measurement.BornRule decl_use
weight_bridge in IndisputableMonolith.Measurement.C2ABridge decl_use
weight_equals_born in IndisputableMonolith.Measurement.C2ABridge decl_use
amplitude_mod_sq_eq_weight in IndisputableMonolith.Measurement.PathAction decl_use
pathWeight_pos in IndisputableMonolith.Measurement.PathAction decl_use

Lean names referenced from this declaration's body.

bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
pathAction in IndisputableMonolith.Measurement.PathAction decl_use
RecognitionPath in IndisputableMonolith.Measurement.PathAction decl_use
Amplitude in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use