PathWeight
PathWeight defines the exponential weight of a configuration path as the real exponential of the negative total J-cost accumulated along that path. Researchers deriving the Born rule from action costs in Recognition Science modal actualization would cite this definition when normalizing path probabilities. The definition is a direct one-line wrapper applying the exponential to the output of PathAction.
claimFor a path of configurations, the path weight is $W[γ] = exp(-C[γ])$, where $C[γ]$ is the total J-cost accumulated along the path.
background
In the Modal.Actualization module, paths are lists of Config structures imported from Gravity.ILG, each carrying a value and position. PathAction computes the accumulated cost as the sum of J on each configuration value plus J_transition terms between consecutive positions. This rests on the J-function from the forcing chain (T5 J-uniqueness) and upstream results such as collision-free empirical programs and edge lengths from simplicial ledgers.
proof idea
This is a one-line wrapper that applies the real exponential function to the negation of PathAction path.
why it matters in Recognition Science
PathWeight supplies the weights that feed directly into the BornRule structure and its normalization theorem, where path probabilities emerge as normalized weights rather than being postulated. It realizes the doc-comment claim that this quantity gives rise to the Born rule from the cost structure. In the Recognition framework it connects J-cost accumulation to probabilistic actualization, supporting the transition from the eight-tick octave to modal geometry.
scope and limits
- Does not specify the explicit form of J_transition between configurations.
- Does not prove positivity or normalization of the resulting weights.
- Does not incorporate phase differences for interference effects.
- Does not handle empty paths beyond the base case in PathAction.
formal statement (Lean)
144noncomputable def PathWeight (path : List Config) : ℝ :=
proof body
Definition body.
145 Real.exp (-PathAction path)
146
147/-- Path weight is always positive. -/