RecognitionPath
plain-language theorem explainer
The structure defines a positive duration equipped with a strictly positive rate function on the closed interval from zero to T. Physicists constructing path integrals within Recognition Science cite this when building amplitudes from rate profiles. It is introduced as a direct structure declaration encoding the required positivity constraints.
Claim. A recognition path consists of a duration $T > 0$ and a rate function $r : [0,T] → ℝ$ such that $r(t) > 0$ whenever $t ∈ [0,T]$.
background
This module supplies a lightweight interface for recognition paths and the actions and weights derived from them, deliberately avoiding detailed measure-theoretic results to preserve build stability. The structure captures a time-parameterized positive rate function, which enters the action integral through the J-cost function imported from the Cost module. The module depends on period definitions from Breath1024 and triangular numbers from Gap45.SyncMinimization to support consistent timing conventions across the framework.
proof idea
The declaration is a direct structure definition that bundles the duration field, its positivity proof, the rate function, and the interval positivity condition.
why it matters
The structure provides the domain type for the path action definition, which integrates J-cost along the path to obtain the recognition action C[γ]. This action determines the weight as the exponential of the negative action and the amplitude as the product of the exponential of half the negative action with the phase factor exp(iφ), which appear in downstream results such as the modulus squared equality and the construction from rotation. The structure supports the path-based formulation of recognition processes that connects to the J-uniqueness and composition law in the broader forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.