path_weight_pos
plain-language theorem explainer
Path weight positivity follows directly from the exponential definition in the Modal.Actualization setting. Researchers formalizing the emergence of quantum probabilities from classical costs in Recognition Science cite this when verifying that all paths contribute positively to interference sums. The proof is a one-line term that invokes the positivity of the real exponential on the negated path action.
Claim. Let $γ$ be any finite list of configurations. Define the path weight by $W[γ] = exp(-C[γ])$, where $C[γ]$ denotes the path action. Then $W[γ] > 0$.
background
The Actualization module treats configurations as states that can be actualized along paths. PathWeight is the exponential map applied to the negative of the accumulated PathAction, ensuring positivity as a foundation for probability interpretations. This relies on cost functions from upstream modules such as ObserverForcing.cost, which assigns non-negative J-costs to recognition events, and MultiplicativeRecognizerL4.cost for derived costs on ratios. A parallel result exists in Foundation.PathIntegralDeep.path_weight_pos, which proves positivity for parameterized path weights using the same exponential argument. The module context emphasizes that this positivity allows the Born rule to emerge without postulate, as the normalized weights P[γ] = W[γ] / sum W[γ'] arise naturally from the cost structure.
proof idea
The proof applies the lemma Real.exp_pos directly to the expression for PathWeight path, which is Real.exp (-PathAction path). This term-mode proof requires no further tactics or case analysis because the exponential is positive for every real number.
why it matters
This result is a prerequisite for the PathIntegralDeepCert structure in Foundation.PathIntegralDeep, which bundles positivity, maximality at unit ratio, and normalization at equality. It directly supports the Born rule emergence comment in the module, where probabilities are proportional to weights without being postulated. In the broader framework, it aligns with the eight-tick octave and D=3 dimensions by ensuring consistent weighting in the phi-ladder mass formulas and recognition events. It is also invoked in Modal.ModalGeometry.constructive_at_zero to establish constructive interference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.