Measurement Path Action Path Weight Pos

Positive weight

A recognition path is a time-parameterized positive rate function, a mathematical way to describe how a recognition process unfolds over time. Each path carries a cost, called its action, computed by integrating the cost function J over the path's duration. The weight of a path is then defined as the exponential of the negative of that action: w[γ] = exp(-C[γ]).

Because the action C[γ] is a real number, and the exponential of any real number is strictly greater than zero, the weight is always positive. This is the content of the lemma pathWeight_pos: for any recognition path γ, the weight w[γ] satisfies 0 < w[γ]. The proof is immediate from the definition and the known positivity of the real exponential function.

This positivity is not a deep physical law but a structural guarantee. It ensures that weights behave like probabilities or statistical weights in later constructions: they can be added, compared, and used to define expectations without ever encountering a zero or negative weight that would break normalization. The same interface also defines an amplitude bridge, a complex number whose modulus squared equals the weight, which connects this path-weight picture to quantum-style probability amplitudes.

In Recognition Science, this declaration is part of a minimal interface for recognition paths. The framework deliberately omits heavier measure-theoretic lemmas, such as piecewise additivity or domain shifts, to keep the build surface stable for paper exports. What pathWeight_pos establishes is the basic positivity fact; it does not claim that weights sum to one, that they are normalized, or that they define a probability measure over paths.

What this means for the reader is simple: whenever a recognition path is considered, its weight is a well-defined positive real number. This is the foundation on which later probabilistic and amplitude-based reasoning can be built, without needing to check for edge cases where a weight might vanish or go negative.

/-- Weight is positive. -/
lemma pathWeight_pos (γ : RecognitionPath) : 0 < pathWeight γ := by
  unfold pathWeight
  exact Real.exp_pos _

/-- Positive weight w[γ] = exp(-C[γ]). -/
noncomputable def pathWeight (γ : RecognitionPath) : ℝ :=
  Real.exp (- pathAction γ)

/-- Amplitude modulus squared equals weight. -/
theorem amplitude_mod_sq_eq_weight (γ : RecognitionPath) (φ : ℝ) :
  ‖pathAmplitude γ φ‖ ^ 2 = pathWeight γ := by
  unfold pathAmplitude pathWeight
  have h1 : ‖Complex.exp (-(pathAction γ) / 2)‖ = Real.exp (-(pathAction γ) / 2) := by
    simpa using Complex.norm_exp_ofReal (-(pathAction γ) / 2)
  have h2 := Complex.norm_exp_ofReal_mul_I φ
  rw [norm_mul]
  simp only [h1, h2, mul_one, sq]
  rw [← Real.exp_add]
  ring

What this page does not claim

Weights are not claimed to be normalized or to sum to one over any collection of paths. The lemma does not claim that recognition paths form a probability space or that weights define a probability measure. No claim is made about the physical interpretation of the action beyond its definition as an integral of the cost function.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Measurement/PathAction.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: