Encyclopedia Gravity Gravity Derived Factors

ARTICLE 4 claims 2 theorems 2 models

Gravity Derived Factors

Gravity derived factors are the suppression and radial terms that adjust the ILG kernel to match galaxy rotation, with a established high-acceleration limit.

Verify this page

Gravity Derived Factors

Gravity derived factors are the correction terms in Recognition Science that adjust the ILG kernel, the framework's modification to Newtonian gravity, to match observed galaxy rotation curves. The module DerivedFactors.the kernel-checked library addresses a specific empirical problem: the ILG kernel overpredicts rotation velocities for High Surface Brightness (HSB) galaxies, which are baryon-dominated, and underpredicts for Low Surface Brightness (LSB) galaxies, which are dark-matter-dominated. The core idea is a suppression mechanism that turns off the ILG effect at high accelerations, recovering Newtonian behavior.

The suppression factor xi_derived is defined as 1 / (1 + g / (8*a0)), where g is baryonic acceleration and a0 is the characteristic acceleration scale. The factor 8 comes from the seven-beat gap: an 8-beat cycle has 7 active modes, while a 7-beat cycle has 6 degrees of freedom, giving a relative gap of 1/8. The saturation acceleration is therefore 8 times a0, the stiffness of the 8-beat lock. The module proves two limits: as acceleration goes to infinity, the suppression factor tends to 0, meaning the ILG modification vanishes; as acceleration goes to zero, the factor tends to 1, meaning the full ILG effect is present. The radial profile n_derived is currently set to unity, with the hypothesis that the suppression factor handles the main systematic bias.

These definitions and theorems are in the public module IndisputableMonolith/Gravity/DerivedFactors.the kernel-checked library. The suppression limits are established in the kernel-checked library, but the functional forms and the physical interpretation of the seven-beat gap are hypotheses, not derived results. The module does not claim to have solved the LSB underprediction; it identifies it as a remaining target.

MODEL xi_derived · IndisputableMonolith/Gravity/DerivedFactors.lean
xi_derived · IndisputableMonolith/Gravity/DerivedFactors.lean:69 
/-- 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))
THEOREM hsb_suppression_limit · IndisputableMonolith/Gravity/DerivedFactors.lean
hsb_suppression_limit · IndisputableMonolith/Gravity/DerivedFactors.lean:107 
/-- 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_unsuppressed_limit · IndisputableMonolith/Gravity/DerivedFactors.lean
lsb_unsuppressed_limit · IndisputableMonolith/Gravity/DerivedFactors.lean:121 
/-- 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
MODEL n_derived · IndisputableMonolith/Gravity/DerivedFactors.lean
n_derived · IndisputableMonolith/Gravity/DerivedFactors.lean:88 
/-- The radial profile `n(r)` was calibrated to increase at large radii.
    From a derived perspective, this is likely the inverse of the suppression.

    As r increases, acceleration g drops.
    So ξ(g) increases towards 1.

    If `n(r)` is meant to provide *extra* boost at very low density (LSB underprediction),
    it might be a "Resonance" term that kicks in when `g < a0`.

    Hypothesis: `n(r)` is related to the `ScaleGate` threshold `λ_rec`.
    If density drops near `λ_rec`, maybe we get critical opalescence (enhancement)?

    For now, we define `n_derived` as unity, assuming `xi_derived` handles the
    main systematic bias (HSB overprediction). The LSB underprediction might
    require tuning `a0` or `C` rather than a separate `n(r)`. -/
def n_derived : ℝ := 1

What this page does not claim

Not a derivation of the suppression factor's functional form from first principles. Not a solution to the LSB underprediction problem. Not a claim that the seven-beat leakage mechanism is physically established.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND