pathFromRotation
plain-language theorem explainer
This definition constructs a recognition path from a two-branch geodesic rotation by setting terminal time to π/2 minus the starting angle θ_s and shifting the recognition profile to serve as the rate. Researchers deriving the C=2A equivalence for quantum measurement cite the construction when building the path object. Positivity of T and the rate interval on [0,T] follows from direct assignment plus linear arithmetic on the rotation's angle bounds.
Claim. Given a two-branch geodesic rotation with starting angle $θ_s$ satisfying $0 ≤ θ_s ≤ π/2$, the recognition path has terminal time $T = π/2 - θ_s$ and rate function $ϑ ↦$ recognition profile of $(ϑ + θ_s)$.
background
The module proves the central equivalence C = 2A between recognition cost and residual-model rate action for any two-branch geodesic rotation, showing that quantum measurement and recognition share the same unique cost functional J. A recognition path is defined by a terminal time T together with a positivity proof and a rate function that remains positive on the closed interval from 0 to T. Upstream arithmetic lemmas establish addition associativity and commutativity; these are invoked to rewrite interval bounds during positivity verification. Structures for J-cost calibration and ledger factorization supply the surrounding Recognition Science setting.
proof idea
The definition assigns T directly to π/2 minus the rotation's starting angle. Positivity of T is immediate from the supplied angle bounds via linarith. The rate is defined pointwise as the recognition profile shifted by the starting angle. Positivity of the rate on [0,T] applies the profile's own positivity lemma after rewriting the upper bound with add_comm, add_assoc, and simpa to align the shifted interval.
why it matters
The definition supplies the concrete path object required by the main measurement bridge theorem that equates path action to twice the rate action, and by the downstream amplitude-modulus, weight, and Born-rule bridges. It realizes the explicit construction step inside the C=2A equivalence that links the recognition cost functional J to the rate action. The result sits inside the framework's claim that the same J-cost governs both recognition paths and quantum measurement outcomes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.