Measurement Kernel Match Kernel Match Differential

The kernel match identity

The declaration kernel_match_differential belongs to Recognition Science, a framework that begins with the idea that reality keeps a ledger, a discrete record of recognition events, and that the cost of each recognition is forced by a proved law. The framework's central cost function is J(x) = (x + 1/x)/2 - 1, a fixed shape that any valid recognition cost must take. The declaration in question proves a pointwise identity: when the recognition profile r(θ) is set to 1 + 2 cot θ + √((1 + 2 cot θ)² - 1), then J(r(θ)) equals 2 cot θ exactly, for every angle θ in the closed interval from 0 to π/2.

This identity matters because it connects two different measurements of the same thing. The left side, J(r(θ)), is the cost of a recognition event as a function of the profile. The right side, 2 cot θ, is twice the cotangent of the angle, a quantity that integrates to twice the area under a curve. The theorem kernel_match_differential states this equality as a formal result in the framework's machine-checked library of formal theorems, and a companion theorem kernel_integral_match extends it to integrals: the integral of J(r(θ)) over an interval equals twice the integral of cot θ over the same interval. In plain terms, the cost accumulated over a sweep of angles equals twice the area swept out, a bridge between the ledger's cost accounting and ordinary geometry.

The proof is constructive. The recognition profile is defined explicitly, and the theorem kernel_match_pointwise verifies the identity by direct computation. The framework's library checks the positivity of the profile and the domain condition on the angle, so the result holds for all θ in [0, π/2], not just for a few sample points. This is a fully formal result: the equality is derived from the definitions and the proved properties of the cost function, with no unstated assumptions about the angle or the profile.

What the declaration does not claim is just as important. It does not assert that the recognition profile is the only possible one, nor that the identity holds outside the stated angle range. It does not say anything about what the area A physically represents, or why the constant 2 appears rather than some other factor. The theorem is a precise, narrow bridge: it equates two expressions under a specific profile and a specific domain. It leaves open the question of whether this profile is forced by deeper principles, and it does not by itself establish any empirical prediction about the physical world.

The payoff is a clean example of how the framework's cost function connects to classical geometry. A stranger can see that the ledger's cost, a quantity defined by a functional equation, coincides with a simple trigonometric expression under a chosen profile. That coincidence is not an accident; it is proved. But the proof does not explain why the profile takes this form, and it does not claim that the identity is universal. It is one verified link in a larger chain, useful precisely because its scope is explicit.

/-- Differential form of kernel match: J(r) dϑ = 2 cot ϑ dϑ -/
theorem kernel_match_differential (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
  Jcost (recognitionProfile ϑ) = 2 * Real.cot ϑ :=
  kernel_match_pointwise ϑ hϑ

/-- 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

/-- 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

What this page does not claim

The recognition profile is not claimed to be unique or forced by the framework's axioms. The identity is not claimed to hold for angles outside the closed interval [0, π/2]. The constant 2 in the identity is not claimed to have a physical meaning beyond its algebraic role.

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: