import FrcCore.Transform
import FrcCore.Theme.Drift
import FrcCore.Theme.Dark

/-!
# FrcCore.Keys.Dark — the keyed theorems of the dark theme (ledger migration, task LM19)

One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem
that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration
`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).
-/

namespace FRC.Ledger

-- Keys of the dark theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)
/-- p32016 — 32:C1. Newton's inverse-square law from the discrete Gauss law of the synchronisation flux. -/
theorem p32016 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) (J : Nat → Nat → FRC.Shell p), (∀ (x y : Nat), J x y = -J y x) → ∀ (R : Nat → Bool), FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => J x y) n) n = FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * J x y) n) n) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) (J : Nat → Nat → FRC.Shell p), (∀ (x y : Nat), J x y = -J y x) → ∀ (R : Nat → Bool) (src : Nat → FRC.Shell p), (∀ (x : Nat), FRC.Shell.sumRange (fun y => J x y) n = src x) → FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * J x y) n) n = FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * src x) n) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) (J : Nat → Nat → FRC.Shell p), (∀ (x y : Nat), J x y = -J y x) → ∀ (R : Nat → Bool), (∀ (x : Nat), FRC.Shell.sumRange (fun y => J x y) n = (0 : FRC.Shell p)) → FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * J x y) n) n = (0 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] (n : Nat) (J K : Nat → Nat → FRC.Shell p) (R : Nat → Bool), FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * (J x y + K x y)) n) n = FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * J x y) n) n + FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * K x y) n) n :=
  And.intro @FRC.Drift.gauss_law (And.intro @FRC.Dark.enclosed_flux (And.intro @FRC.Dark.source_free_flux (@FRC.Dark.flux_superposition)))
/-- p32018 — 32:C3. Amplitude is the square root of the count (exact in $\Z[i]$, by cross-term cancellation). -/
theorem p32018 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b : FRC.Extension.Ext p ν), (a + b).norm + (a + -b).norm = a.norm + a.norm + (b.norm + b.norm)) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (u : FRC.Extension.Ext p ν) (n : Nat), (FRC.Extension.Ext.ofShell (FRC.Shell.ofNat n) * u).norm = FRC.Shell.ofNat n * FRC.Shell.ofNat n * u.norm) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (us : List (FRC.Extension.Ext p ν)), FRC.Dark.tot (0 : FRC.Extension.Ext p ν) us = FRC.Shell.ofNat ((2 : Nat) ^ us.length) * FRC.Dark.normSum us :=
  And.intro @FRC.Dark.parallelogram (And.intro @FRC.Dark.coherent_stack (@FRC.Dark.incoherent_mean))
/-- p32019 — 32:C4. 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. -/
theorem p32019 : (∀ {p : Nat} [FRC.Pos p] (G M a r v s : FRC.Shell p), s * s + -(G * M * a) = (0 : FRC.Shell p) → v * v + -s = (0 : FRC.Shell p) → v * v * v * v = G * M * a) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) (J : Nat → Nat → FRC.Shell p), (∀ (x y : Nat), J x y = -J y x) → ∀ (R : Nat → Bool), (∀ (x : Nat), FRC.Shell.sumRange (fun y => J x y) n = (0 : FRC.Shell p)) → FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * J x y) n) n = (0 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) (J : Nat → Nat → FRC.Shell p), (∀ (x y : Nat), J x y = -J y x) → ∀ (R : Nat → Bool), FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => J x y) n) n = FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * J x y) n) n :=
  And.intro @FRC.Dark.tully_fisher (And.intro @FRC.Dark.source_free_flux (@FRC.Drift.gauss_law))
/-- p32020 — 32:C5. Flat rotation curves and the baryonic Tully--Fisher relation $v^4=GM\az$. -/
theorem p32020 : ∀ {p : Nat} [FRC.Pos p] (G M a r v s : FRC.Shell p), s * s + -(G * M * a) = (0 : FRC.Shell p) → v * v + -s = (0 : FRC.Shell p) → v * v * v * v = G * M * a :=
  @FRC.Dark.tully_fisher
/-- p32021 — 32:C6. 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$. -/
theorem p32021 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g0 : FRC.Shell p}, FRC.Shell.Frame p κ g0 → ∀ (z f g : FRC.Shell p), z ≠ (0 : FRC.Shell p) → f + -g ≠ (0 : FRC.Shell p) → z * (f * f + (1 : FRC.Shell p)) + -(f + f) = (0 : FRC.Shell p) → z * (g * g + (1 : FRC.Shell p)) + -(g + g) = (0 : FRC.Shell p) → z * (f + g) + -((1 : FRC.Shell p) + (1 : FRC.Shell p)) = (0 : FRC.Shell p) ∧ f * g = (1 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] (z f : FRC.Shell p), z * (f * f + (1 : FRC.Shell p)) + -(f + f) = (0 : FRC.Shell p) → ∀ (k : Nat), z * (f ^ k + f ^ (k + (2 : Nat))) = f ^ (k + (1 : Nat)) + f ^ (k + (1 : Nat)) :=
  And.intro @FRC.Dark.passage_vieta (@FRC.Dark.line_passage)
/-- p32022 — 32:C7. 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})$. -/
theorem p32022 : (∀ {p : Nat} [FRC.Pos p] (z f t : FRC.Shell p), z * (f * f + (1 : FRC.Shell p)) + -(f + f) = (0 : FRC.Shell p) → z * (t + t * f * f) = t * f + t * f) ∧ (∀ {p : Nat} [FRC.Pos p] (z f : FRC.Shell p), z * (f * f + (1 : FRC.Shell p)) + -(f + f) = (0 : FRC.Shell p) → ∀ (k : Nat), z * (f ^ k + f ^ (k + (2 : Nat))) = f ^ (k + (1 : Nat)) + f ^ (k + (1 : Nat))) ∧ (∀ {p : Nat} [FRC.Pos p] (z f : FRC.Shell p), z * (f * f + (1 : FRC.Shell p)) + -(f + f) = (0 : FRC.Shell p) → ∀ (k j : Nat), z * (f ^ k + f ^ (j + (2 : Nat)) + (f ^ (k + (2 : Nat)) + f ^ j)) = f ^ (k + (1 : Nat)) + f ^ (j + (1 : Nat)) + (f ^ (k + (1 : Nat)) + f ^ (j + (1 : Nat)))) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g0 : FRC.Shell p}, FRC.Shell.Frame p κ g0 → ∀ (z f g : FRC.Shell p), z ≠ (0 : FRC.Shell p) → f + -g ≠ (0 : FRC.Shell p) → z * (f * f + (1 : FRC.Shell p)) + -(f + f) = (0 : FRC.Shell p) → z * (g * g + (1 : FRC.Shell p)) + -(g + g) = (0 : FRC.Shell p) → z * (f + g) + -((1 : FRC.Shell p) + (1 : FRC.Shell p)) = (0 : FRC.Shell p) ∧ f * g = (1 : FRC.Shell p) :=
  And.intro @FRC.Dark.passage_step (And.intro @FRC.Dark.line_passage (And.intro @FRC.Dark.cycle_passage (@FRC.Dark.passage_vieta)))
/-- p32027 — 32:X1. \textbf{Newton's inverse-square law and the equivalence principle} follow from the discrete Gauss law of the synchronisation flux, the acceleration of a test cluster independent of its mass and composition. -/
theorem p32027 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) (J : Nat → Nat → FRC.Shell p), (∀ (x y : Nat), J x y = -J y x) → ∀ (R : Nat → Bool), FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => J x y) n) n = FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * J x y) n) n) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) (J : Nat → Nat → FRC.Shell p), (∀ (x y : Nat), J x y = -J y x) → ∀ (R : Nat → Bool) (src : Nat → FRC.Shell p), (∀ (x : Nat), FRC.Shell.sumRange (fun y => J x y) n = src x) → FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * J x y) n) n = FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * src x) n) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) (J : Nat → Nat → FRC.Shell p), (∀ (x y : Nat), J x y = -J y x) → ∀ (R : Nat → Bool), (∀ (x : Nat), FRC.Shell.sumRange (fun y => J x y) n = (0 : FRC.Shell p)) → FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * J x y) n) n = (0 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] (n : Nat) (J K : Nat → Nat → FRC.Shell p) (R : Nat → Bool), FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * (J x y + K x y)) n) n = FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * J x y) n) n + FRC.Shell.sumRange (fun x => FRC.Drift.ind R x * FRC.Shell.sumRange (fun y => ((1 : FRC.Shell p) + -FRC.Drift.ind R y) * K x y) n) n :=
  And.intro @FRC.Drift.gauss_law (And.intro @FRC.Dark.enclosed_flux (And.intro @FRC.Dark.source_free_flux (@FRC.Dark.flux_superposition)))
/-- p32029 — 32:X3. \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. -/
theorem p32029 : ∀ {p : Nat} [FRC.Pos p] (G M a r v s : FRC.Shell p), s * s + -(G * M * a) = (0 : FRC.Shell p) → v * v + -s = (0 : FRC.Shell p) → v * v * v * v = G * M * a :=
  @FRC.Dark.tully_fisher
/-- p32030 — 32:X4. \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. -/
theorem p32030 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g0 : FRC.Shell p}, FRC.Shell.Frame p κ g0 → ∀ (z f g : FRC.Shell p), z ≠ (0 : FRC.Shell p) → f + -g ≠ (0 : FRC.Shell p) → z * (f * f + (1 : FRC.Shell p)) + -(f + f) = (0 : FRC.Shell p) → z * (g * g + (1 : FRC.Shell p)) + -(g + g) = (0 : FRC.Shell p) → z * (f + g) + -((1 : FRC.Shell p) + (1 : FRC.Shell p)) = (0 : FRC.Shell p) ∧ f * g = (1 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] (z f : FRC.Shell p), z * (f * f + (1 : FRC.Shell p)) + -(f + f) = (0 : FRC.Shell p) → ∀ (k : Nat), z * (f ^ k + f ^ (k + (2 : Nat))) = f ^ (k + (1 : Nat)) + f ^ (k + (1 : Nat)) :=
  And.intro @FRC.Dark.passage_vieta (@FRC.Dark.line_passage)
/-- p32033 — 32:X7. \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. -/
theorem p32033 : (∀ {p : Nat} [FRC.Pos p] (z : FRC.Shell p) (m : Nat), FRC.Shell.sumRange (fun x => z) m = FRC.Shell.ofNat m * z) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {x : FRC.Shell p} (n : Nat), x ^ n = (1 : FRC.Shell p) → x ≠ (1 : FRC.Shell p) → FRC.Shell.sumRange (fun l => x ^ l) n = (0 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] (s1 s2 s3 : FRC.Shell p), (s1 + s2 + s3) * (s1 + s2 + s3) = s1 * s1 + s2 * s2 + s3 * s3 + (s1 * s2 + s1 * s2 + (s1 * s3 + s1 * s3) + (s2 * s3 + s2 * s3)) :=
  And.intro @FRC.Drift.locked_sum (And.intro @FRC.Shell.Frame.geom_sum_eq_zero (@FRC.Dark.cohsum_three))
/-- p32034 — 32:X8. \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. -/
theorem p32034 : (∀ {p : Nat} [FRC.Pos p] (s1 s2 s3 : FRC.Shell p), (s1 + s2 + s3) * (s1 + s2 + s3) = s1 * s1 + s2 * s2 + s3 * s3 + (s1 * s2 + s1 * s2 + (s1 * s3 + s1 * s3) + (s2 * s3 + s2 * s3))) ∧ ∀ {p : Nat} [FRC.Pos p] (s : FRC.Shell p) (N : Nat), FRC.Shell.sumRange (fun x => s) N * FRC.Shell.sumRange (fun x => s) N = FRC.Shell.ofNat N * FRC.Shell.sumRange (fun x => s * s) N :=
  And.intro @FRC.Dark.cohsum_three (@FRC.Dark.neff_equal)
/-- p32042 — 32:P5. Coherence-state cluster gas: the X-ray gas gravitates only when bulk-coherent, contributing in a relaxed cluster ($C_{ij}\to1$) and dropping out of a merger ($C_{ij}\to0$), the lensing displacement growing with the shock Mach number; the quantitative core residual of the same law is the conjecture Y1. Falsifier: a merger lensing peak tracking the shocked gas, or no relaxed-versus-merging difference. -/
theorem p32042 : (∀ {p : Nat} [FRC.Pos p] (s1 s2 s3 : FRC.Shell p), (s1 + s2 + s3) * (s1 + s2 + s3) = s1 * s1 + s2 * s2 + s3 * s3 + (s1 * s2 + s1 * s2 + (s1 * s3 + s1 * s3) + (s2 * s3 + s2 * s3))) ∧ ∀ {p : Nat} [FRC.Pos p] (z : FRC.Shell p) (m : Nat), FRC.Shell.sumRange (fun x => z) m = FRC.Shell.ofNat m * z :=
  And.intro @FRC.Dark.cohsum_three (@FRC.Drift.locked_sum)
/-- p32050 — 32:C10. The merging-cluster lensing offset onto the coherent component, the enhancement sourced by $\sum_c w_c\Sigma_c$ (B6, B9). -/
theorem p32050 : (∀ {p : Nat} [FRC.Pos p] (z : FRC.Shell p) (m : Nat), FRC.Shell.sumRange (fun x => z) m = FRC.Shell.ofNat m * z) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {x : FRC.Shell p} (n : Nat), x ^ n = (1 : FRC.Shell p) → x ≠ (1 : FRC.Shell p) → FRC.Shell.sumRange (fun l => x ^ l) n = (0 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] (s1 s2 s3 : FRC.Shell p), (s1 + s2 + s3) * (s1 + s2 + s3) = s1 * s1 + s2 * s2 + s3 * s3 + (s1 * s2 + s1 * s2 + (s1 * s3 + s1 * s3) + (s2 * s3 + s2 * s3))) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (u : FRC.Extension.Ext p ν) (n : Nat), (FRC.Extension.Ext.ofShell (FRC.Shell.ofNat n) * u).norm = FRC.Shell.ofNat n * FRC.Shell.ofNat n * u.norm :=
  And.intro @FRC.Drift.locked_sum (And.intro @FRC.Shell.Frame.geom_sum_eq_zero (And.intro @FRC.Dark.cohsum_three (@FRC.Dark.coherent_stack)))
-- end keys

end FRC.Ledger