recognitionProfile
plain-language theorem explainer
The recognition profile r(ϑ) is the explicit algebraic function 1 + 2 cot ϑ + sqrt((1 + 2 cot ϑ)^2 - 1) that solves J(r(ϑ)) = 2 cot ϑ. Measurement theorists building the C = 2A bridge in Recognition Science cite this definition to construct rate functions for recognition paths from two-branch rotations. It is supplied as a closed-form expression that directly implements the required J-cost condition from Local-Collapse Appendix D.
Claim. The recognition profile is the function $r: [0, π/2] → ℝ$ defined by $r(ϑ) := 1 + 2 cot ϑ + √((1 + 2 cot ϑ)^2 - 1)$, which satisfies the pointwise relation $J(r(ϑ)) = 2 cot ϑ$ where $J$ is the Recognition Science cost function.
background
This definition sits in the KernelMatch module, whose module documentation states it proves the constructive kernel match from Local-Collapse Appendix D. The central identity is the pointwise relation J(r) dϑ = 2 dA, which enables the integral bridge C = 2A. The J-cost is the function J(x) = (x + x^{-1})/2 - 1 that obeys the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The profile is built to match the differential form needed for pathAction and rateAction in the measurement setting.
proof idea
This is a direct definition that supplies the closed-form algebraic solution to the equation J(r) = 2 cot ϑ. No lemmas or tactics are invoked; the expression is written explicitly as 1 + 2 cot ϑ + sqrt((1 + 2 cot ϑ)^2 - 1) to satisfy the kernel condition.
why it matters
The definition supplies the rate function used in pathFromRotation and the main C=2A Bridge Theorem measurement_bridge_C_eq_2A, where pathAction(pathFromRotation rot) = 2 * rateAction rot. It implements the key lemma from Local-Collapse eq (D.1) that feeds kernel_integral_match and kernel_match_pointwise. In the framework it connects to J-uniqueness (T5) and supports the kernel identity required for the eight-tick octave structure in measurement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.