integral_cot_from_theta
plain-language theorem explainer
The definite integral of cot θ from θ_s to π/2 equals -log(sin θ_s) when 0 < θ_s < π/2. Researchers deriving the C=2A equivalence for two-branch geodesic paths in recognition models cite this evaluation when computing path actions. The proof applies the fundamental theorem of calculus to f(θ) = log(sin θ) after verifying the derivative identity, differentiability, and interval integrability via chain rule and positivity of sine.
Claim. For $0 < θ_s < π/2$, $∫_{θ_s}^{π/2} cot θ dθ = -log(sin θ_s)$.
background
The C=2A Measurement Bridge module establishes that recognition cost C equals twice the rate action A for any two-branch geodesic rotation, showing that quantum measurement and recognition share the same cost functional J. This integral supplies the explicit antiderivative evaluation needed inside the pathAction computation. Upstream results include the composition operation on J-automorphisms from CostAlgebra and the active edge count A per fundamental tick from IntegrationGap, which together anchor the φ-power balance at D=3.
proof idea
Define f(θ) := log(sin θ). Establish that deriv f equals cot on the open interval via HasDerivAt for log and sin composed by the chain rule, then confirm sin x ≠ 0 and positivity to obtain differentiability on the closed interval. Prove continuity of cot, deduce interval integrability, apply intervalIntegral.integral_deriv_eq_sub to obtain f(π/2) - f(θ_s), and use congruence to replace the derivative integrand with cot.
why it matters
This result is invoked by the parent theorem measurement_bridge_C_eq_2A, which asserts pathAction(pathFromRotation rot) = 2 * rateAction rot and thereby equates C with 2A. It closes the explicit integral step required to link the recognition cost functional to the rate action in the forcing chain (T5 J-uniqueness through T8 D=3). The lemma touches no open scaffolding but supplies a deterministic calculus fact inside the Recognition Composition Law setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.