The core module lean/FrcCore/Theme/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): 16 theorems (2 definitions): 16 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.Drift23/-!4# FrcCore.Theme.Dark — the dark theme: 32-dark's exact content (18 October 2026)56The dark sector of *The Dark Sector over Finite Relational Substrate* (32-dark), on the gravity theme's Gauss law7(`FRC.Drift.gauss_law`, 00:E3) and locked sum, the frame theme's vanishing cycle sum and the extension norm of8`Theme/Quadratic`. Every statement is on a shell `Shell p` or its quadratic extension `Ext p ν`; every proof is the9kernel's (`decide +kernel` through the normaliser `RE.sound`, with explicit cofactors for the identities that hold10modulo a hypothesis) or a structural induction, and no axiom enters.1112* **The first-passage law (32:C7, B8, C6, X4).** With `z(f² + 1) = 2f` (the single-step generating factor of the13 first-passage quadratic), the sequence `u_k = f^k` satisfies the walk's recursion `z(u_{k−1} + u_{k+1}) = 2u_k` at14 every step (`passage_step`, `line_passage`), and so does the two-image sum `f^{·} + f^{N−·}` on the cycle `Z_N`15 (`cycle_passage`): divided by `1 + f^N` it is the exact escape transform with the absorbing point at distance16 `a` one way and `N − a` the other, the second image the wrap correction. Two distinct roots of the quadratic have17 `z(f + g) = 2` and `fg = 1` (`passage_vieta`): the second root is `1/f`, the long route round the cycle.18* **The deep regime (32:C4, C5, X3).** `s² = GMa₀` and `v² = s` give `v⁴ = GMa₀` (`tully_fisher`): the baryonic19 Tully–Fisher relation as a ring identity of the amplitude reading.20* **The amplitude identity (32:C3).** `N(a + b) + N(a − b) = 2N(a) + 2N(b)` (`parallelogram`); `n` copies of one21 phasor have norm `n² N(u)` (`coherent_stack`); the norms of the `2^n` signed sums add up to `2^n Σ N(u_k)`22 (`tot_eq`, `incoherent_mean`), so the mean squared amplitude of an incoherent ensemble of unit phasors is `n`, its23 amplitude `√n`.24* **The coherence sums (32:C10, X7, X8, P5, B9).** `(s₁ + s₂ + s₃)² = Σ s_i² + 2Σ_{i<j} s_i s_j` (`cohsum_three`), the25 amplitude law at `C_ij = 1`; `N` equal components give `(Σ s)² = N Σ s²` (`neff_equal`), `N_eff = N`.26* **The enclosed flux (32:C1, X1, C4).** For antisymmetric link currents with divergence `src`, the flux through a27 region's boundary is the enclosed source (`enclosed_flux`); a source-free current has zero flux (`source_free_flux`);28 fluxes superpose (`flux_superposition`). A unit source gives unit flux through every enclosing surface, and the29 floor noise, source-free, leaves the mean force unchanged.30-/3132namespace FRC.Dark33open FRC.Shell FRC.Shell.Frame FRC.Extension FRC.Extension.Ext FRC.Drift3435variable {p : Nat} [Pos p] {ν : Shell p}3637/-- An identity modulo one hypothesis: from `L = R + A·X` and `A = 0`, `L = R`. -/38
theorem red1 {L R A X : Shell p} (e : L = R + A * X) (ha : A = 0) : L = R := by39 rw [e, ha, zero_mul, add_zero]4041/-- An identity modulo two hypotheses. -/42theorem red2 {L R A B X Y : Shell p} (e : L = R + A * X + B * Y) (ha : A = 0) (hb : B = 0) : L = R := by43 rw [e, ha, hb, zero_mul, zero_mul, add_zero, add_zero]4445/-! ## The first-passage law on the cycle (32:C7, B8) -/4647/-- 32:C7, 32:B8 — one step of the killed walk's recursion: if `z(f² + 1) = 2f` (the single-step generating factor `f` of the48first-passage quadratic `(z/2)f² − f + z/2 = 0`), then for every `t` (standing for `f^k`) `z(t + t f²) = 2 t f`:49the sequence `u_k = f^k` satisfies `z(u_{k−1} + u_{k+1}) = 2u_k`. -/50theorem passage_step (z f t : Shell p) (h : z * (f * f + 1) + -(f + f) = 0) :51 z * (t + t * f * f) = t * f + t * f :=52 red1 (RE.sound (look [z, f, t]) (.mul (.var 0) (.add (.var 2) (.mul (.mul (.var 2) (.var 1)) (.var 1)))) (.add (.add (.mul (.var 2) (.var 1)) (.mul (.var 2) (.var 1))) (.mul (.add (.mul (.var 0) (.add (.mul (.var 1) (.var 1)) .one)) (.neg (.add (.var 1) (.var 1)))) (.var 2))) (by decide +kernel) : z * (t + t * f * f) = t * f + t * f + (z * (f * f + 1) + -(f + f)) * t) h5354/-- 32:C7, 32:C6, 32:X4 — the line solution: `u_k = f^k` solves the recursion at every interior step, `z(f^k + f^{k+2}) = 2 f^{k+1}`. -/55theorem line_passage (z f : Shell p) (h : z * (f * f + 1) + -(f + f) = 0) (k : Nat) :56 z * (f ^ k + f ^ (k + 2)) = f ^ (k + 1) + f ^ (k + 1) := by57 have e2 : f ^ (k + 2) = f ^ k * f * f := by rw [pow_succ, pow_succ]58 have e1 : f ^ (k + 1) = f ^ k * f := pow_succ f k59 rw [e2, e1]; exact passage_step z f (f ^ k) h6061/-- 32:C7, 32:B8 — the two-image solution on the cycle `Z_N` with the absorbing point at distance `k+1` one way and `j+1` the62other (`N = k + j + 2`): `u = f^{·} + f^{N−·}` satisfies the same recursion, `z(u_{k} + u_{k+2}) = 2u_{k+1}`, written63with the two exponents `k, j`; the normalisation by `1 + f^N` makes the absorbing value one. -/64theorem cycle_passage (z f : Shell p) (h : z * (f * f + 1) + -(f + f) = 0) (k j : Nat) :65 z * ((f ^ k + f ^ (j + 2)) + (f ^ (k + 2) + f ^ j)) =66 (f ^ (k + 1) + f ^ (j + 1)) + (f ^ (k + 1) + f ^ (j + 1)) := by67 have hk := line_passage z f h k68 have hj := line_passage z f h j69 have e : (f ^ k + f ^ (j + 2)) + (f ^ (k + 2) + f ^ j) = (f ^ k + f ^ (k + 2)) + (f ^ j + f ^ (j + 2)) := by70 rw [add_add_add_comm, add_comm (f ^ (j + 2)) (f ^ j)]71 rw [e, left_distrib, hk, hj, add_add_add_comm]7273/-- 32:C6, 32:X4, 32:C7 — Vieta for the first-passage quadratic: two distinct roots `f ≠ g` of `z(x² + 1) = 2x` have `z(f + g) = 2` and74`f g = 1` (`z ≠ 0`): the second root is `1/f`, the long route round the cycle. -/75theorem passage_vieta {κ : Nat} {g0 : Shell p} (F : Frame p κ g0) (z f g : Shell p) (hz : z ≠ 0) (hfg : f + -g ≠ 0)76 (h1 : z * (f * f + 1) + -(f + f) = 0) (h2 : z * (g * g + 1) + -(g + g) = 0) :77 z * (f + g) + -(1 + 1) = 0 ∧ f * g = 1 := by78 have s : z * ((f + g) * (f + -g)) = f + -g + (f + -g) :=79 red2 (RE.sound (look [z, f, g]) (.mul (.var 0) (.mul (.add (.var 1) (.var 2)) (.add (.var 1) (.neg (.var 2))))) (.add (.add (.add (.add (.var 1) (.neg (.var 2))) (.add (.var 1) (.neg (.var 2)))) (.mul (.add (.mul (.var 0) (.add (.mul (.var 1) (.var 1)) .one)) (.neg (.add (.var 1) (.var 1)))) .one)) (.mul (.add (.mul (.var 0) (.add (.mul (.var 2) (.var 2)) .one)) (.neg (.add (.var 2) (.var 2)))) (.neg .one))) (by decide +kernel) : z * ((f + g) * (f + -g)) = f + -g + (f + -g) + (z * (f * f + 1) + -(f + f)) * 1 + (z * (g * g + 1) + -(g + g)) * (-1)) h1 h280 -- (z(f+g) − 2)(f − g) = 0, so z(f+g) = 281 have s' : (z * (f + g) + -(1 + 1)) * (f + -g) = 0 := by82 have : (z * (f + g) + -(1 + 1)) * (f + -g) = z * ((f + g) * (f + -g)) + -(f + -g + (f + -g)) :=83 RE.sound (look [z, f, g]) (.mul (.add (.mul (.var 0) (.add (.var 1) (.var 2))) (.neg (.add .one .one))) (.add (.var 1) (.neg (.var 2)))) (.add (.mul (.var 0) (.mul (.add (.var 1) (.var 2)) (.add (.var 1) (.neg (.var 2))))) (.neg (.add (.add (.var 1) (.neg (.var 2))) (.add (.var 1) (.neg (.var 2)))))) (by decide +kernel)84 rw [this, s, add_neg]85 have h3 : z * (f + g) + -(1 + 1) = 0 := by86 rcases F.mul_eq_zero s' with h | h87 · exact h88 · exact absurd h hfg89 refine ⟨h3, ?_⟩90 have pz : z * (1 + -(f * g)) = 0 :=91 red2 (RE.sound (look [z, f, g]) (.mul (.var 0) (.add .one (.neg (.mul (.var 1) (.var 2))))) (.add (.add .zero (.mul (.add (.mul (.var 0) (.add (.mul (.var 1) (.var 1)) .one)) (.neg (.add (.var 1) (.var 1)))) .one)) (.mul (.add (.mul (.var 0) (.add (.var 1) (.var 2))) (.neg (.add .one .one))) (.neg (.var 1)))) (by decide +kernel) : z * (1 + -(f * g)) = 0 + (z * (f * f + 1) + -(f + f)) * 1 + (z * (f + g) + -(1 + 1)) * (-f)) h1 h392 rcases F.mul_eq_zero pz with h | h93 · exact absurd h hz94 · -- 1 + -(f g) = 0, so f g = 195 have e1 : (1 : Shell p) = f * g := by96 have := eq_neg_of_add_eq_zero h97 rw [this, neg_neg]98 exact e1.symm99100/-! ## The deep regime and Tully–Fisher (32:C4, C5, X3) -/101102/-- 32:C4, 32:C5, 32:X3 — the amplitude reading squared is the flux: with `s² = G M a₀` (the deep-regime registered force times `r`) and103`v² = s` (the circular speed, `v² = g r` with `g = s/r`), `v⁴ = G M a₀` — the baryonic Tully–Fisher relation as a104ring identity. -/105theorem tully_fisher (G M a r v s : Shell p) (hs : s * s + -(G * M * a) = 0) (hv : v * v + -s = 0) :106 v * v * v * v = G * M * a :=107 red2 (RE.sound (look [G, M, a, r, v, s]) (.mul (.mul (.mul (.var 4) (.var 4)) (.var 4)) (.var 4)) (.add (.add (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.mul (.add (.mul (.var 5) (.var 5)) (.neg (.mul (.mul (.var 0) (.var 1)) (.var 2)))) .one)) (.mul (.add (.mul (.var 4) (.var 4)) (.neg (.var 5))) (.add (.mul (.var 4) (.var 4)) (.var 5)))) (by decide +kernel) : v * v * v * v = G * M * a + (s * s + -(G * M * a)) * 1 + (v * v + -s) * (v * v + s)) hs hv108109/-! ## The amplitude identity (32:C3) -/110111/-- 32:C3 — the parallelogram law of the extension norm: `N(a + b) + N(a − b) = 2N(a) + 2N(b)` — the cross terms of two112phasors cancel between the two signs. -/113theorem parallelogram (a b : Ext p ν) :114 norm (a + b) + norm (a + -b) = (norm a + norm a) + (norm b + norm b) := by115 show (a.re + b.re) * (a.re + b.re) + -(ν * ((a.im + b.im) * (a.im + b.im))) + ((a.re + -b.re) * (a.re + -b.re) + -(ν * ((a.im + -b.im) * (a.im + -b.im)))) = a.re * a.re + -(ν * (a.im * a.im)) + (a.re * a.re + -(ν * (a.im * a.im))) + (b.re * b.re + -(ν * (b.im * b.im)) + (b.re * b.re + -(ν * (b.im * b.im))))116 exact RE.sound (look [a.re, a.im, b.re, b.im, ν]) (.add (.add (.mul (.add (.var 0) (.var 2)) (.add (.var 0) (.var 2))) (.neg (.mul (.var 4) (.mul (.add (.var 1) (.var 3)) (.add (.var 1) (.var 3)))))) (.add (.mul (.add (.var 0) (.neg (.var 2))) (.add (.var 0) (.neg (.var 2)))) (.neg (.mul (.var 4) (.mul (.add (.var 1) (.neg (.var 3))) (.add (.var 1) (.neg (.var 3)))))))) (.add (.add (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 1) (.var 1))))) (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 1) (.var 1)))))) (.add (.add (.mul (.var 2) (.var 2)) (.neg (.mul (.var 4) (.mul (.var 3) (.var 3))))) (.add (.mul (.var 2) (.var 2)) (.neg (.mul (.var 4) (.mul (.var 3) (.var 3))))))) (by decide +kernel)117118/-- 32:C3, 32:C10 — the coherent stack: `n` copies of one phasor have norm `n²N(u)` (`norm_scale` with `c = ofNat n`). -/119theorem coherent_stack (u : Ext p ν) (n : Nat) : norm (ofShell (ofNat n) * u) = ofNat n * ofNat n * norm u :=120 norm_scale (ofNat n) u121122/-- 32:C3 — the sum over all sign patterns of the norm of the signed sum: `tot acc us` branches on the sign of each phasor,123`tot acc [] = N(acc)`, `tot acc (u :: us) = tot (acc + u) us + tot (acc − u) us`, so `tot 0 us` is `Σ_ε N(Σ ε_k u_k)`124over the `2^n` patterns. -/125
def tot (acc : Ext p ν) : List (Ext p ν) → Shell p126 | [] => norm acc127 | u :: us => tot (acc + u) us + tot (acc + -u) us128129/-- 32:C3 — the sum of the norms of the phasors. -/130def normSum : List (Ext p ν) → Shell p131 | [] => 0132 | u :: us => norm u + normSum us133134/-- 32:C3 — the pattern sum from any starting phasor: `tot acc us = 2^n (N(acc) + Σ N(u_k))`. -/135theorem tot_eq (us : List (Ext p ν)) : ∀ acc : Ext p ν, tot acc us = ofNat (2 ^ us.length) * (norm acc + normSum us) := by136 induction us with137 | nil =>138 intro acc139 show norm acc = ofNat 1 * (norm acc + 0)140 rw [add_zero, show (ofNat 1 : Shell p) = 1 from rfl, FRC.Shell.one_mul]141 | cons u us ih =>142 intro acc143 show tot (acc + u) us + tot (acc + -u) us = ofNat (2 ^ (us.length + 1)) * (norm acc + (norm u + normSum us))144 rw [ih (acc + u), ih (acc + -u)]145 have h2 : (ofNat (2 ^ (us.length + 1)) : Shell p) = ofNat (2 ^ us.length) + ofNat (2 ^ us.length) := by146 rw [Nat.pow_succ, Nat.mul_two, ← ofNat_add]147 rw [h2]148 have par := parallelogram acc u149 -- 2^n (N(acc+u) + S) + 2^n (N(acc−u) + S) = (2^n + 2^n)(N(acc) + N(u) + S), given the parallelogram law150 have e : ∀ c A B S Na Nu : Shell p, A + B = (Na + Na) + (Nu + Nu) →151 c * (A + S) + c * (B + S) = (c + c) * (Na + (Nu + S)) := by152 intro c A B S Na Nu hAB153 rw [← left_distrib]154 have : A + S + (B + S) = (A + B) + (S + S) := add_add_add_comm A S B S155 rw [this, hAB]156 exact RE.sound (look [c, S, Na, Nu]) (.mul (.var 0) (.add (.add (.add (.var 2) (.var 2)) (.add (.var 3) (.var 3))) (.add (.var 1) (.var 1)))) (.mul (.add (.var 0) (.var 0)) (.add (.var 2) (.add (.var 3) (.var 1)))) (by decide +kernel)157 exact e _ _ _ _ _ _ par158159/-- 32:C3 — the incoherent mean: the norms of the `2^n` signed sums add up to `2^n` times the sum of the norms, so160the mean squared amplitude of an incoherent ensemble is `Σ N(u_k)` (the count `n` for unit phasors), its amplitude161`√n`, while the coherent stack has `n²`. -/162theorem incoherent_mean (us : List (Ext p ν)) : tot 0 us = ofNat (2 ^ us.length) * normSum us := by163 rw [tot_eq us 0]164 have h0 : norm (0 : Ext p ν) = 0 := by165 show (0 : Shell p) * 0 + -(ν * (0 * 0)) = 0166 rw [mul_zero, mul_zero, neg_zero, add_zero]167 rw [h0, zero_add]168169/-! ## The coherence sums (32:C10, X8, P5, B9) -/170171/-- 32:C10, 32:X7, 32:X8, 32:P5 — three mutually coherent components add as amplitudes: `(s₁ + s₂ + s₃)² = Σ s_i² + 2Σ_{i<j} s_i s_j`, the law172`g²_amp/a₀ = Σ g_i + 2Σ_{i<j} √(g_i g_j) Re C_ij` at `C_ij = 1`; at `C_ij = 0` only `Σ g_i` remains. -/173theorem cohsum_three (s1 s2 s3 : Shell p) :174 (s1 + s2 + s3) * (s1 + s2 + s3) = s1 * s1 + s2 * s2 + s3 * s3 + (s1 * s2 + s1 * s2 + (s1 * s3 + s1 * s3) + (s2 * s3 + s2 * s3)) :=175 RE.sound (look [s1, s2, s3]) (.mul (.add (.add (.var 0) (.var 1)) (.var 2)) (.add (.add (.var 0) (.var 1)) (.var 2))) (.add (.add (.add (.mul (.var 0) (.var 0)) (.mul (.var 1) (.var 1))) (.mul (.var 2) (.var 2))) (.add (.add (.add (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1))) (.add (.mul (.var 0) (.var 2)) (.mul (.var 0) (.var 2)))) (.add (.mul (.var 1) (.var 2)) (.mul (.var 1) (.var 2))))) (by decide +kernel)176177/-- 32:X8 — `N` equal coherent components: `(Σ√g)² = N² g = N · Σ g`, so `N_eff = N` (the coherent core's `√N_eff` boost). -/178theorem neff_equal (s : Shell p) (N : Nat) : sumRange (fun _ => s) N * sumRange (fun _ => s) N = ofNat N * sumRange (fun _ => s * s) N := by179 rw [locked_sum, locked_sum]180 exact RE.sound (look [ofNat N, s]) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1))) (.mul (.var 0) (.mul (.var 0) (.mul (.var 1) (.var 1)))) (by decide +kernel)181182/-! ## The enclosed flux (32:C1, X1, C4) -/183184/-- 32:C1, 32:X1, 32:C4 — the flux through the boundary of a region equals the source it encloses: for antisymmetric link currents with185divergence `src`, `Σ_{x∈R} Σ_{y∉R} J_xy = Σ_{x∈R} src x` (the Gauss law). A unit source inside gives unit flux186through every enclosing surface. -/187theorem enclosed_flux {κ : Nat} {g : Shell p} (F : Frame p κ g) (n : Nat) (J : Nat → Nat → Shell p)188 (hJ : ∀ x y, J x y = -(J y x)) (R : Nat → Bool) (src : Nat → Shell p)189 (hdiv : ∀ x, sumRange (fun y => J x y) n = src x) :190 sumRange (fun x => ind R x * sumRange (fun y => (1 + -(ind R y)) * J x y) n) n = sumRange (fun x => ind R x * src x) n := by191 rw [← gauss_law F n J hJ R]192 exact sum_congr n (fun x _ => by rw [hdiv x])193194/-- 32:C1, 32:X1, 32:C4 — a source-free current has zero flux through every closed surface: the floor noise, zero-mean and source-free,195leaves the mean force unchanged. -/196theorem source_free_flux {κ : Nat} {g : Shell p} (F : Frame p κ g) (n : Nat) (J : Nat → Nat → Shell p)197 (hJ : ∀ x y, J x y = -(J y x)) (R : Nat → Bool) (hdiv : ∀ x, sumRange (fun y => J x y) n = 0) :198 sumRange (fun x => ind R x * sumRange (fun y => (1 + -(ind R y)) * J x y) n) n = 0 := by199 rw [enclosed_flux F n J hJ R (fun _ => 0) hdiv]200 exact sum_zero n (fun x _ => mul_zero _)201202/-- 32:C1, 32:X1 — superposition: the flux of `J + K` is the sum of the fluxes — a source-free perturbation adds nothing. -/203theorem flux_superposition (n : Nat) (J K : Nat → Nat → Shell p) (R : Nat → Bool) :204 sumRange (fun x => ind R x * sumRange (fun y => (1 + -(ind R y)) * (J x y + K x y)) n) n =205 sumRange (fun x => ind R x * sumRange (fun y => (1 + -(ind R y)) * J x y) n) n +206 sumRange (fun x => ind R x * sumRange (fun y => (1 + -(ind R y)) * K x y) n) n := by207 rw [← sum_add]208 exact sum_congr n (fun x _ => by209 rw [← left_distrib, ← sum_add]210 congr 1211 exact sum_congr n (fun y _ => by rw [left_distrib]))212213end FRC.Dark214