Gravity Derived Factors Xi Derived

The suppression factor

Galaxy rotation curves posed a puzzle for decades: the outer parts of galaxies spin as if more mass were present than the stars and gas can account for. Modified gravity explanations, including the one explored inside the Recognition Science framework, try to reproduce those curves by altering the gravitational force law at low accelerations. But that same modification, applied naively, predicts rotation velocities that are too high for high surface brightness galaxies, where ordinary matter dominates. The framework's library contains a definition, xi_derived, that is meant to suppress the modification precisely in that regime.

The definition is a simple saturation function. If g is the baryonic acceleration and a0 is a characteristic scale, the suppression factor is ξ(g) = 1 / (1 + g / (8·a0)). The factor multiplies the modified-gravity kernel amplitude. When g is much smaller than 8·a0, ξ is close to 1, so the full modification survives. When g is much larger, ξ approaches 0, so the force law returns to the standard Newtonian form. The factor 8 comes from the gap between an 8-beat cycle and a 7-beat cycle, a distinction the framework derives from its recognition-cycle structure.

Two limit theorems are proved in the machine-checked library. As the baryonic acceleration goes to infinity, ξ tends to 0, which is the Newtonian recovery. As the acceleration goes to zero, ξ tends to 1, which is the unsuppressed low-acceleration regime. These are the only two formal results attached to the definition. The definition itself is a modeling choice, not a derivation: the functional form 1/(1+x) is chosen because it is the standard saturation shape, and the coefficient 8 is chosen from the 7-beat gap. The radial profile n(r), a companion factor in the same module, is set to 1, with the comment that the LSB underprediction might be handled by tuning other parameters instead.

What the declaration does not claim is as important as what it proves. It does not prove that the suppression factor is unique, nor that it follows from first principles. The docstring itself calls the mechanism a hypothesis. It does not prove that the factor actually matches any observed rotation curve; that would require an empirical check against galaxy data, which the library does not contain. It does not even prove that the 8-beat structure is physically real; that bridge from recognition cycles to gravity is left open in the framework. The two proved theorems only establish the asymptotic behavior of a chosen function.

In plain terms, the declaration gives a concrete candidate for how a modified gravity theory might hide its modification in high-acceleration environments. The candidate is plausible and its limits are mathematically clean, but it is a starting point for testing, not a finished result. A reader should treat ξ as a proposed piece of the model, with exactly two proved properties, and look elsewhere in the framework for the derivation of the 8-beat cycle itself.

/-- Theorem: HSB Suppression recovers Newtonian limit.
    As baryon acceleration goes to infinity, the ILG modification vanishes. -/
theorem hsb_suppression_limit (a0 : ℝ) (ha0 : a0 > 0) :
    Filter.Tendsto (fun g => xi_derived g a0) Filter.atTop (nhds 0) := by
  unfold xi_derived
  have h_sat_pos : a_saturation a0 > 0 := by
    unfold a_saturation lock_stiffness seven_beat_gap
    linarith
  -- Rewrite 1/(1+x) as (1+x)⁻¹ to match inv_tendsto_atTop
  rw [show (fun g => 1 / (1 + g / a_saturation a0)) = (fun g => (1 + g / a_saturation a0)⁻¹) by ext; simp]
  apply Filter.Tendsto.inv_tendsto_atTop
  apply Filter.tendsto_atTop_add_const_left
  apply Filter.Tendsto.atTop_mul_const (inv_pos.mpr h_sat_pos) Filter.tendsto_id

/-- Theorem: LSB Limit is Unsuppressed.
    As baryon acceleration goes to zero, the suppression factor goes to 1. -/
theorem lsb_unsuppressed_limit (a0 : ℝ) (ha0 : a0 > 0) :
    Filter.Tendsto (fun g => xi_derived g a0) (nhds 0) (nhds 1) := by
  unfold xi_derived
  -- We prove 1 / (1 + g / K) -> 1
  -- Rewrite 1 as 1 / (1 + 0 / K)
  conv in (nhds 1) => rw [show (1 : ℝ) = 1 / (1 + 0 / a_saturation a0) by
    field_simp [a_saturation, lock_stiffness, seven_beat_gap]; linarith]
  apply Filter.Tendsto.div
  · exact tendsto_const_nhds
  · apply Filter.Tendsto.add
    · exact tendsto_const_nhds
    · apply Filter.Tendsto.div
      · exact Filter.tendsto_id
      · exact tendsto_const_nhds
      · -- Denominator ≠ 0
        unfold a_saturation lock_stiffness seven_beat_gap
        linarith
  · -- Limit denominator (1 + 0) ≠ 0
    norm_num

/-- The HSB suppression factor ξ(g).
    This factor multiplies the ILG kernel amplitude.

    Behavior:
    - Low g (<< a_sat): ξ ≈ 1 (Full ILG effect)
    - High g (>> a_sat): ξ -> 0 (Newtonian recovery)

    Functional form: Standard saturation `1 / (1 + x)`.
    Argument x: `g / a_sat`.

    Formula: ξ(g) = 1 / (1 + g / (8*a0))

    This provides the necessary suppression for HSB galaxies (where g is high)
    while maintaining the ILG boost for LSB galaxies (where g is low). -/
def xi_derived (g_baryon : ℝ) (a0 : ℝ) : ℝ :=
  1 / (1 + g_baryon / (a_saturation a0))

What this page does not claim

Not a derivation of the suppression factor from the recognition-cost function. Not a proof that the factor matches any observed galaxy rotation curve. Not a proof that the 8-beat cycle is physically real in gravity. Not a claim that the radial profile n(r) is derived; it is set to 1.

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