Encyclopedia Measurement Measurement Kernel Match Kernel Match Pointwise

ARTICLE 3 claims 2 theorems 1 model

Measurement Kernel Match Kernel Match Pointwise

A formal proof shows that one recognition profile makes the framework's cost exactly equal to twice the cotangent, a bridge between discrete cost and continuous area.

Verify this page

The pointwise match

The cotangent function, written cot θ, is the ratio of cosine to sine: cot θ = cos θ / sin θ. It appears throughout geometry and trigonometry, for example in the slopes of lines and in integral tables. The statement here is a pointwise identity: for every angle θ in the closed interval from 0 to π/2 (a right angle), a certain profile r(θ) satisfies J(r(θ)) = 2 cot θ. The profile is r(θ) = 1 + 2 cot θ + √((1 + 2 cot θ)² − 1). The identity holds at each θ separately, hence the word pointwise.

In Recognition Science, a framework that derives structure from a forced cost of recognition, the function J is the unique cost function forced by five plain conditions. The recognition profile r(θ) is a specific choice of scale ratio parameterized by angle. The theorem kernel_match_pointwise, proved in the framework's machine-checked library of formal theorems, establishes exactly this: plugging the profile into the cost yields twice the cotangent, for every angle in the stated range. A companion theorem extends the identity to integrals, so the area under the cost curve equals twice the area under the cotangent curve over the same interval.

What does this change? It gives a constructive bridge between a discrete ledger of recognition events and a continuous geometric quantity. The identity is a technical lemma, not a standalone physical law; its role is to enable the integral identity that connects cost to area in the framework's derivation. The proof is machine-checked, meaning the logical steps are verified by a computer, so the identity itself is not in question.

What it does not claim: the theorem does not assign physical meaning to θ or to the area; that interpretation is a separate modeling step. It does not prove that the profile is unique, nor that the identity holds outside the stated angle range. It says nothing about measured values or empirical data; it is a purely mathematical statement within the framework.

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 theorem does not assign physical meaning to the angle or the area. The theorem does not prove the profile is unique. The theorem does not make any empirical or measured-value claim.

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