btfrData
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.