Dark.lean — FrcLedger

1import Mathlib2import FrcLedger.Theme.Dark3import FrcLedger.Keys.Chart45/-!6# 32-dark — the chart readings on Mathlib (18 October 2026)78The paper module of *The Dark Sector over Finite Relational Substrate* (tree `32-dark-20260627`) on Mathlib: every9declaration is the chart theme's, under the paper's name — the floor value and the running floor (`FRC.Chart`), the10registration root, the crossover squeeze with the Tully–Fisher algebra, the deep limit and the discriminant11(`FRC.Strong`, shared with 21-gravity), and the dark readings of `FrcLedger/Theme/Dark.lean` (`FRC.DarkML`): the12first-passage factor and its reduction, the conditional count and the chart angle, the strictly increasing relation,13the external field, the scatter's deep rise, the coherence weight and `N_eff`, the small-tilt response, the sign of Λ,14the redshift zero-point, the wide binaries, the pressure-supported offset and the Λ-face floor. Classical (tier 2).15The finite content is the core's (`FrcCore/Theme/Dark.lean`, no axioms); the predicates `p32NNN` at the end are16generated by `make_predicates.py`, aliases of the keys of `Keys/Chart.lean`.17-/1819namespace FRC.Dark2021open Real2223/-! ## Old names (18 October 2026): every declaration of this module is an alias of the chart theme's (`FRC.Chart`,24`FRC.Strong`, `FRC.DarkML`), under the paper's name -/2526/-- 32:C2, 32:X2, 32:X10 — `Chart.floor_value`. -/27theorem floor_value (c H0 : ℝ) (hc : c = 299792458) (hH : H0 = 67.4e3 / 3.0856775814913673e22) :28    (1.04e-10 : ℝ) < c * H0 / (2 * π) ∧ c * H0 / (2 * π) < 1.05e-10 ∧29    (0.868 : ℝ) < c * H0 / (2 * π) / 1.2e-10 ∧ c * H0 / (2 * π) / 1.2e-10 < 0.870 ∧30    (0.65 : ℝ) < (1.2e-10 - c * H0 / (2 * π)) / 0.24e-10 ∧31    (1.2e-10 - c * H0 / (2 * π)) / 0.24e-10 < 0.67 :=32  FRC.Chart.floor_value c H0 hc hH3334/-- 32:P1 — `Chart.running_floor`. -/35theorem running_floor (c G M : ℝ) (H a v : ℝ → ℝ) (z : ℝ) (hc : 0 < c) (hG : 0 < G) (hM : 0 < M)36    (h0 : 0 < H 0) (hz : 0 < H z) (ha : ∀ z, a z = c * H z / (2 * π)) (hv0 : 0 < v 0) (hvz : 0 < v z)37    (htf : ∀ z, v z ^ 4 = G * M * a z) :38    a z / a 0 = H z / H 0 ∧ v z / v 0 = (H z / H 0) ^ (1 / 4 : ℝ) :=39  FRC.Chart.running_floor c G M H a v z hc hG hM h0 hz ha hv0 hvz htf4041/-- 32:C6, 32:X4 — `Strong.registration_root`. -/42theorem registration_root (w : ℝ) (hw0 : 0 < w) (hw1 : w < 1) :43    w * ((1 - √(1 - w ^ 2)) / w) ^ 2 - 2 * ((1 - √(1 - w ^ 2)) / w) + w = 0 ∧44    0 < (1 - √(1 - w ^ 2)) / w ∧ (1 - √(1 - w ^ 2)) / w < 1 ∧45    1 < (1 + √(1 - w ^ 2)) / w ∧46    (∀ x : ℝ, w * x ^ 2 - 2 * x + w = 0 →47      x = (1 - √(1 - w ^ 2)) / w ∨ x = (1 + √(1 - w ^ 2)) / w) :=48  FRC.Strong.registration_root w hw0 hw14950/-- 32:C4, 32:C5, 32:C6, 32:X3 — `Strong.crossover_limits`. -/51theorem crossover_limits (t : ℝ) (ht : 0 < t) :52    0 < 1 - exp (-t) ∧ 1 ≤ t / (1 - exp (-t)) ∧53    (t ≤ 1 → t / (1 - exp (-t)) ≤ 1 / (1 - 3 * t / 4)) ∧54    (∀ G M r a₀ v : ℝ, 0 < r → 0 ≤ G * M → 0 ≤ a₀ →55      v ^ 2 = √(G * M / r ^ 2 * a₀) * r → v ^ 4 = G * M * a₀) :=56  FRC.Strong.crossover_limits t ht5758/-- 32:C4 — `Strong.crossover_deep_limit`. -/59theorem crossover_deep_limit :60    Filter.Tendsto (fun t : ℝ => t / (1 - exp (-t))) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1) :=61  FRC.Strong.crossover_deep_limit6263/-- 32:C6, 32:X4 — `Strong.interpolant_discriminant`. -/64theorem interpolant_discriminant :65    (1.11966 : ℝ) < 1 / (1 - exp (-√5)) ∧ 1 / (1 - exp (-√5)) < 1.11967 ∧66    (1.17082 : ℝ) < 1 / 2 + √(1 / 4 + 1 / 5) ∧ 1 / 2 + √(1 / 4 + 1 / 5) < 1.17083 ∧67    (0.0511 : ℝ) < (1 / 2 + √(1 / 4 + 1 / 5)) - 1 / (1 - exp (-√5)) ∧68    (1 / 2 + √(1 / 4 + 1 / 5)) - 1 / (1 - exp (-√5)) < 0.0512 :=69  FRC.Strong.interpolant_discriminant7071/-- 32:C7 — `DarkML.passage_factor`. -/72theorem passage_factor (u : ℝ) (hu : 1 ≤ u) :73    (1 - √(1 - (1 / u) ^ 2)) / (1 / u) = u - √(u ^ 2 - 1) ∧74    (u - √(u ^ 2 - 1)) * (u + √(u ^ 2 - 1)) = 1 ∧75    exp (-Real.log (u + √(u ^ 2 - 1))) = u - √(u ^ 2 - 1) :=76  FRC.DarkML.passage_factor u hu7778/-- 32:C7 — `DarkML.passage_reduction`. -/79theorem passage_reduction (s : ℝ) (hs : 0 < s) :80    √(2 * s) ≤ Real.log (exp s + √(exp s ^ 2 - 1)) ∧81    Real.log (exp s + √(exp s ^ 2 - 1)) ≤ √(2 * s) * exp (s / 2) :=82  FRC.DarkML.passage_reduction s hs8384/-- 32:C6, 32:X4 — `DarkML.rar_from_count`. -/85theorem rar_from_count (x gb gobs : ℝ) (hx : 0 < x) :86    0 < 1 - exp (-√x) ∧87    ((1 - exp (-√x)) * gobs = gb ↔ gobs = gb / (1 - exp (-√x))) ∧88    sin (arcsin (√(exp (-√x)))) ^ 2 = exp (-√x) ∧89    cos (arcsin (√(exp (-√x)))) ^ 2 = 1 - exp (-√x) :=90  FRC.DarkML.rar_from_count x gb gobs hx9192/-- 32:X11, 32:P6 — `DarkML.rar_monotone`. -/93theorem rar_monotone : StrictMonoOn (fun x : ℝ => x / (1 - exp (-√x))) (Set.Ioi 0) :=94  FRC.DarkML.rar_monotone9596/-- 32:C9, 32:X6 — `DarkML.nu_antitone`. -/97theorem nu_antitone (y₁ y₂ : ℝ) (h0 : 0 < y₁) (h : y₁ < y₂) :98    1 / (1 - exp (-√y₂)) < 1 / (1 - exp (-√y₁)) :=99  FRC.DarkML.nu_antitone y₁ y₂ h0 h100101/-- 32:C9 — `DarkML.collinear_bound`. -/102theorem collinear_bound (gin gext : EuclideanSpace ℝ (Fin 3)) : ‖gin + gext‖ ≤ ‖gin‖ + ‖gext‖ :=103  FRC.DarkML.collinear_bound gin gext104105/-- 32:C8, 32:X5, 32:P2 — `DarkML.scatter_deep`. -/106theorem scatter_deep (x y : ℝ) (hx : 0 < x) (hxy : x < y) :107    1 / (exp (√y) - 1) < 1 / (exp (√x) - 1) ∧108    (x ≤ 1 → (1 - √x) / √x ≤ 1 / (exp (√x) - 1) ∧ 1 / (exp (√x) - 1) < 1 / √x) :=109  FRC.DarkML.scatter_deep x y hx hxy110111/-- 32:C10, 32:X7 — `DarkML.coherence_weight`. -/112theorem coherence_weight (n : ℕ) (hn : 0 < n) (z : Fin n → ℂ) (h : ∀ k, ‖z k‖ = 1) (z₀ : ℂ) (h₀ : ‖z₀‖ = 1) :113    ‖(∑ k, z k) / n‖ ^ 2 ≤ 1 ∧ ‖(∑ _k : Fin n, z₀) / n‖ ^ 2 = 1 :=114  FRC.DarkML.coherence_weight n hn z h z₀ h₀115116/-- 32:X8 — `DarkML.neff_bounds`. -/117theorem neff_bounds (n : ℕ) (g : Fin n → ℝ) (hg : ∀ k, 0 ≤ g k) :118    ∑ k, g k ≤ (∑ k, √(g k)) ^ 2 ∧ (∑ k, √(g k)) ^ 2 ≤ n * ∑ k, g k :=119  FRC.DarkML.neff_bounds n g hg120121/-- 32:C4 — `DarkML.odd_linear_response`. -/122theorem odd_linear_response (f : ℝ → ℝ) (χ : ℝ) (hodd : ∀ T, f (-T) = -f T) (hd : HasDerivAt f χ 0)123    (hχ : χ ≠ 0) :124    Filter.Tendsto (fun T : ℝ => f T / (χ * T)) (nhdsWithin 0 {0}ᶜ) (nhds 1) :=125  FRC.DarkML.odd_linear_response f χ hodd hd hχ126127/-- 32:C11, 32:X9, 32:X10 — `DarkML.lambda_positive`. -/128theorem lambda_positive (r S : ℝ) (hr : r ≠ 0) (hS : r ^ 2 = S / π) : 0 < 3 / r ^ 2 ∧ 3 / r ^ 2 * S = 3 * π :=129  FRC.DarkML.lambda_positive r S hr hS130131/-- 32:P1 — `DarkML.ez_quarter_brackets`. -/132theorem ez_quarter_brackets :133    (1.072 : ℝ) < √(√(√(0.315 * 1.5 ^ 3 + 0.685))) ∧ √(√(√(0.315 * 1.5 ^ 3 + 0.685))) < 1.073 ∧134    (1.156 : ℝ) < √(√(√(0.315 * 2 ^ 3 + 0.685))) ∧ √(√(√(0.315 * 2 ^ 3 + 0.685))) < 1.158 ∧135    (1.319 : ℝ) < √(√(√(0.315 * 3 ^ 3 + 0.685))) ∧ √(√(√(0.315 * 3 ^ 3 + 0.685))) < 1.320 :=136  FRC.DarkML.ez_quarter_brackets137138/-- 32:P3 — `DarkML.wide_binary_band`. -/139theorem wide_binary_band :140    (0.115 : ℝ) < √(1 / (1 - exp (-√2.6535))) - 1 ∧ √(1 / (1 - exp (-√2.6535))) - 1 < 0.116 ∧141    (0.148 : ℝ) < √(1 / (1 - exp (-√2.0134))) - 1 ∧ √(1 / (1 - exp (-√2.0134))) - 1 < 0.149 ∧142    (0.159 : ℝ) < √(1 / (1 - exp (-√1.8533))) - 1 ∧ √(1 / (1 - exp (-√1.8533))) - 1 < 0.160 :=143  FRC.DarkML.wide_binary_band144145/-- 32:P4 — `DarkML.coherence_offset`. -/146theorem coherence_offset :147    (-0.0485 : ℝ) < -Real.log (1 + (1 / 2) ^ 2) / (2 * Real.log 10) ∧ -Real.log (1 + (1 / 2) ^ 2) / (2 * Real.log 10) < -0.0484 ∧148    (-0.1506 : ℝ) < -Real.log (1 + 1 ^ 2) / (2 * Real.log 10) ∧ -Real.log (1 + 1 ^ 2) / (2 * Real.log 10) < -0.1505 :=149  FRC.DarkML.coherence_offset150151/-- 32:C2, 32:X2, 32:X10 — `DarkML.floor_lambda_face`. -/152theorem floor_lambda_face (c lP S : ℝ) (hc : c = 299792458) (hl : lP = 1.616255e-35) (hS : S = 3.3e122) :153    (8.63e-11 : ℝ) < c ^ 2 / (2 * lP * √(π * S)) ∧ c ^ 2 / (2 * lP * √(π * S)) < 8.64e-11 :=154  FRC.DarkML.floor_lambda_face c lP S hc hl hS155156-- Ledger predicates of 32-dark (generated by make_predicates.py from docs/32-dark/32-dark-ledger.json; edit the ledger, not this section)157/-- 32:C2 (p32017) — The acceleration floor $\az=c\Hzero/2\pi$, parameter-free, $13\%$ below the fitted value ($0.7\sigma$ of its systematic band). -/158theorem p32017 : (∀ (c H0 : ℝ), c = (299792458 : ℝ) → H0 = 674e2 / 30856775814913673e6 → 104e-12 < c * H0 / ((2 : ℝ) * Real.pi) ∧ c * H0 / ((2 : ℝ) * Real.pi) < 105e-12 ∧ 0.868 < c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 ∧ c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 < 0.870 ∧ 0.65 < (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 ∧ (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 < 0.67) ∧ ∀ (c lP S : ℝ), c = (299792458 : ℝ) → lP = 1616255e-41 → S = 33e121 → 863e-13 < c ^ (2 : ℕ) / ((2 : ℝ) * lP * √(Real.pi * S)) ∧ c ^ (2 : ℕ) / ((2 : ℝ) * lP * √(Real.pi * S)) < 864e-13 :=159  @FRC.LedgerML.p32017160/-- 32:C4 (p32019) — The deep-regime geometric mean $\geff=\sqrt{\gb\az}$, given the amplitude reading B4; the mean force of the link is Newtonian at every noise level (exactly so in the stationary solution), so the law is registration, not force modification. -/161theorem p32019 : Filter.Tendsto (fun t => t / ((1 : ℝ) - Real.exp (-t))) (nhdsWithin (0 : ℝ) (Set.Ioi (0 : ℝ))) (nhds (1 : ℝ)) ∧ ∀ (f : ℝ → ℝ) (χ : ℝ), (∀ (T : ℝ), f (-T) = -f T) → HasDerivAt f χ (0 : ℝ) → χ ≠ (0 : ℝ) → Filter.Tendsto (fun T => f T / (χ * T)) (nhdsWithin (0 : ℝ) {(0 : ℝ)}ᶜ) (nhds (1 : ℝ)) :=162  @FRC.LedgerML.p32019163/-- 32:C5 (p32020) — Flat rotation curves and the baryonic Tully--Fisher relation $v^4=GM\az$. -/164theorem p32020 : ∀ (t : ℝ), (0 : ℝ) < t → (0 : ℝ) < (1 : ℝ) - Real.exp (-t) ∧ (1 : ℝ) ≤ t / ((1 : ℝ) - Real.exp (-t)) ∧ (t ≤ (1 : ℝ) → t / ((1 : ℝ) - Real.exp (-t)) ≤ (1 : ℝ) / ((1 : ℝ) - (3 : ℝ) * t / (4 : ℝ))) ∧ ∀ (G M r a₀ v : ℝ), (0 : ℝ) < r → (0 : ℝ) ≤ G * M → (0 : ℝ) ≤ a₀ → v ^ (2 : ℕ) = √(G * M / r ^ (2 : ℕ) * a₀) * r → v ^ (4 : ℕ) = G * M * a₀ :=165  @FRC.LedgerML.p32020166/-- 32:C6 (p32021) — The registration theorem: the finite coincidence count, its first-passage law, and flux conservation give the radial acceleration relation given B8; the fitting function of \citet{mcgaugh2016} is this form with $g_\dagger$ for $\az$. -/167theorem p32021 : (∀ (w : ℝ), (0 : ℝ) < w → w < (1 : ℝ) → w * (((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w) ^ (2 : ℕ) - (2 : ℝ) * (((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w) + w = (0 : ℝ) ∧ (0 : ℝ) < ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w ∧ ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w < (1 : ℝ) ∧ (1 : ℝ) < ((1 : ℝ) + √((1 : ℝ) - w ^ (2 : ℕ))) / w ∧ ∀ (x : ℝ), w * x ^ (2 : ℕ) - (2 : ℝ) * x + w = (0 : ℝ) → x = ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w ∨ x = ((1 : ℝ) + √((1 : ℝ) - w ^ (2 : ℕ))) / w) ∧ (∀ (t : ℝ), (0 : ℝ) < t → (0 : ℝ) < (1 : ℝ) - Real.exp (-t) ∧ (1 : ℝ) ≤ t / ((1 : ℝ) - Real.exp (-t)) ∧ (t ≤ (1 : ℝ) → t / ((1 : ℝ) - Real.exp (-t)) ≤ (1 : ℝ) / ((1 : ℝ) - (3 : ℝ) * t / (4 : ℝ))) ∧ ∀ (G M r a₀ v : ℝ), (0 : ℝ) < r → (0 : ℝ) ≤ G * M → (0 : ℝ) ≤ a₀ → v ^ (2 : ℕ) = √(G * M / r ^ (2 : ℕ) * a₀) * r → v ^ (4 : ℕ) = G * M * a₀) ∧ (1.11966 < (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) ∧ (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) < 1.11967 ∧ 1.17082 < (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) ∧ (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) < 1.17083 ∧ 511e-4 < (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) - (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) ∧ (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) - (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) < 512e-4) ∧ ∀ (x gb gobs : ℝ), (0 : ℝ) < x → (0 : ℝ) < (1 : ℝ) - Real.exp (-√x) ∧ (((1 : ℝ) - Real.exp (-√x)) * gobs = gb ↔ gobs = gb / ((1 : ℝ) - Real.exp (-√x))) ∧ Real.sin (Real.arcsin √(Real.exp (-√x))) ^ (2 : ℕ) = Real.exp (-√x) ∧ Real.cos (Real.arcsin √(Real.exp (-√x))) ^ (2 : ℕ) = (1 : ℝ) - Real.exp (-√x) :=168  @FRC.LedgerML.p32021169/-- 32:C7 (p32022) — The finite-cycle first-passage law: $e^{-\sqrt x}$ is carrier-exact (amplitude identity) and the resolvable reading of the exact transform, to $O(\Om^{-1/2})$. -/170theorem p32022 : (∀ (u : ℝ), (1 : ℝ) ≤ u → ((1 : ℝ) - √((1 : ℝ) - ((1 : ℝ) / u) ^ (2 : ℕ))) / ((1 : ℝ) / u) = u - √(u ^ (2 : ℕ) - (1 : ℝ)) ∧ (u - √(u ^ (2 : ℕ) - (1 : ℝ))) * (u + √(u ^ (2 : ℕ) - (1 : ℝ))) = (1 : ℝ) ∧ Real.exp (-Real.log (u + √(u ^ (2 : ℕ) - (1 : ℝ)))) = u - √(u ^ (2 : ℕ) - (1 : ℝ))) ∧ ∀ (s : ℝ), (0 : ℝ) < s → √((2 : ℝ) * s) ≤ Real.log (Real.exp s + √(Real.exp s ^ (2 : ℕ) - (1 : ℝ))) ∧ Real.log (Real.exp s + √(Real.exp s ^ (2 : ℕ) - (1 : ℝ))) ≤ √((2 : ℝ) * s) * Real.exp (s / (2 : ℝ)) :=171  @FRC.LedgerML.p32022172/-- 32:C8 (p32023) — The intrinsic-scatter relation, smallest at high acceleration and rising as $x^{-1/4}$. -/173theorem p32023 : ∀ (x y : ℝ), (0 : ℝ) < x → x < y → (1 : ℝ) / (Real.exp √y - (1 : ℝ)) < (1 : ℝ) / (Real.exp √x - (1 : ℝ)) ∧ (x ≤ (1 : ℝ) → ((1 : ℝ) - √x) / √x ≤ (1 : ℝ) / (Real.exp √x - (1 : ℝ)) ∧ (1 : ℝ) / (Real.exp √x - (1 : ℝ)) < (1 : ℝ) / √x) :=174  @FRC.LedgerML.p32023175/-- 32:C9 (p32024) — The external-field effect from the total-field dependence of the registration. -/176theorem p32024 : (∀ (y₁ y₂ : ℝ), (0 : ℝ) < y₁ → y₁ < y₂ → (1 : ℝ) / ((1 : ℝ) - Real.exp (-√y₂)) < (1 : ℝ) / ((1 : ℝ) - Real.exp (-√y₁))) ∧ ∀ (gin gext : EuclideanSpace ℝ (Fin (3 : ℕ))), ‖gin + gext‖ ≤ ‖gin‖ + ‖gext‖ :=177  @FRC.LedgerML.p32024178set_option linter.defProp false in179/-- 32:C10 (p32050) — The merging-cluster lensing offset onto the coherent component, the enhancement sourced by $\sum_c w_c\Sigma_c$ (B6, B9). -/180def p32050 := @FRC.LedgerML.p32050181/-- 32:C11 (p32026) — The cosmological constant $\Lambda\sim1/\Om$, sign positive, $w=-1$ de Sitter section; no $120$-order cancellation. -/182theorem p32026 : ∀ (r S : ℝ), r ≠ (0 : ℝ) → r ^ (2 : ℕ) = S / Real.pi → (0 : ℝ) < (3 : ℝ) / r ^ (2 : ℕ) ∧ (3 : ℝ) / r ^ (2 : ℕ) * S = (3 : ℝ) * Real.pi :=183  @FRC.LedgerML.p32026184/-- 32:X2 (p32028) — \textbf{The acceleration scale $\az=c\Hzero/2\pi$} is the phase-coherence threshold, the acceleration whose winding frequency reaches the drive's cyclic rate, the $2\pi$ the radian-to-cycle conversion of the angular Hubble rate, parameter-free, $13\%$ below the fitted value at the entailed $\Hzero$. -/185theorem p32028 : (∀ (c H0 : ℝ), c = (299792458 : ℝ) → H0 = 674e2 / 30856775814913673e6 → 104e-12 < c * H0 / ((2 : ℝ) * Real.pi) ∧ c * H0 / ((2 : ℝ) * Real.pi) < 105e-12 ∧ 0.868 < c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 ∧ c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 < 0.870 ∧ 0.65 < (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 ∧ (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 < 0.67) ∧ ∀ (c lP S : ℝ), c = (299792458 : ℝ) → lP = 1616255e-41 → S = 33e121 → 863e-13 < c ^ (2 : ℕ) / ((2 : ℝ) * lP * √(Real.pi * S)) ∧ c ^ (2 : ℕ) / ((2 : ℝ) * lP * √(Real.pi * S)) < 864e-13 :=186  @FRC.LedgerML.p32028187/-- 32:X3 (p32029) — \textbf{Flat rotation curves and the baryonic Tully--Fisher relation} $v^{4}=GM\az$ are the deep-regime geometric mean $\geff=\sqrt{\gb\az}$, the amplitude reading of the field below the floor. -/188theorem p32029 : ∀ (t : ℝ), (0 : ℝ) < t → (0 : ℝ) < (1 : ℝ) - Real.exp (-t) ∧ (1 : ℝ) ≤ t / ((1 : ℝ) - Real.exp (-t)) ∧ (t ≤ (1 : ℝ) → t / ((1 : ℝ) - Real.exp (-t)) ≤ (1 : ℝ) / ((1 : ℝ) - (3 : ℝ) * t / (4 : ℝ))) ∧ ∀ (G M r a₀ v : ℝ), (0 : ℝ) < r → (0 : ℝ) ≤ G * M → (0 : ℝ) ≤ a₀ → v ^ (2 : ℕ) = √(G * M / r ^ (2 : ℕ) * a₀) * r → v ^ (4 : ℕ) = G * M * a₀ :=189  @FRC.LedgerML.p32029190/-- 32:X4 (p32030) — \textbf{The radial acceleration relation carries no fitted function}: its interpolation is the finite first-passage registration given one declared identification, the amplitude barrier (B8), and it is the curve the data selected. -/191theorem p32030 : (∀ (w : ℝ), (0 : ℝ) < w → w < (1 : ℝ) → w * (((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w) ^ (2 : ℕ) - (2 : ℝ) * (((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w) + w = (0 : ℝ) ∧ (0 : ℝ) < ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w ∧ ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w < (1 : ℝ) ∧ (1 : ℝ) < ((1 : ℝ) + √((1 : ℝ) - w ^ (2 : ℕ))) / w ∧ ∀ (x : ℝ), w * x ^ (2 : ℕ) - (2 : ℝ) * x + w = (0 : ℝ) → x = ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w ∨ x = ((1 : ℝ) + √((1 : ℝ) - w ^ (2 : ℕ))) / w) ∧ (1.11966 < (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) ∧ (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) < 1.11967 ∧ 1.17082 < (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) ∧ (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) < 1.17083 ∧ 511e-4 < (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) - (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) ∧ (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) - (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) < 512e-4) ∧ ∀ (x gb gobs : ℝ), (0 : ℝ) < x → (0 : ℝ) < (1 : ℝ) - Real.exp (-√x) ∧ (((1 : ℝ) - Real.exp (-√x)) * gobs = gb ↔ gobs = gb / ((1 : ℝ) - Real.exp (-√x))) ∧ Real.sin (Real.arcsin √(Real.exp (-√x))) ^ (2 : ℕ) = Real.exp (-√x) ∧ Real.cos (Real.arcsin √(Real.exp (-√x))) ^ (2 : ℕ) = (1 : ℝ) - Real.exp (-√x) :=192  @FRC.LedgerML.p32030193/-- 32:X5 (p32031) — \textbf{The relation is tight}, its intrinsic scatter ($0.04$\,dex at the knee, SPARC at fixed $\az$) smallest at high acceleration and rising as $x^{-1/4}$ into the deep regime, the spread of the collective phase. -/194theorem p32031 : ∀ (x y : ℝ), (0 : ℝ) < x → x < y → (1 : ℝ) / (Real.exp √y - (1 : ℝ)) < (1 : ℝ) / (Real.exp √x - (1 : ℝ)) ∧ (x ≤ (1 : ℝ) → ((1 : ℝ) - √x) / √x ≤ (1 : ℝ) / (Real.exp √x - (1 : ℝ)) ∧ (1 : ℝ) / (Real.exp √x - (1 : ℝ)) < (1 : ℝ) / √x) :=195  @FRC.LedgerML.p32031196/-- 32:X6 (p32032) — \textbf{The external-field effect breaks the strong equivalence principle}, the internal dynamics depending on the total field through the registration. -/197theorem p32032 : ∀ (y₁ y₂ : ℝ), (0 : ℝ) < y₁ → y₁ < y₂ → (1 : ℝ) / ((1 : ℝ) - Real.exp (-√y₂)) < (1 : ℝ) / ((1 : ℝ) - Real.exp (-√y₁)) :=198  @FRC.LedgerML.p32032199set_option linter.defProp false in200/-- 32:X7 (p32033) — \textbf{The merging-cluster lensing offset} is a selection: the coherence-weighted enhancement follows the collisionless galaxies and drops the shock-decohered gas ($C_{ij}\to0$), not a coincidence. -/201def p32033 := @FRC.LedgerML.p32033202/-- 32:X8 (p32034) — \textbf{The cluster-core residual} is referred to the coherent amplitude addition $\sqrt{N_{\mathrm{eff}}}$ over the core's separately virialised composites, the one law that also gives the merger selection (C10); the quantitative closure, with $N_{\mathrm{eff}}$ uncomputed, is the conjecture Y1. -/203theorem p32034 : ∀ (n : ℕ) (g : Fin n → ℝ), (∀ (k : Fin n), (0 : ℝ) ≤ g k) → ∑ k, g k ≤ (∑ k, √(g k)) ^ (2 : ℕ) ∧ (∑ k, √(g k)) ^ (2 : ℕ) ≤ ↑n * ∑ k, g k :=204  @FRC.LedgerML.p32034205/-- 32:X9 (p32035) — \textbf{The cosmological constant is small}, $\Lambda\sim1/\Om$, the curvature of the finite chart and a reading of the one cardinality rather than a mode-sum vacuum energy, so no $120$-order cancellation arises. -/206theorem p32035 : ∀ (r S : ℝ), r ≠ (0 : ℝ) → r ^ (2 : ℕ) = S / Real.pi → (0 : ℝ) < (3 : ℝ) / r ^ (2 : ℕ) ∧ (3 : ℝ) / r ^ (2 : ℕ) * S = (3 : ℝ) * Real.pi :=207  @FRC.LedgerML.p32035208/-- 32:X10 (p32036) — \textbf{The dark-matter and dark-energy scales coincide} because both are readings of the one cardinality $\Om$, the floor $\az=c\Hzero/2\pi$ and the curvature $\Lambda\sim1/\Om$ fixed together. -/209theorem p32036 : (∀ (c H0 : ℝ), c = (299792458 : ℝ) → H0 = 674e2 / 30856775814913673e6 → 104e-12 < c * H0 / ((2 : ℝ) * Real.pi) ∧ c * H0 / ((2 : ℝ) * Real.pi) < 105e-12 ∧ 0.868 < c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 ∧ c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 < 0.870 ∧ 0.65 < (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 ∧ (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 < 0.67) ∧ (∀ (c lP S : ℝ), c = (299792458 : ℝ) → lP = 1616255e-41 → S = 33e121 → 863e-13 < c ^ (2 : ℕ) / ((2 : ℝ) * lP * √(Real.pi * S)) ∧ c ^ (2 : ℕ) / ((2 : ℝ) * lP * √(Real.pi * S)) < 864e-13) ∧ ∀ (r S : ℝ), r ≠ (0 : ℝ) → r ^ (2 : ℕ) = S / Real.pi → (0 : ℝ) < (3 : ℝ) / r ^ (2 : ℕ) ∧ (3 : ℝ) / r ^ (2 : ℕ) * S = (3 : ℝ) * Real.pi :=210  @FRC.LedgerML.p32036211/-- 32:X11 (p32037) — \textbf{The dark sector adds no particle}: the registered acceleration is a strictly increasing function of the baryonic acceleration and the one global $\az$, so one registered acceleration fixes one baryonic acceleration with no room for a second component; the galactic discrepancy is the amplitude reading of the baryonic field, the direct-detection and axion nulls are consistent, and no dark subhaloes exist. -/212theorem p32037 : StrictMonoOn (fun x => x / ((1 : ℝ) - Real.exp (-√x))) (Set.Ioi (0 : ℝ)) :=213  @FRC.LedgerML.p32037214/-- 32:P1 (p32038) — The redshift law $\az(z)=cH(z)/2\pi$: the knee shifts and the Tully--Fisher zero-point evolves, $v_{\mathrm{flat}}\propto E(z)^{1/4}$ ($+7\%$, $+16\%$, $+32\%$ at $z=0.5,1,2$ for $\Omega_m=0.315$), parameter-free; shape resolvable, value in Z1. Falsifier: a high-$z$ knee away from $cH(z)/2\pi$, or a non-evolving Tully--Fisher zero-point. -/215theorem p32038 : (∀ (c G M : ℝ) (H a v : ℝ → ℝ) (z : ℝ), (0 : ℝ) < c → (0 : ℝ) < G → (0 : ℝ) < M → (0 : ℝ) < H (0 : ℝ) → (0 : ℝ) < H z → (∀ (z : ℝ), a z = c * H z / ((2 : ℝ) * Real.pi)) → (0 : ℝ) < v (0 : ℝ) → (0 : ℝ) < v z → (∀ (z : ℝ), v z ^ (4 : ℕ) = G * M * a z) → a z / a (0 : ℝ) = H z / H (0 : ℝ) ∧ v z / v (0 : ℝ) = (H z / H (0 : ℝ)) ^ (1 / 4 : ℝ)) ∧ 1.072 < √√√(0.315 * 1.5 ^ (3 : ℕ) + 0.685) ∧ √√√(0.315 * 1.5 ^ (3 : ℕ) + 0.685) < 1.073 ∧ 1.156 < √√√(0.315 * (2 : ℝ) ^ (3 : ℕ) + 0.685) ∧ √√√(0.315 * (2 : ℝ) ^ (3 : ℕ) + 0.685) < 1.158 ∧ 1.319 < √√√(0.315 * (3 : ℝ) ^ (3 : ℕ) + 0.685) ∧ √√√(0.315 * (3 : ℝ) ^ (3 : ℕ) + 0.685) < 1.320 :=216  @FRC.LedgerML.p32038217/-- 32:P2 (p32039) — The scatter is the two-variable form $\sigma=(2\tan\alpha/\ln10)\,\delta\alpha$, vanishing for cold high-$x$ systems and rising as $x^{-1/4}$; SPARC at fixed $\az$: intrinsic $0.038$\,dex overall, $0.04$ at the knee, $0.13$ at $x\simeq0.02$, bounding $\delta\alpha\lesssim3.5^{\circ}$. Falsifier: a deep-regime intrinsic scatter that does not rise, or a measured collective spread the scatter does not track. -/218theorem p32039 : ∀ (x y : ℝ), (0 : ℝ) < x → x < y → (1 : ℝ) / (Real.exp √y - (1 : ℝ)) < (1 : ℝ) / (Real.exp √x - (1 : ℝ)) ∧ (x ≤ (1 : ℝ) → ((1 : ℝ) - √x) / √x ≤ (1 : ℝ) / (Real.exp √x - (1 : ℝ)) ∧ (1 : ℝ) / (Real.exp √x - (1 : ℝ)) < (1 : ℝ) / √x) :=219  @FRC.LedgerML.p32039220/-- 32:P3 (p32040) — Wide binaries ($\gtrsim10$\,kAU) follow $\gb/(1-e^{-\sqrt{x}})$ with the global $\az$ and the vector Galactic field $\gext\simeq1.8\az$: a $10$--$30\%$ velocity enhancement ($12$--$16\%$ at $10$--$40$\,kAU on the collinear estimate), the exponential knee distinct from Newtonian and rational forms. Falsifier: Newtonian wide-binary motion, or a knee of the wrong shape. -/221theorem p32040 : 0.115 < √((1 : ℝ) / ((1 : ℝ) - Real.exp (-√2.6535))) - (1 : ℝ) ∧ √((1 : ℝ) / ((1 : ℝ) - Real.exp (-√2.6535))) - (1 : ℝ) < 0.116 ∧ 0.148 < √((1 : ℝ) / ((1 : ℝ) - Real.exp (-√2.0134))) - (1 : ℝ) ∧ √((1 : ℝ) / ((1 : ℝ) - Real.exp (-√2.0134))) - (1 : ℝ) < 0.149 ∧ 0.159 < √((1 : ℝ) / ((1 : ℝ) - Real.exp (-√1.8533))) - (1 : ℝ) ∧ √((1 : ℝ) / ((1 : ℝ) - Real.exp (-√1.8533))) - (1 : ℝ) < 0.160 :=222  @FRC.LedgerML.p32040223/-- 32:P4 (p32041) — Pressure-supported systems (ellipticals, dSphs, UDGs) lie below the cold-disk relation by the coherence factor $\sqrt{w}$, $w=1/(1+(\sigma_v/v)^{2})$, by $0.05$--$0.15$\,dex for $\sigma_v/v=0.5$--$1$, correlating with $\sigma_v/v$. Falsifier: pressure-supported systems on the cold-disk relation. -/224theorem p32041 : -485e-4 < -Real.log ((1 : ℝ) + (1 / 2 : ℝ) ^ (2 : ℕ)) / ((2 : ℝ) * Real.log (10 : ℝ)) ∧ -Real.log ((1 : ℝ) + (1 / 2 : ℝ) ^ (2 : ℕ)) / ((2 : ℝ) * Real.log (10 : ℝ)) < -484e-4 ∧ -0.1506 < -Real.log ((1 : ℝ) + (1 : ℝ) ^ (2 : ℕ)) / ((2 : ℝ) * Real.log (10 : ℝ)) ∧ -Real.log ((1 : ℝ) + (1 : ℝ) ^ (2 : ℕ)) / ((2 : ℝ) * Real.log (10 : ℝ)) < -0.1505 :=225  @FRC.LedgerML.p32041226/-- 32:P6 (p32043) — A global, isotropic scale and no dark substructure: the registered acceleration depends on the baryonic field and the one global $\az$ alone, strictly increasing, with no direction or environment in the law once the external field is in its argument; no new dark-matter state and no dark subhaloes, so stream perturbations and the satellite abundance trace baryons alone. Falsifier: a directional or density dependence of $\az$ beyond the external-field effect, or stream gaps and substructure lensing with no baryonic counterpart. -/227theorem p32043 : StrictMonoOn (fun x => x / ((1 : ℝ) - Real.exp (-√x))) (Set.Ioi (0 : ℝ)) :=228  @FRC.LedgerML.p32043229-- end ledger predicates230231end FRC.Dark232