pith. sign in
module module high

IndisputableMonolith.Measurement.PathAction

show as:
view Lean formalization →

The PathAction module defines recognition paths as time-parameterized positive rate functions together with their action, weight, and amplitude. Researchers deriving the Born rule or the C=2A bridge from recognition cost would cite these objects. The module is purely definitional and supplies the core notation used by BornRule, C2ABridge, KernelMatch, and TwoBranchGeodesic.

claimA recognition path is a function $r(t)>0$. The path action is $A(r)=∫J(r(t))dt$, the path weight is $w(r)=e^{-A(r)}$, and the path amplitude is $α(r)=√w(r)·e^{iφ(r)}$.

background

Recognition Science measures recognition effort with the J-cost functional imported from the Cost module. This module establishes the measurement-domain setting by introducing recognition paths as positive rate functions r(t) that parameterize time evolution. The sibling definitions RecognitionPath, pathAction, pathWeight, pathAmplitude, pathWeight_pos, and amplitude_mod_sq_eq_weight supply the objects needed for the amplitude bridge 𝒜=exp(-C/2)·exp(iφ) used in downstream modules.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the foundational objects for the measurement theory. It feeds the BornRule module deriving P(I)=|α_I|² from J and the amplitude bridge, the C2ABridge proving C=2A exactly for two-branch geodesics, the KernelMatch establishing the pointwise identity J(r(ϑ))dt=2dA, and the TwoBranchGeodesic formalizing residual norm and rate action A=-ln(sin θ_s). It fills the definitional step preceding the Local-Collapse appendix results.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)