The core module lean/FrcCore/Keys/Dark.lean — the substrate from first principles, no Mathlib, no axioms (the modules in order: Nat, Pigeonhole, Shell, Series, Cycle, Ring, FrameCore, Frame, Parity, Transform, Orbit, Sum, Theme/Projective, Theme/Fourier, Theme/Fractional, Theme/Lifts, Theme/Dichotomy, Theme/Rotations, Theme/Heisenberg, Theme/Spectra, Theme/Exclusivity, Theme/Quadratic, Theme/Extension, Theme/Tally, Theme/Numbers, Theme/Logic, Theme/SecondOrder, Theme/Formation, Theme/Field, Theme/Foundation, Theme/Drive, Theme/Carrier, Theme/Subject, Theme/Pair, Theme/Hopf, Theme/Symbol, Theme/Gravity, Theme/Quantum, Theme/Unitary, Theme/Interactions, Theme/Fields, Theme/Horizon, Theme/Zeros, Theme/Shift, Theme/Lattice, Theme/Drift, Theme/Observation, Theme/Interference, Theme/Composite, Theme/Ladder, Theme/Flavour, Theme/Dark, Meridian, Fourier, Algebra, Epi, Dimensions, Poly, Quaternion, Causality, Representation, Reductio, Godel, Finitism, Geometry, Complex, Instances, Rh, Entropy, Dirac, Gravity, S13, Fields, Qm, Pnp, Flavour, Dark, Keys/Frame, Keys/Extension, Keys/Projective, Keys/Fourier, Keys/Numbers, Keys/Logic, Keys/Foundation, Keys/Carrier, Keys/Subject, Keys/Gravity, Keys/Quantum, Keys/Interactions, Keys/Horizon, Keys/Flavour, Keys/Dark, Theme/Hadrons, Hadrons, Keys/Hadrons): 13 theorems (0 definitions): 13 with no axioms, 0 at tier 1 (propext, Quot.sound), 0 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (green, the core; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import FrcCore.Transform2import FrcCore.Theme.Drift3import FrcCore.Theme.Dark45/-!6# FrcCore.Keys.Dark — the keyed theorems of the dark theme (ledger migration, task LM19)78One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem9that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration10`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).11-/1213namespace FRC.Ledger1415-- Keys of the dark theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)16/-- p32016 — 32:C1. Newton's inverse-square law from the discrete Gauss law of the synchronisation flux. -/17
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 :=18 And.intro @FRC.Drift.gauss_law (And.intro @FRC.Dark.enclosed_flux (And.intro @FRC.Dark.source_free_flux (@FRC.Dark.flux_superposition)))19/-- p32018 — 32:C3. Amplitude is the square root of the count (exact in $\Z[i]$, by cross-term cancellation). -/20theorem 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 :=21 And.intro @FRC.Dark.parallelogram (And.intro @FRC.Dark.coherent_stack (@FRC.Dark.incoherent_mean))22/-- 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. -/23theorem 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 :=24 And.intro @FRC.Dark.tully_fisher (And.intro @FRC.Dark.source_free_flux (@FRC.Drift.gauss_law))25/-- p32020 — 32:C5. Flat rotation curves and the baryonic Tully--Fisher relation $v^4=GM\az$. -/26theorem 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 :=27 @FRC.Dark.tully_fisher28/-- 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$. -/29theorem 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)) :=30 And.intro @FRC.Dark.passage_vieta (@FRC.Dark.line_passage)31/-- 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})$. -/32theorem 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) :=33 And.intro @FRC.Dark.passage_step (And.intro @FRC.Dark.line_passage (And.intro @FRC.Dark.cycle_passage (@FRC.Dark.passage_vieta)))34/-- 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. -/35theorem 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 :=36 And.intro @FRC.Drift.gauss_law (And.intro @FRC.Dark.enclosed_flux (And.intro @FRC.Dark.source_free_flux (@FRC.Dark.flux_superposition)))37/-- 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. -/38theorem 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 :=39 @FRC.Dark.tully_fisher40/-- 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. -/41theorem 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)) :=42 And.intro @FRC.Dark.passage_vieta (@FRC.Dark.line_passage)43/-- 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. -/44theorem 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)) :=45 And.intro @FRC.Drift.locked_sum (And.intro @FRC.Shell.Frame.geom_sum_eq_zero (@FRC.Dark.cohsum_three))46/-- 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. -/47theorem 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 :=48 And.intro @FRC.Dark.cohsum_three (@FRC.Dark.neff_equal)49/-- 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. -/50theorem 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 :=51 And.intro @FRC.Dark.cohsum_three (@FRC.Drift.locked_sum)52/-- p32050 — 32:C10. The merging-cluster lensing offset onto the coherent component, the enhancement sourced by $\sum_c w_c\Sigma_c$ (B6, B9). -/53theorem 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 :=54 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)))55-- end keys5657end FRC.Ledger58