pathAction
plain-language theorem explainer
The pathAction definition assigns to each recognition path γ the real number obtained by integrating the J-cost of its instantaneous rate over the interval [0, T]. Researchers deriving the Born rule or the C=2A amplitude bridge cite this as the explicit recognition action functional. The definition is a direct integral expression using the Jcost operator supplied by the Cost module.
Claim. For a recognition path γ with duration T > 0 and positive rate function r(t), the recognition action is defined by C[γ] := ∫ from 0 to T of J(r(t)) dt, where J denotes the J-cost function.
background
A recognition path is formalized as a structure carrying a positive duration T, a rate function r: ℝ → ℝ that remains strictly positive on the closed interval [0, T], and the corresponding positivity proof. The module supplies a minimal interface for paths and their derived quantities while deliberately omitting measure-theoretic lemmas on additivity or domain shifts. Upstream, the Cost abbreviation supplies the Quantity CostUnit wrapper whose Jcost component is the integrand; the T abbreviation from Breath1024 supplies the fundamental period convention used for the integration limits.
proof idea
This is a one-line definition that directly expresses the action as the Lebesgue integral of Jcost(γ.rate t) over the interval (0, γ.T).
why it matters
The definition supplies the action functional C[γ] that is unfolded in every downstream weight and amplitude construction. It is invoked by born_rule_from_C to obtain probabilities from squared amplitudes, by amplitude_modulus_bridge to equate modulus with exp(-C/2), and by measurement_bridge_C_eq_2A to equate path action with twice the rate action. In the Recognition framework it realizes the integral form of the recognition action that links the J-uniqueness fixed point to the measurement postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.