Gravity Coercive Projection No Retuning Consistent

The consistency statement

The declaration no_retuning_consistent is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states a mathematical fact about a weight function w that is always at least 1: for any real numbers x and f, the product w(x) * f^2 is nonnegative. In plain terms, if the weight operator never shrinks a signal below its original size, then the energy it defines can never fall below zero.

This is the formal core of the framework's "no per-galaxy retuning" claim. The energy functional in its Information-Limited Gravity model is built from such weight operators. The theorem shows that the energy is bounded below, which is a necessary condition for the existence of a unique energy minimizer. The framework's library also proves the coercivity constant c = 49/162, the net constant K_net = 81/49, and the positivity of the operator, all of which are assembled into a single certificate that the minimization problem is well-posed.

In Recognition Science, the theorem does not claim that any particular galaxy's rotation curve is predicted without fitting. It does not assert that the weight function w is derived from first principles, nor that the energy minimizer has been found. The theorem only establishes the consistency of the no-retuning principle: the mathematical structure admits a well-defined minimization problem. The physical bridge from this formal result to observed galaxy dynamics remains a separate, open question.

/-- The no-retuning condition is consistent with operator positivity:
    if w_global(x) >= 1 for all x, the energy at w_global is bounded
    but finite, so a unique minimizer exists. -/
theorem no_retuning_consistent (w : ℝ → ℝ) (hw : ∀ x, 1 ≤ w x) :
    ∀ x f : ℝ, 0 ≤ w x * f ^ 2 :=
  fun x f => energy_bounded_below (w x) f (hw x) (sq_nonneg f)

/-- The no-retuning condition is consistent with operator positivity:
    if w_global(x) >= 1 for all x, the energy at w_global is bounded
    but finite, so a unique minimizer exists. -/
theorem no_retuning_consistent (w : ℝ → ℝ) (hw : ∀ x, 1 ≤ w x) :
    ∀ x f : ℝ, 0 ≤ w x * f ^ 2 :=
  fun x f => energy_bounded_below (w x) f (hw x) (sq_nonneg f)

theorem c_coercive_value : c_coercive = 49 / 162 := rfl

theorem K_net_value : K_net = 81 / 49 := by
  unfold K_net; norm_num

/-- The ILG weight operator is positive: if w(x) >= 1 for all x,
    then <f, w*f> >= ||f||^2 (in L^2 inner product sense).

    We formalize this pointwise: w(x) * f(x)^2 >= f(x)^2. -/
theorem operator_positivity_pointwise (w_val f_val : ℝ) (hw : 1 ≤ w_val) :
    f_val ^ 2 ≤ w_val * f_val ^ 2 := by
  nlinarith [sq_nonneg f_val]

What this page does not claim

The theorem does not predict any observed galaxy rotation curve without fitting parameters. The theorem does not derive the weight function w from first principles. The theorem does not prove that the energy minimizer has been explicitly found.

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/CoerciveProjection.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: