Gravity Coherence Collapse Jcost Nonneg

A cost that cannot go negative

The function J(x) = (x + 1/x)/2 - 1 is a simple algebraic expression that appears throughout the Recognition Science framework as a measure of recognition cost. For any positive number x, this expression is always greater than or equal to zero. The theorem Jcost_nonneg in the framework's machine-checked library of formal theorems proves this non-negativity directly: it rewrites the expression as (x - 1)² / (2x), which is a square divided by a positive number, hence never negative.

This non-negativity is not a trivial observation. In the framework, J(x) represents the cost of recognizing a state, and a cost that could go negative would be physically meaningless. The theorem guarantees that the cost function behaves sensibly for all positive inputs. It reaches its minimum value of zero exactly at x = 1, where the expression (x + 1/x)/2 equals 1. For any other positive x, the cost is strictly positive, growing as x moves away from 1 in either direction.

The theorem is a small but load-bearing piece of a larger structure. In the framework's account of gravitational collapse and quantum measurement, this cost function is integrated along a path to define a recognition action C. The non-negativity of J ensures that this action is itself non-negative, a prerequisite for interpreting exp(-C) as a probability weight. The framework then derives the Born rule of quantum mechanics, P = |amplitude|², from this cost structure, and proposes a mesoscopic threshold around 0.2 nanograms where quantum superpositions give way to classical behavior.

In Recognition Science, the non-negativity theorem is one step in a chain that aims to unify quantum measurement with gravitational collapse. The framework models the recognition cost along a geodesic rotation as twice a residual rate action, and from this identity derives the Born rule. The Jcost_nonneg theorem does not by itself establish any physical claim; it is a mathematical fact about a specific function. What it does is guarantee that the cost function used in the framework is well-behaved, providing a foundation for the subsequent physical derivations.

The theorem's scope is deliberately narrow. It applies only to positive real numbers x, and it makes no statement about what happens for negative x or zero. It does not claim that the cost function is the only possible one, nor does it derive the specific form of J from first principles. Those are separate results in the framework. What Jcost_nonneg establishes is a clean, checkable property: for positive inputs, the recognition cost never dips below zero.

This matters because it is the kind of fact that makes a physical theory usable. A cost function that could go negative would produce probabilities greater than one or negative probabilities, breaking the probabilistic interpretation. The theorem closes that door, ensuring that the framework's cost structure is consistent with the basic requirements of probability theory. It is a small result, but it is the kind of small result that a larger edifice depends on.

/-- J-cost is non-negative for positive x. -/
theorem Jcost_nonneg (x : ℝ) (hx : 0 < x) : 0 ≤ Jcost x := by
  unfold Jcost
  have : (x - 1)^2 / (2 * x) ≥ 0 := div_nonneg (sq_nonneg _) (by linarith)
  have : (x + x⁻¹) / 2 - 1 = (x - 1)^2 / (2 * x) := by field_simp; ring
  linarith

/-- Born weight is positive. -/
theorem born_weight_pos (C_I : ℝ) : 0 < born_weight C_I := Real.exp_pos _

/-- For the C = 2A case: born_weight = sin²(θ_s).
    This follows from exp(-2A) = exp(2 ln sin θ) = sin²θ. -/
theorem born_weight_is_sin_sq (theta_s : ℝ) (h_sin_pos : 0 < Real.sin theta_s) :
    born_weight (recognition_action theta_s) =
    (Real.sin theta_s) ^ 2 := by
  unfold born_weight recognition_action rate_action
  rw [show -(2 * -Real.log (Real.sin theta_s)) = 2 * Real.log (Real.sin theta_s) from by ring]
  rw [show (2 : ℝ) * Real.log (Real.sin theta_s) =
      Real.log ((Real.sin theta_s) ^ 2) from by
    rw [Real.log_pow]; ring]
  rw [Real.exp_log (sq_pos_of_pos h_sin_pos)]

What this page does not claim

The theorem does not prove that the cost function J(x) is the only possible cost function. The theorem does not apply to non-positive values of x. The theorem does not by itself establish any physical claim about gravity or quantum mechanics.

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/Gravity/CoherenceCollapse.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: