Gravity Derived Factors

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.lean 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.lean. The suppression limits are established in Lean, 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

THEOREM hsb_suppression_limit · IndisputableMonolith/Gravity/DerivedFactors.lean

THEOREM lsb_unsuppressed_limit · IndisputableMonolith/Gravity/DerivedFactors.lean

MODEL n_derived · IndisputableMonolith/Gravity/DerivedFactors.lean

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: