The core module lean/FrcCore/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.Theme.Dark2import FrcCore.Theme.Drift3import FrcCore.Transform4import FrcCore.Keys.Dark56/-!7# FrcCore.Dark — 32-dark's paper module (18 October 2026)89The predicate declarations of *The Dark Sector over Finite Relational Substrate* (32-dark), `FRC.Dark.p32NNN`, one per10witnessed row, each the conjunction of the theorems its ledger row cites: the dark theme's `Theme/Dark.lean` (the11first-passage recursion and its two-image solution, Vieta, the Tully–Fisher identity, the parallelogram law and the12incoherent mean, the coherence sums, the enclosed flux), the gravity theme's Gauss law and locked sum, and the frame13theme's vanishing cycle sum. The declarations are generated by `lean/make_predicates.py` from the paper's ledger; the14theorems live in the theme files.15-/1617namespace FRC.Dark1819-- Ledger predicates of 32-dark (generated by make_predicates.py from docs/32-dark/32-dark-ledger.json; edit the ledger, not this section)20/-- 32:C1 (p32016) — Newton's inverse-square law from the discrete Gauss law of the synchronisation flux. -/21
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 :=22 @FRC.Ledger.p3201623/-- 32:C3 (p32018) — Amplitude is the square root of the count (exact in $\Z[i]$, by cross-term cancellation). -/24theorem 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 :=25 @FRC.Ledger.p3201826/-- 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. -/27theorem 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 :=28 @FRC.Ledger.p3201929/-- 32:C5 (p32020) — Flat rotation curves and the baryonic Tully--Fisher relation $v^4=GM\az$. -/30theorem 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 :=31 @FRC.Ledger.p3202032/-- 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$. -/33theorem 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)) :=34 @FRC.Ledger.p3202135/-- 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})$. -/36theorem 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) :=37 @FRC.Ledger.p3202238/-- 32:C10 (p32050) — The merging-cluster lensing offset onto the coherent component, the enhancement sourced by $\sum_c w_c\Sigma_c$ (B6, B9). -/39theorem 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 :=40 @FRC.Ledger.p3205041/-- 32:X1 (p32027) — \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. -/42theorem 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 :=43 @FRC.Ledger.p3202744/-- 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. -/45theorem 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 :=46 @FRC.Ledger.p3202947/-- 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. -/48theorem 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)) :=49 @FRC.Ledger.p3203050/-- 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. -/51theorem 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)) :=52 @FRC.Ledger.p3203353/-- 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. -/54theorem 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 :=55 @FRC.Ledger.p3203456/-- 32:P5 (p32042) — 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. -/57theorem 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 :=58 @FRC.Ledger.p3204259-- end ledger predicates6061end FRC.Dark62