recognitionProfile_pos
plain-language theorem explainer
The lemma establishes strict positivity of the recognition profile over the closed interval from 0 to π/2. Kernel matching constructions in the Measurement domain cite this result to guarantee positive rates when building recognition paths from rotations. The term-mode proof chains an auxiliary lower bound on the cotangent expression, a lift to strict positivity, non-negativity of the square root, and a sum-positivity lemma.
Claim. For every real number $ϑ$ satisfying $0 ≤ ϑ ≤ π/2$, the recognition profile at $ϑ$ is strictly positive.
background
The module proves the pointwise kernel match J(r) dt = 2 dA drawn from Local-Collapse Appendix D. The recognition profile is the auxiliary function whose positivity is required so that rates remain positive when the profile is shifted by a rotation angle; its explicit form is 1 + 2 cot ϑ + √((1 + 2 cot ϑ)^2 − 1). The local setting is the constructive identification of the BIT kernel and ILG kernel families with the active edge count A = 1 at D = 3.
proof idea
Term-mode proof. It invokes the sibling lemma arcosh_arg_ge_one to obtain 1 ≤ 1 + 2 cot ϑ, lifts to strict positivity via lt_of_lt_of_le with zero_lt_one, records non-negativity of the square-root term by Real.sqrt_nonneg, and closes with add_pos_of_pos_of_nonneg.
why it matters
The result supplies the positivity hypothesis needed by pathFromRotation in C2ABridge, where the rate function is defined directly from the recognition profile. It therefore supports the integral identity C = 2A that closes the kernel match. Within the Recognition Science framework this step aligns the measurement construction with the eight-tick octave and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.