IndisputableMonolith.Measurement.PathAction
Defines recognition paths as time-parameterized positive rate functions, together with the path action (integral of the J-cost), Boltzmann weight, and complex amplitude. Measurement theorists cite it as the shared vocabulary for Born-rule and C=2A arguments. The module is mostly definitional, with short positivity and modulus-squared identities.
claimA recognition path is a map $r: I \to \mathbb{R}_{>0}$ on a time interval. The path action is $C[r] = \int J(r(t))\,dt$ for the recognition cost $J$. The path weight is $w = e^{-C}$ and the amplitude is $\mathcal{A} = e^{-C/2} e^{i\phi}$, so $|\mathcal{A}|^2 = w$.
background
Recognition Science measures mismatch by the unique cost $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), forced by the Recognition Composition Law. Measurement modules treat a continuous positive rate $r(t)$ as the instantaneous stretch factor along a recognition trajectory.
This module packages that trajectory as a recognition path and defines the path action by integrating $J(r(t))$ in time. Exponentiating gives a positive Boltzmann weight; the amplitude bridge halves the cost in the real exponent and attaches a phase. The Cost import supplies $J$ and its elementary identities; no forcing-chain material is re-proved here.
Downstream geometry (two-branch geodesics, residual rate action $A$) will specialize these paths; the present layer stays coordinate-free and profile-agnostic.
proof idea
Definition module. It introduces the path type, the integral action, the weight $e^{-C}$, and the amplitude $e^{-C/2}e^{i\phi}$. The only nontrivial lemmas are positivity of the weight (from $J \ge 0$ and the exponential) and the identity $|\mathcal{A}|^2 = w$, which is pure complex arithmetic on the polar form. No geodesic or Born-rule argument lives here.
why it matters in Recognition Science
Shared substrate for the measurement stack. BornRule imports it to turn amplitudes into $P(I) = |\alpha_I|^2$ from $J$ and the bridge $\mathcal{A} = e^{-C/2}e^{i\phi}$. C2ABridge uses the same action to state the exact identity $C = 2A$ on two-branch geodesic rotations. KernelMatch needs the pathwise integrand to prove the pointwise kernel $J(r(\vartheta)) = 2\cot\vartheta$ that integrates to $C = 2A$. TwoBranchGeodesic specializes paths to the residual rotation geometry ($|R| = \pi/2 - \theta_s$, $A = -\ln(\sin\theta_s)$).
Without a single path-action vocabulary, those four modules would each re-encode the integral of $J$. The module sits below the Local-Collapse appendix chain rather than inside the T0–T8 forcing spine, but it is what makes the cost-to-probability bridge speakable in Lean.
scope and limits
- Does not prove Born's rule or any probability normalization.
- Does not establish C = 2A or the kernel identity J(r(θ)) = 2 cot θ.
- Does not construct two-branch geodesics or residual norms.
- Does not force J, φ, or dimension; those live in the upstream Cost and forcing chain.
- Does not specify a particular path profile; paths remain arbitrary positive rates.