btfrData
btfrData defines a string constant that records the observed baryonic Tully-Fisher relation. Galaxy dynamics researchers would cite it when comparing Recognition Science ledger models to cold dark matter simulations. The definition is a direct string literal with no computation or lemma applications.
claimThe baryonic Tully-Fisher relation states that baryonic mass scales as the fourth power of rotation velocity, $M_ {baryon} ∝ v^4$, with scatter below 0.1 dex.
background
The module derives flat galaxy rotation curves from dark matter as ledger shadows tied to odd phases in the eight-tick cycle. Flat curves follow from isothermal ledger distributions and J-cost equilibrium, while the standard Keplerian falloff is replaced by constant velocity at large radii. Upstream, the tick supplies the fundamental time quantum, phase from EightTick generates the periodic structure for ledger counting, and cost functions from MultiplicativeRecognizerL4 and ObserverForcing quantify the recognition costs that set equilibrium profiles.
proof idea
The definition is a direct string literal assignment. No lemmas or tactics are invoked; the body simply records the empirical statement for reference in the module's predictions section.
why it matters in Recognition Science
This definition supplies the empirical anchor for the Tully-Fisher item in the module's RS predictions list. It connects to J-cost equilibrium and eight-tick phase counting that produces the 5:1 dark matter ratio. The relation's tightness challenges cold dark matter while matching the MOND-like low-acceleration regime that emerges from Recognition Science forcing.
scope and limits
- Does not derive the $v^4$ scaling from ledger axioms or the forcing chain.
- Does not express the scatter bound in RS-native units.
- Does not specify the radial or velocity range of validity.
- Does not connect the exponent 4 to a concrete step in the T0-T8 chain.
formal statement (Lean)
197def btfrData : String :=
proof body
Definition body.
198 "M_baryon ∝ v⁴ with scatter < 0.1 dex"
199
200/-! ## Predictions -/
201
202/-- RS predictions for galaxy rotation:
203
204 1. **Flat curves**: From isothermal ledger distribution
205 2. **Cores, not cusps**: From ledger interactions at high density
206 3. **Tully-Fisher**: From J-cost equilibrium
207 4. **MOND-like behavior**: At low accelerations
208 5. **DM ratio ≈ 5:1**: From 8-tick phase counting -/