pathFromRotation
Definition pathFromRotation builds a RecognitionPath from any two-branch geodesic rotation by setting the period T to π/2 minus the rotation angle θ_s and shifting the recognition profile to define the rate function. Researchers deriving the C=2A equivalence for quantum measurement would cite it when converting geodesic rotations into explicit recognition paths. The construction directly populates the RecognitionPath record and discharges positivity obligations with linarith on the supplied θ_s bounds.
claimFor a two-branch geodesic rotation with angle θ_s (0 ≤ θ_s ≤ π/2), the recognition path has period T = π/2 - θ_s and rate function ϑ ↦ recognitionProfile(ϑ + θ_s) for ϑ ∈ [0, T].
background
Recognition Science derives all physics from the unique J-cost functional obeying the Recognition Composition Law. The present module establishes the central C=2A bridge: the recognition action C along a constructed path equals twice the rate action A of the underlying two-branch geodesic rotation. RecognitionPath packages a positive period T, a positivity witness, and a rate function built from the recognition profile; TwoBranchRotation supplies the angle θ_s together with its interval bounds. Upstream structures include PhiForcingDerived.of (structure of J-cost) and LedgerFactorization.of (calibration of J on the positive reals).
proof idea
Direct record construction: T is set to π/2 - rot.θ_s and its positivity proved by linarith on the θ_s bounds; the rate is defined as recognitionProfile shifted by θ_s; rate positivity follows by applying recognitionProfile_pos after verifying the shifted interval [0, T] lies inside [0, π/2] via add_le_add_right and arithmetic simplifications.
why it matters in Recognition Science
This definition supplies the concrete path object required by measurement_bridge_C_eq_2A, which proves pathAction(pathFromRotation rot) = 2 * rateAction rot and thereby feeds amplitude_modulus_bridge, weight_bridge, weight_equals_born, and born_rule_from_C. It realizes the module claim that recognition cost C equals twice the residual-model rate action A, linking geodesic rotations directly to the J-cost functional and supporting derivation of the Born rule from the unique cost. In the framework it closes the measurement bridge between rotations and recognition paths.
scope and limits
- Does not prove the C=2A equality itself.
- Does not handle rotations outside the two-branch geodesic class.
- Does not compute numerical values for path weights or amplitudes.
- Does not extend to multi-branch or higher-dimensional cases.
Lean usage
theorem use_bridge (rot : TwoBranchRotation) : pathAction (pathFromRotation rot) = 2 * rateAction rot := by rw [measurement_bridge_C_eq_2A]formal statement (Lean)
28noncomputable def pathFromRotation (rot : TwoBranchRotation) : RecognitionPath where
29 T := π/2 - rot.θ_s
proof body
Definition body.
30 T_pos := by
31 have ⟨_, h2⟩ := rot.θ_s_bounds
32 linarith
33 rate := fun ϑ => recognitionProfile (ϑ + rot.θ_s)
34 rate_pos := by
35 intro t ht
36 apply recognitionProfile_pos
37 have ⟨h1, h2⟩ := rot.θ_s_bounds
38 constructor
39 · -- 0 ≤ t + θ_s
40 have := ht.1
41 linarith
42 · -- t + θ_s ≤ π/2
43 have ht' : t ≤ π/2 - rot.θ_s := ht.2
44 have := add_le_add_right ht' rot.θ_s
45 simpa [add_comm, add_left_comm, add_assoc, sub_eq_add_neg] using this
46
47/-- The integral of tan from θ_s to π/2 equals -ln(sin θ_s) -/