Encyclopedia Measurement Measurement Kernel Match Kernel Integral Match

ARTICLE 3 claims 2 theorems 1 model

Measurement Kernel Match Kernel Integral Match

A machine-checked theorem shows that a specific recognition profile converts a cost integral into a simple trigonometric one, but it does not by itself establish any physical measurement.

Verify this page

The kernel integral match

The declaration kernel_integral_match is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that for a certain function called the recognition profile, the integral of the recognition cost over a range of angles equals twice the integral of the cotangent function over the same range. The recognition profile is defined as r(θ) = 1 + 2 cot θ + √((1 + 2 cot θ)² − 1), and the cost function J is the framework's forced cost of recognition, J(x) = (x + 1/x)/2 − 1. The theorem holds for any starting angle θ_s between 0 and π/2, integrating from 0 to π/2 − θ_s.

This result is a pointwise identity in disguise. The framework first proves that for every angle θ in the allowed range, J(r(θ)) = 2 cot θ exactly. The integral match then follows by integrating both sides of this pointwise equality over the same interval. The theorem is constructive: it does not merely assert that the two integrals are equal, but derives the equality from the explicit form of the recognition profile and the cost function. This is the kind of result that the framework's library checks by machine, meaning every step of the proof is verified by a computer program that allows no gaps.

What the theorem does not claim is important. It does not say that the recognition profile is the only function satisfying this integral relation, nor does it say that the cotangent function has any special physical meaning on its own. The theorem is a statement about a specific mathematical construction within the framework, not about the empirical world. It does not establish that any physical measurement must follow this pattern, and it does not derive any numerical constant or coupling from the identity. The recognition profile itself is a definitional choice, not a derived quantity; the framework chooses this form because it makes the cost identity work out cleanly.

The payoff of the theorem is that it provides a bridge between the framework's abstract cost function and a concrete integral that can be evaluated. This is a step toward connecting the framework's internal mathematics to measurable quantities, but the connection is not yet complete. The framework's own documentation describes this as enabling the integral identity C = 2A, where C is a cost integral and A is an area, but the physical interpretation of that identity remains a target for further work, not an established fact.

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

What this page does not claim

The theorem does not claim that any physical measurement follows this integral pattern. The theorem does not derive any numerical constant or coupling from the identity. The recognition profile is a definitional choice, not a quantity forced by the framework's axioms.

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