Gravity Ilgreal Exponent Enhancement Enhancement Real Pos

The radial weight

In the Recognition Science framework's treatment of gravity, a central object is a radial weight: a number that multiplies a velocity-squared term and grows with distance from a source. The framework defines this weight as w_real(R, r0, α) = 1 + C · (R/r0)^α, where R is the distance from the source, r0 is a reference radius, C is a positive constant, and α is an exponent. The definition itself does not require α to be positive; it is a formal expression that works for any real exponent.

The theorem named enhancement_real_pos establishes that this weight is always greater than zero whenever both R and r0 are positive, regardless of the value of α. The proof is short and mechanical: a positive distance ratio raised to any real power stays positive, multiplying by a positive constant keeps it positive, and adding 1 leaves the result strictly above zero. The same argument actually proves the stronger statement that the weight is greater than 1, which the library records as a separate theorem, enhancement_real_above_one.

This positivity fact matters because the weight appears as a multiplier on a velocity-squared term in the framework's gravity equations. A negative or zero weight would flip the sign of that term, producing unphysical behavior such as a squared velocity that decreases with distance. The theorem guarantees that cannot happen for any positive distance, so the enhancement never reverses the direction of the term it multiplies. The library also proves that the weight grows without bound as R increases, and that it strictly increases with R when α is positive, facts that together describe how the enhancement behaves at large distances.

The theorem does not claim that the weight is positive for all real R; it requires R and r0 to be positive. It does not assign a value to the constant C or the exponent α, and it does not say anything about what the weight means physically beyond its role as a multiplier. The positivity result is a structural guarantee, not a physical prediction.

theorem enhancement_real_pos (R r0 α : ℝ)
    (hR : 0 < R) (hr0 : 0 < r0) :
    0 < w_real R r0 α := by
  unfold w_real
  have hC : 0 < C_lock := C_lock_pos
  have hd : 0 < R / r0 := div_pos hR hr0
  have hpow : 0 < (R / r0) ^ α := Real.rpow_pos_of_pos hd α
  have : 0 < C_lock * (R / r0) ^ α := mul_pos hC hpow
  linarith

theorem enhancement_real_above_one (R r0 α : ℝ)
    (hR : 0 < R) (hr0 : 0 < r0) :
    1 < w_real R r0 α := by
  unfold w_real
  have hC : 0 < C_lock := C_lock_pos
  have hd : 0 < R / r0 := div_pos hR hr0
  have hpow : 0 < (R / r0) ^ α := Real.rpow_pos_of_pos hd α
  have : 0 < C_lock * (R / r0) ^ α := mul_pos hC hpow
  linarith

What this page does not claim

The theorem does not claim positivity for zero or negative distances. It does not assign numerical values to the constant or the exponent. It does not state that the weight itself is a measurable physical quantity.

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