Encyclopedia Measurement Measurement Kernel Match

ARTICLE 3 claims 2 theorems 1 model

Measurement Kernel Match

A single curve makes the cost of recognition equal twice an area, and the framework proves it exactly.

Verify this page

The kernel match identity

Measurement kernel match is a precise identity inside Recognition Science. The framework's central object is the cost, a function J(x) that measures the forced price of recognizing a ratio x between two quantities. The identity states that for a specially chosen profile r(θ), the cost J(r(θ)) equals 2 cot θ at every point θ in the interval from 0 to π/2. The profile is r(θ) = 1 + 2 cot θ + √((1 + 2 cot θ)² − 1). This is not an approximation or a numerical coincidence; the framework's machine-checked library of formal theorems proves the equality pointwise, for every θ in that range.

The consequence is an integral identity. Integrating both sides over any subinterval of (0, π/2) gives ∫ J(r(θ)) dθ = 2 ∫ cot θ dθ. Since the integral of cot θ is ln(sin θ), the right side is twice the logarithm of a sine, which is the area under the cotangent curve. The framework writes this as C = 2A: the accumulated cost C along the profile equals twice the area A swept by the cotangent. The module proves this integral match as a theorem, not as a heuristic. The proof chain runs from the definition of the profile, through a lemma that the square root argument is never negative, to the pointwise equality, and then to the integral version.

In Recognition Science, this match is the constructive kernel match from Local-Collapse Appendix D. It connects the abstract cost function to a geometric area, which is the kind of link the framework uses to translate between its discrete recognition ledger and continuous classical quantities. The profile r(θ) is called the recognition profile, and it is the specific curve that makes the cost match the area. The module does not claim the profile is unique, and it does not derive any physical constant from the identity. It establishes one clean equality: the cost along this curve is twice the cotangent, pointwise and in the integral.

THEOREM kernel_match_pointwise · IndisputableMonolith/Measurement/KernelMatch.lean
kernel_match_pointwise · IndisputableMonolith/Measurement/KernelMatch.lean:59 
/-- Pointwise kernel matching: J(r(ϑ)) = 2 cot ϑ
    This is the core technical lemma enabling C = 2A -/
