pathAction
plain-language theorem explainer
Recognition action C[γ] for a path γ is the integral of J-cost of its instantaneous rate over [0, T]. Researchers deriving the Born rule or C=2A bridge in the measurement layer cite this definition when converting path costs to weights and amplitudes. The definition is introduced directly as an integral expression using Jcost on the rate function.
Claim. For a recognition path γ with duration T > 0 and rate function r(t) > 0 on [0, T], the recognition action is C[γ] := ∫ from 0 to T of J(r(t)) dt, where J denotes the J-cost function.
background
RecognitionPath is the structure carrying a positive duration T together with a rate function required to be positive on the closed interval [0, T]. Cost.Jcost is the J-cost drawn from the Quantity CostUnit abbreviation in RSNative.Core. The module supplies a minimal interface for paths, actions and weights, deliberately omitting piecewise additivity and domain-shift lemmas.
proof idea
One-line wrapper that directly expresses the action as the integral of Cost.Jcost applied to γ.rate over the interval (0)..γ.T.
why it matters
The definition supplies the recognition action C[γ] that is unfolded in pathWeight, pathAmplitude, amplitude_mod_sq_eq_weight, amplitude_modulus_bridge and measurement_bridge_C_eq_2A. It realizes the action integral that connects recognition paths to the Born rule theorem and the C=2A bridge inside the measurement domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.