pathFromRotation
plain-language theorem explainer
pathFromRotation builds a RecognitionPath object from any TwoBranchRotation by fixing its period T to π/2 minus the rotation's starting angle θ_s and shifting the recognitionProfile rate function accordingly. Workers on the C=2A measurement equivalence cite this construction when converting geodesic rotations into explicit recognition paths for action calculations. The definition supplies the four fields of RecognitionPath with direct arithmetic checks on the supplied θ_s bounds.
Claim. For a two-branch rotation rot whose angle θ_s satisfies 0 ≤ θ_s ≤ π/2, define the recognition path P by T_P = π/2 - θ_s together with the rate function ϑ ↦ recognitionProfile(ϑ + θ_s) on the interval [0, T_P].
background
The module establishes the central C = 2A bridge: recognition cost C equals twice the residual-model rate action A for any two-branch geodesic rotation, showing that quantum measurement and recognition obey the same J-cost functional. RecognitionPath is the structure carrying period T, positivity witness T_pos, rate function, and rate_pos witness; TwoBranchRotation supplies θ_s together with its bounds. The rate function invokes recognitionProfile, whose positivity is supplied by an upstream lemma in the PathAction import.
proof idea
The definition is written in structure mode. T is set by the explicit expression π/2 - rot.θ_s. T_pos applies linarith to the rotation bounds. The rate field is the lambda that shifts recognitionProfile by rot.θ_s. rate_pos invokes recognitionProfile_pos, then uses linarith plus the arithmetic lemmas add_comm, add_assoc, add_left_comm and sub_eq_add_neg to verify the shifted argument stays inside the profile's domain.
why it matters
This definition supplies the concrete path object required by measurement_bridge_C_eq_2A, which proves pathAction(pathFromRotation rot) = 2 * rateAction rot and thereby discharges the main C = 2A claim. The same object is fed to amplitude_modulus_bridge, weight_bridge and weight_equals_born, which connect the recognition weight exp(-C) to Born-rule probabilities. It therefore realizes the J-uniqueness (T5) and Recognition Composition Law inside the measurement setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.