IndisputableMonolith.Measurement.PathAction
This module defines recognition paths as time-parameterized positive rate functions and associated functionals for measurement. It is imported by BornRule, C2ABridge, KernelMatch and TwoBranchGeodesic to derive the Born rule and C=2A identities. The module supplies only definitions and basic lemmas with no theorems proved.
claimA recognition path is a function $r:ℝ→(0,∞)$. The module introduces the functionals pathAction, pathWeight and pathAmplitude together with the identities pathWeight_pos and amplitude_mod_sq_eq_weight.
background
The module sits in the Measurement domain and imports only Mathlib and IndisputableMonolith.Cost. Its single doc-comment states that a recognition path is a time-parameterized positive rate function. Sibling declarations supply the concrete objects RecognitionPath, pathAction, pathWeight, pathAmplitude and the two lemmas pathWeight_pos, amplitude_mod_sq_eq_weight.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The definitions feed directly into IndisputableMonolith.Measurement.BornRule (derives P(I)=|α_I|² from J and 𝒜=exp(-C/2)·exp(iφ)), IndisputableMonolith.Measurement.C2ABridge (proves C=2A for two-branch geodesics), IndisputableMonolith.Measurement.KernelMatch (J(r(ϑ))=2 tan ϑ pointwise) and IndisputableMonolith.Measurement.TwoBranchGeodesic (A=-ln(sin θ_s)).
scope and limits
- Does not contain any proved theorems.
- Does not import modules other than Cost and Mathlib.
- Does not introduce constants, dimensions or the forcing chain.
- Does not state or prove the Recognition Composition Law.