Encyclopedia Cpm Cpm Law Of Existence Cproj From J Second Deriv

ARTICLE 4 claims 3 theorems 1 model

Cpm Law Of Existence Cproj From J Second Deriv

A machine-checked theorem ties the second derivative of a cost function at its minimum to the value 2, a constant that controls how much error a projection can hide.

Verify this page

The projection constant

The declaration cproj_from_J_second_deriv is a compact theorem in the framework's machine-checked library of formal theorems. It states two facts together: the projection constant Cproj equals 2, and the second derivative of the cost function J, evaluated at the point where its argument is 1, equals 1. The second fact is the normalization condition that pins down the first. In plain terms, the theorem says that when the cost function is measured in the right logarithmic scale, its curvature at the minimum is exactly 1, and that curvature value forces the projection constant to be exactly 2.

The cost function J(x) = (x + 1/x)/2 - 1 measures the price of a recognition event, where x is the ratio of two quantities being compared. Its minimum occurs at x = 1, where the cost is zero. The theorem evaluates the second derivative of J(exp(t)) at t = 0, which is the curvature of the cost when the ratio is expressed in logarithmic coordinates. That curvature equals 1 by a direct calculation from the definition of J. The projection constant Cproj = 2 then appears as a consequence of this normalization, not as an independent assumption.

The theorem belongs to a larger formal structure called the Coercive Projection Method, which analyzes how much error a projection onto a subspace can introduce. The constant Cproj appears in inequalities that bound the size of a defect, the part of a quantity that lies outside the subspace. A value of 2 means that the defect mass is at most twice the orthogonal mass, a bound that holds for any model satisfying the framework's axioms. The theorem thus provides a concrete numerical anchor for a general inequality.

In Recognition Science, this result is one step in a chain that derives physical constants from the cost function. The same normalization appears in the cone constants record, where Knet = 1, Cproj = 2, Ceng = 1, and Cdisp = 1, and in the eight-tick record, where Knet = (9/7)^2. The theorem does not by itself derive any other constant; it only fixes the projection constant given the second-derivative normalization. The derivation of other constants, such as the energy gap coefficient cmin = 1/2 for the cone case, relies on additional theorems.

What the theorem does not claim is equally important. It does not derive the cost function J itself; that derivation is a separate theorem. It does not claim that Cproj = 2 holds for all possible constants; it holds for the specific cone constants record defined in the library. It does not assert any physical interpretation of the projection constant; the interpretation as a bound on defect mass comes from the surrounding framework, not from this declaration alone.

THEOREM cproj_from_J_second_deriv · IndisputableMonolith/CPM/LawOfExistence.lean
cproj_from_J_second_deriv · IndisputableMonolith/CPM/LawOfExistence.lean:295 
/-- C_proj = 2 follows from the J-cost second derivative normalization.

The Hermitian rank-one bound ‖Pψ‖² ≤ C_proj · ‖ψ‖² has optimal constant
C_proj = 2 when the projection is normalized so that J''(1) = 1 in
log-coordinates. This is the content of `RS.Jcost_log_second_deriv_normalized`. -/
theorem cproj_from_J_second_deriv :
    RS.coneConstants.Cproj = 2 ∧
    deriv (deriv (fun t : ℝ => IndisputableMonolith.Cost.Jcost (Real.exp t))) 0 = 1 :=
  ⟨rfl, RS.Jcost_log_second_deriv_normalized⟩
