Encyclopedia Gravity Gravity Derived Factors N Derived
ARTICLE 3 claims 1 theorem 2 models
Gravity Derived Factors N Derived
In the Recognition Science library, n_derived is simply the constant 1, a placeholder that says the radial shape needs no separate correction.
The radial factor n_derived
The declaration n_derived is a definition in the machine-checked library. It sets a number called the radial factor to exactly 1. The radial factor is a multiplier meant to adjust a galaxy rotation model as distance from the center grows. Setting it to 1 means the model uses no extra radial adjustment beyond what the main suppression factor already provides.
The context is a known problem. A model called ILG overpredicts rotation speeds for high-surface-brightness galaxies, where ordinary matter dominates, and underpredicts for low-surface-brightness galaxies, where dark matter dominates. The library's proposed fix is a suppression factor, named xi_derived, that reduces the model's effect at high acceleration and lets it recover Newtonian behavior. That factor has a specific form: xi(g) = 1 / (1 + g / (8 * a0)), where g is baryonic acceleration and a0 is a characteristic scale. The number 8 comes from a hypothesized stiffness of an 8-beat cycle against leakage into a 7-beat mode. The radial factor n_derived is separate. The docstring says that, for now, the suppression factor handles the main systematic bias, so n_derived is defined as unity. The low-surface-brightness underprediction might be fixed by tuning a0 or another constant, not by a separate radial profile.
The definition carries no proof. It is a choice, a placeholder. The library does prove two limits for the suppression factor: as acceleration goes to infinity, xi tends to 0, and as acceleration goes to zero, xi tends to 1. Those are results. But n_derived itself is not derived from anything; it is set to 1. The docstring even calls the radial profile a hypothesis about a resonance term, but the formal definition does not implement that hypothesis.
What a reader should take away: n_derived is a formal placeholder that says the radial direction needs no correction in the current model. It is not a result about galaxies. It is not a measured value. It is not a prediction. It is a constant set to 1 so the model can proceed while the suppression factor does the work.
MODEL n_derived · IndisputableMonolith/Gravity/DerivedFactors.lean
/-- 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
MODEL n_derived · IndisputableMonolith/Gravity/DerivedFactors.lean
/-- 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
THEOREM hsb_suppression_limit · lsb_unsuppressed_limit · IndisputableMonolith/Gravity/DerivedFactors.lean
/-- 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
What this page does not claim
n_derived is not derived from any principle; it is a placeholder set to 1. The radial factor does not claim to explain low-surface-brightness underprediction. The theorems about xi_derived do not prove that the suppression mechanism is physically correct.
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:
- What physical evidence would require n_derived to differ from 1?
- How does the suppression factor xi_derived relate to the measured rotation curves of HSB and LSB galaxies?
- What is the derivation of the characteristic acceleration a0 in the framework?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
MODEL n_derived · IndisputableMonolith/Gravity/DerivedFactors.lean
/-- 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 : ℝ := 1The declaration n_derived is a definition in the machine-checked library. n_derived · IndisputableMonolith/Gravity/DerivedFactors.leanMODEL n_derived · IndisputableMonolith/Gravity/DerivedFactors.lean
/-- 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 : ℝ := 1It sets a number called the radial factor to exactly 1. n_derived · IndisputableMonolith/Gravity/DerivedFactors.leanTHEOREM hsb_suppression_limit · lsb_unsuppressed_limit · IndisputableMonolith/Gravity/DerivedFactors.lean
/-- 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_numThe library proves two limits for the suppression factor: as acceleration goes to infinity, xi tends to 0, and as acceleration goes to zero, xi tends to 1. hsb_suppression_limit · lsb_unsuppressed_limit · IndisputableMonolith/Gravity/DerivedFactors.lean