pathAction
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove additivity, translation invariance, or any other functional properties of the integral.
- Does not supply an explicit closed-form expression for the Jcost integrand.
- Does not address measure-theoretic regularity conditions on the rate function beyond positivity.
Lean usage
theorem pathWeight_def (γ : RecognitionPath) : pathWeight γ = Real.exp (- pathAction γ) := by rflformal statement (Lean)
25noncomputable def pathAction (γ : RecognitionPath) : ℝ :=
proof body
Definition body.
26 ∫ t in (0)..γ.T, Cost.Jcost (γ.rate t)
27
28/-- Positive weight w[γ] = exp(-C[γ]). -/