theorem kernel_match_pointwise (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
  Jcost (recognitionProfile ϑ) = 2 * Real.cot ϑ := by
  classical
  set y := 1 + 2 * Real.cot ϑ
  set s := Real.sqrt (y ^ 2 - 1)
  have hy : 1 ≤ y := by
    simpa [y] using arcosh_arg_ge_one ϑ hϑ
  have hy_pos : 0 < y := lt_of_lt_of_le zero_lt_one hy
  have hynonneg : 0 ≤ y := le_trans (by norm_num) hy
  have hrad_nonneg : 0 ≤ y ^ 2 - 1 := by
    have hsub : 0 ≤ y - 1 := sub_nonneg.mpr hy
    have hadd : 0 ≤ y + 1 := add_nonneg hynonneg (by norm_num)
    have hx := mul_nonneg hsub hadd
    convert hx using 1 <;> ring
  have hs_sq : s ^ 2 = y ^ 2 - 1 := by
    have := Real.mul_self_sqrt hrad_nonneg
    simpa [s, pow_two] using this
  have hxmul : (y + s) * (y - s) = 1 := by
    calc
      (y + s) * (y - s) = y ^ 2 - s ^ 2 := by ring
      _ = y ^ 2 - (y ^ 2 - 1) := by simpa [pow_two, hs_sq]
      _ = 1 := by ring
  have hxpos : 0 < y + s := add_pos_of_pos_of_nonneg hy_pos (Real.sqrt_nonneg _)
  have hxinv :
      (y + s) ⁻¹ = y - s := by
    have hxnonzero : y + s ≠ 0 := ne_of_gt hxpos
    have hx' := congrArg (fun t => (y + s)⁻¹ * t) hxmul
    have hx'' : (y - s) = (y + s)⁻¹ := by
      simpa [mul_assoc, hxnonzero] using hx'
    simpa [recognitionProfile, y, s] using hx''.symm
  have hxsum : (y + s) + (y - s) = 2 * y := by ring
  have hydiv : (2 * y) / 2 = y := by
    have : (2 : ℝ) ≠ 0 := by norm_num
    simpa [mul_comm] using (mul_div_cancel' y this)
  have hy_sub : y - 1 = 2 * Real.cot ϑ := by simp [y]
  calc
    Jcost (recognitionProfile ϑ)
        = ((y + s) + (y + s)⁻¹) / 2 - 1 := by simp [Jcost, recognitionProfile, y, s]
    _ = ((y + s) + (y - s)) / 2 - 1 := by simp [hxinv]
    _ = (2 * y) / 2 - 1 := by simpa [hxsum]
    _ = y - 1 := by simpa [hydiv]
    _ = 2 * Real.cot ϑ := hy_sub
MODEL recognitionProfile · IndisputableMonolith/Measurement/KernelMatch.lean
recognitionProfile · IndisputableMonolith/Measurement/KernelMatch.lean:21 
/-- Recognition profile from eq (D.1) of Local-Collapse:
    r(ϑ) solves J(r(ϑ)) = 2 cot ϑ. -/
noncomputable def recognitionProfile (ϑ : ℝ) : ℝ :=
  1 + 2 * Real.cot ϑ + Real.sqrt ((1 + 2 * Real.cot ϑ) ^ 2 - 1)
THEOREM kernel_integral_match · IndisputableMonolith/Measurement/KernelMatch.lean
kernel_integral_match · IndisputableMonolith/Measurement/KernelMatch.lean:109 
/-- The integrand match: ∫ J(r(ϑ)) dϑ = 2 ∫ cot ϑ dϑ -/
theorem kernel_integral_match (θ_s : ℝ) (hθ : 0 < θ_s ∧ θ_s < π/2) :
  ∫ ϑ in (0)..(π/2 - θ_s), Jcost (recognitionProfile (ϑ + θ_s)) =
  2 * ∫ ϑ in (0)..(π/2 - θ_s), Real.cot (ϑ + θ_s) := by
  -- Follows by integrating the pointwise identity
  -- measurability and integrability are standard for these smooth functions
  have hb_nonneg : 0 ≤ π/2 - θ_s := sub_nonneg.mpr (le_of_lt hθ.2)
  have hpt : ∀ ϑ ∈ Set.Icc (0 : ℝ) (π/2 - θ_s),
      Jcost (recognitionProfile (ϑ + θ_s)) = 2 * Real.cot (ϑ + θ_s) := by
    intro ϑ hϑ
    apply kernel_match_pointwise (ϑ + θ_s)
    constructor
    · have hθ_nonneg : 0 ≤ θ_s := le_of_lt hθ.1
      exact add_nonneg hϑ.1 hθ_nonneg
    · have : ϑ ≤ π/2 - θ_s := hϑ.2
      have hsum := add_le_add_right this θ_s
      simpa [add_comm, add_left_comm, add_assoc] using hsum
  have h_ae :
      ∀ᵐ ϑ ∂MeasureTheory.volume,
        ϑ ∈ Set.uIoc 0 (π/2 - θ_s) →
          Jcost (recognitionProfile (ϑ + θ_s)) = 2 * Real.cot (ϑ + θ_s) := by
    refine Filter.Eventually.of_forall ?_
    intro ϑ hϑ
    have hIoc : ϑ ∈ Set.Ioc (0 : ℝ) (π/2 - θ_s) := by
      simpa [Set.uIoc, hb_nonneg] using hϑ
    have hIcc : ϑ ∈ Set.Icc (0 : ℝ) (π/2 - θ_s) := by
      exact ⟨le_of_lt hIoc.1, hIoc.2⟩
    exact hpt ϑ hIcc
  have hcongr :=
    intervalIntegral.integral_congr_ae
      (μ := MeasureTheory.volume)
      (a := 0) (b := π/2 - θ_s)
      (f := fun ϑ => Jcost (recognitionProfile (ϑ + θ_s)))
      (g := fun ϑ => 2 * Real.cot (ϑ + θ_s)) h_ae
  simpa using hcongr

What this page does not claim

The profile r(θ) is not claimed to be unique. The identity does not by itself derive any physical constant or coupling. The module does not prove that the cost function J is the only possible cost function.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Measurement/KernelMatch.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND