pathWeight_pos
plain-language theorem explainer
The lemma asserts that the weight assigned to any recognition path is strictly positive. Modelers of path integrals or amplitude assignments in the Recognition Science framework cite it to ensure weights yield valid probabilities. The proof is a term-mode one-liner that unfolds the pathWeight definition and invokes the positivity of the real exponential.
Claim. For every recognition path $γ$, the weight satisfies $0 < w[γ]$, where $w[γ] := exp(-C[γ])$ and $C[γ]$ denotes the recognition action of $γ$.
background
A RecognitionPath consists of a positive duration T together with a rate function that remains positive on the closed interval [0,T]. The path weight is defined by pathWeight γ := Real.exp (- pathAction γ), so that w[γ] equals the exponential of the negative recognition action. The module supplies a minimal interface for such paths and their weights, deliberately omitting measure-theoretic lemmas to keep the build surface stable for paper exports.
proof idea
Term-mode proof. Unfold pathWeight to expose Real.exp (- pathAction γ), then apply Real.exp_pos.
why it matters
Positivity of weights is required before amplitudes can be interpreted as probability densities or before modulus-squared relations can be stated. The result therefore supports the sibling construction amplitude_mod_sq_eq_weight inside the same module. It aligns with the positive-rate requirement that appears in the RecognitionPath structure and ultimately traces back to the J-uniqueness step in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.