THEOREM Jcost_log_second_deriv_normalized · IndisputableMonolith/CPM/LawOfExistence.lean
Jcost_log_second_deriv_normalized · IndisputableMonolith/CPM/LawOfExistence.lean:222 
/-- J-cost log-coordinate normalization used as justification hook:
`deriv (deriv (J ∘ exp)) 0 = 1`. -/
lemma Jcost_log_second_deriv_normalized :
  deriv (deriv (fun t : ℝ => IndisputableMonolith.Cost.Jcost (Real.exp t))) 0 = 1 := by
  -- Define f(t) = Jcost (exp t) with no cosh expansion
  set f : ℝ → ℝ := fun t => ((Real.exp t + Real.exp (-t)) / 2) - 1 with hfdef
  have hf_eq : (fun t : ℝ => IndisputableMonolith.Cost.Jcost (Real.exp t)) = f := by
    funext t; simp [hfdef, IndisputableMonolith.Cost.Jcost_exp]
  -- First derivative of f: f'(t) = (exp t - exp (-t)) / 2
  have h_deriv_f : deriv f = fun t => (Real.exp t - Real.exp (-t)) / 2 := by
    funext t
    -- derivative of exp and exp∘neg
    have h1 : HasDerivAt (fun s => Real.exp s) (Real.exp t) t := Real.hasDerivAt_exp t
    have h2 : HasDerivAt (fun s => Real.exp (-s)) (- Real.exp (-t)) t := by
      simpa using (Real.hasDerivAt_exp (-t)).comp t (hasDerivAt_neg t)
    have hsum : HasDerivAt (fun s => Real.exp s + Real.exp (-s)) (Real.exp t - Real.exp (-t)) t := by
      simpa [sub_eq_add_neg] using h1.add h2
    -- scale by 1/2 and subtract constant 1
    have hscale : HasDerivAt (fun s => ((Real.exp s + Real.exp (-s)) / 2)) ((Real.exp t - Real.exp (-t)) / 2) t := by
      -- rewrite to mul_const form using div_eq_mul_inv
      have h := hsum.mul_const ((1:ℝ)/2)
      simpa [div_eq_mul_inv, one_div, mul_comm, mul_left_comm, mul_assoc] using h
    have hfinal : HasDerivAt f ((Real.exp t - Real.exp (-t)) / 2) t := by
      simpa [hfdef] using hscale.sub_const 1
    simpa using hfinal.deriv
  -- Second derivative at 0 via derivative of (deriv f)
  have h_d2_has : HasDerivAt (fun s => deriv f s) ((Real.exp 0 + Real.exp (-0)) / 2) 0 := by
    -- rewrite (deriv f) to a smooth expression and differentiate at 0
    have heq : (fun s => deriv f s) = (fun s => (Real.exp s - Real.exp (-s)) / 2) := by
      funext s; simp [h_deriv_f]
    have h1 : HasDerivAt (fun s => Real.exp s) (Real.exp 0) 0 := Real.hasDerivAt_exp 0
    have h2 : HasDerivAt (fun s => Real.exp (-s)) (- Real.exp (-0)) 0 := by
      simpa using (Real.hasDerivAt_exp (-0)).comp 0 (hasDerivAt_neg 0)
    have hsub : HasDerivAt (fun s => Real.exp s - Real.exp (-s)) (Real.exp 0 + Real.exp (-0)) 0 := by
      simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using h1.sub h2
    have hscale : HasDerivAt (fun s => (Real.exp s - Real.exp (-s)) / 2) ((Real.exp 0 + Real.exp (-0)) / 2) 0 := by
      -- multiply on the right by 1/2
      have h := hsub.mul_const ((1:ℝ)/2)
      simpa [div_eq_mul_inv, one_div, mul_comm, mul_left_comm, mul_assoc] using h
    simpa [heq] using hscale
  have h_val : deriv (fun s => deriv f s) 0 = ((Real.exp 0 + Real.exp (-0)) / 2) := by
    simpa using h_d2_has.deriv
  have : deriv (deriv f) 0 = 1 := by
    -- evaluate at zero
    simpa [Real.exp_zero] using h_val
  -- Rewrite through the explicit definition of f
  have this' : deriv (deriv (fun x => ((Real.exp x + Real.exp (-x)) / 2) - 1)) 0 = 1 := by
    simpa [hfdef] using this
  -- Drop the constant (second derivative of constant is zero)
  have this'' : deriv (deriv (fun x => (Real.exp x + Real.exp (-x)) / 2)) 0 = 1 := by
    simpa using this'
  -- rewrite back to the target function
  simpa [hf_eq] using this''
MODEL coneConstants · IndisputableMonolith/CPM/LawOfExistence.lean
coneConstants · IndisputableMonolith/CPM/LawOfExistence.lean:203 
/-- RS-native CPM constants for cone projection. Placeholders are kept
symbolic by default for `C_eng` and `C_disp`; domain instantiations can
refine them. -/
def coneConstants : Constants := {
  Knet  := 1,
  Cproj := 2,
  Ceng  := 1,
  Cdisp := 1,
  Knet_nonneg := by norm_num,
  Cproj_nonneg := by norm_num,
  Ceng_nonneg := by norm_num,
  Cdisp_nonneg := by norm_num
}
THEOREM c_value_cone · IndisputableMonolith/CPM/LawOfExistence.lean
c_value_cone · IndisputableMonolith/CPM/LawOfExistence.lean:358 
/-- RS cone coercivity constant is 1/2. -/
theorem c_value_cone : cmin RS.coneConstants = 1/2 := by
  simp only [cmin, RS.cone_Knet_eq_one, RS.cone_Cproj_eq_two, RS.cone_Ceng_eq_one]
  norm_num

What this page does not claim

This theorem does not derive the cost function J itself. Cproj = 2 holds only for the specific cone constants record, not for every possible choice of constants. The declaration carries no physical interpretation; the bound on defect mass comes from the surrounding framework.

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/CPM/LawOfExistence.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