PathAction
plain-language theorem explainer
PathAction defines the total recognition cost C[γ] accumulated along a sequence of configurations by summing J at each site plus the transition costs between consecutive ones. Modal physicists building the path-integral form of the Born rule in Recognition Science cite this definition when constructing exponential path weights. The definition is supplied by recursion on the list structure, returning zero for the empty path, J of the value for a singleton, and the head J plus transition plus tail recursion otherwise.
Claim. For a path γ consisting of configurations c_i, the path action is C[γ] = Σ_i J(c_i.value) + Σ_i J_transition(c_i.value, c_{i+1}.value, c_i.pos, c_{i+1}.pos), where J is the recognition cost function and J_transition(x, y, p_x, p_y) = |ln(y/x)| · (J(x) + J(y))/2.
background
In the Modal.Actualization module, a Config is a structure holding a positive real value (generalizing bond multipliers) together with a positivity proof and a time coordinate in ticks; this supplies a simplified point in recognition state space for modal development. The J-cost measures recognition expense at a given value, while J_transition from the Possibility module computes the direct transition cost as |log(y/x)| times the average of the two J values, using the supplied positivity proofs as arguments.
proof idea
The definition is given by pattern matching on the input list. The empty-list case returns 0. The singleton case returns J of the configuration value. The cons case adds J at the first element, calls J_transition on the first two values together with their positivity proofs, and recurses on the tail list.
why it matters
PathAction supplies the cost functional whose negative exponential yields PathWeight, the quantity that produces the Born rule upon summation over paths. It sits inside the Actualization module and feeds the selection operator that picks minimal-J outcomes from the space of possibilities. In the Recognition Science framework this supplies the direct analogue of the classical action, consistent with J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.