summary
plain-language theorem explainer
The summary definition enumerates five points framing galaxy rotation curves as consequences of ledger shadows and J-cost equilibrium in Recognition Science. Cosmologists examining alternatives to particle dark matter would cite it to contrast RS ledger distributions with standard CDM halos. It is realized as a direct list definition with no computational steps or lemmas applied.
Claim. The Recognition Science account of galaxy rotation consists of the list: dark matter equals ledger shadows; halo arises from J-cost equilibrium; flat curves follow from density proportional to $1/r^2$; cores arise from ledger interactions; Tully-Fisher relation follows from J-cost.
background
The Cosmology.GalaxyRotation module starts from the observed failure of Keplerian falloff at large radii and attributes the required extra mass to dark ledger entries, which are odd-phase 8-tick recognitions. J-cost is the cost function induced by a multiplicative recognizer (derivedCost of its comparator on positive ratios) and equivalently the J-cost of any recognition event. Equilibrium holds when Jcost equals zero, as stated by the theorem Jcost 1 = 0. The upstream from theorem in PrimitiveDistinction supplies the structural conditions under which these ledger objects are well-defined.
proof idea
The definition is a direct enumeration of the five explanatory strings. It draws on the equilibrium theorem from NonlinearDynamicsFromRS together with the two cost definitions from MultiplicativeRecognizerL4 and ObserverForcing, but performs no further reduction or tactic steps.
why it matters
This definition condenses the RS derivation of flat rotation curves from J-cost equilibrium and the eight-tick octave structure, placing dark matter as ledger shadows rather than particles. It supports the module's claim that cores arise naturally from ledger interactions and that the Tully-Fisher relation follows directly from J-cost scaling. No downstream theorems are recorded, leaving open the quantitative matching of predicted halo profiles to specific galaxy data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.