PathWeight
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.