pith. sign in
module module high

IndisputableMonolith.Measurement.PathAction

show as:
view Lean formalization →

Recognition paths are formalized here as time-parameterized positive rate functions together with associated action, weight, and amplitude maps. Measurement modules deriving Born's rule and the C=2A bridge import these objects to connect the J-cost to amplitudes. The module is definitional only, importing the Cost primitives and exposing RecognitionPath plus pathAction, pathWeight, and pathAmplitude.

claimA recognition path is a map $r:ℝ→ℝ_{>0}$. The path action is the functional $A[r]=∫J(r(t))dt$, the path weight is $w[r]=exp(-A[r])$, and the path amplitude is $α[r]=√w[r]·exp(iφ[r])$.

background

The module sits in the Measurement domain and imports only the Cost module, which supplies the J-cost functional. RecognitionPath is introduced exactly as a time-parameterized positive rate function. Sibling definitions pathAction, pathWeight, pathAmplitude, pathWeight_pos, and amplitude_mod_sq_eq_weight then equip each such path with its integrated cost, exponential weight, and complex amplitude.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions feed four downstream modules. BornRule uses them to derive P(I)=|α_I|² from J and the bridge 𝒜=exp(-C/2)·exp(iφ). C2ABridge relies on them for the exact equivalence C=2A on two-branch geodesics. KernelMatch uses them for the pointwise identity J(r(ϑ))=2 tan ϑ. TwoBranchGeodesic uses them for the residual-norm and rate-action formulas.

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)