Measurement Kernel Match Recognition Profile Pos

The positive profile

The declaration recognitionProfile_pos is a formal lemma about a particular mathematical function, the recognition profile r(θ) = 1 + 2 cot θ + √((1 + 2 cot θ)² − 1). The lemma states that for any angle θ between 0 and π/2, this expression is strictly greater than zero. In plain terms, the profile never dips to zero or below within that range; it remains positive throughout. The proof is short: it shows the first part, 1 + 2 cot θ, is at least 1, and the square root term is always nonnegative, so their sum must be positive.

This positivity fact matters because of what the profile is used for. The framework's cost function J(x) = (x + 1/x)/2 − 1, which measures the forced cost of recognition, is only defined in a meaningful way for positive inputs. The profile is constructed so that applying J to it yields exactly 2 cot θ, a clean trigonometric identity. That identity, in turn, powers an integral matching result: the integral of J along the profile equals twice the integral of cot θ, written as C = 2A. Without the positivity lemma, the chain would break at the first step, since J would not be well-behaved on the profile's values.

In Recognition Science, this is one link in a longer forcing chain. The framework models reality as maintaining a discrete record of recognition events, with a forced cost J. From J, theorems derive the golden ratio, an eight-tick cycle, and three spatial dimensions. The positivity lemma here is a supporting result: it guarantees that a specific curve used in a matching argument stays within the domain where J behaves properly. It is not itself a grand claim about physics, but a technical guarantee that makes a later integral identity valid.

What the lemma does not claim is just as important. It does not say the profile is positive everywhere, only on the interval from 0 to π/2. It does not assert that the profile has any physical meaning on its own; that interpretation comes from the broader framework, not from this proof. And it does not establish the integral identity C = 2A by itself; that requires the additional kernel matching theorems that build on this positivity result. The lemma is a necessary condition for those later steps, not a sufficient one.

/-- Recognition profile is positive -/
lemma recognitionProfile_pos (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
  0 < recognitionProfile ϑ := by
  have hy : 1 ≤ 1 + 2 * Real.cot ϑ := arcosh_arg_ge_one ϑ hϑ
  have hypos : 0 < 1 + 2 * Real.cot ϑ := lt_of_lt_of_le zero_lt_one hy
  have hs : 0 ≤ Real.sqrt ((1 + 2 * Real.cot ϑ) ^ 2 - 1) := Real.sqrt_nonneg _
  exact add_pos_of_pos_of_nonneg hypos hs

/-- 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 lemma does not prove the profile is positive outside the interval [0, π/2]. It does not by itself establish the integral identity C = 2A; that requires the additional kernel matching theorems. It does not assign physical meaning to the profile; that interpretation comes from the framework's broader modeling choices.

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: