arcosh_arg_ge_one
plain-language theorem explainer
This lemma shows that 1 + 2 cot ϑ is at least 1 for every real angle ϑ in the closed interval [0, π/2]. Researchers constructing the recognition profile inside the kernel matching module cite it to guarantee that the square root in the profile definition stays real. The tactic proof first verifies non-negativity of sine and cosine via interval membership, rewrites cotangent as their ratio, and concludes by adding a non-negative term to 1.
Claim. For every real number $ϑ$ satisfying $0 ≤ ϑ ≤ π/2$, one has $1 ≤ 1 + 2 cot ϑ$.
background
The KernelMatch module proves the constructive pointwise identity between the J-cost of the recognition profile and twice the cotangent, realizing the kernel match J(r) dt = 2 dA from Local-Collapse Appendix D. The recognition profile is given by r(ϑ) = (1 + 2 tan ϑ) + √((1 + 2 tan ϑ)^2 − 1); the present lemma ensures the inner expression 1 + 2 cot ϑ is at least 1 so that the square root is defined over the reals and the profile remains positive.
proof idea
The tactic proof first builds membership of ϑ in [0, π] by applying le_trans to chain the given bound ϑ ≤ π/2 with π/2 ≤ π, then invokes sin_nonneg_of_mem_Icc. It repeats the construction for membership in [-π/2, π/2] to obtain cos ϑ ≥ 0. Cotangent is rewritten via cot_eq_cos_div_sin and shown non-negative by div_nonneg; multiplication by 2 and addition of 1 finish the argument with add_le_add_left.
why it matters
The lemma is invoked directly by kernel_match_pointwise, which states Jcost(recognitionProfile ϑ) = 2 cot ϑ and thereby enables the integral identity C = 2A. It also feeds recognitionProfile_pos. In the Recognition Science framework it supplies the real-analysis step required for the measurement kernel that connects J-uniqueness (T5) to the spatial forcing chain (T8), closing a technical prerequisite without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.