The core module lean/FrcCore/Theme/Loss.lean — the substrate from first principles, no Mathlib, no axioms; one of the core's 137 modules (the index); it rests on 2 modules: Nat, Pigeonhole: 10 theorems (4 definitions): 10 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.Pigeonhole23/-!4# The loss file of 8-dirac — a self-map of a finite set is bijective exactly when its image count is the whole count56The seventh file of the dirac theme (5 November 2026, the core-proof programme): 8:E2 on the register `[0, n)` with the7base theme's lists (`Pigeonhole.mem`, `NoDup`, `erase`). The image count of `f : [0, n) → [0, n)` is the number of values8below `n` that `f` hits; it is `n` exactly when `f` is injective and surjective — the loss factor (the count over the image9count) is one. The surjective direction counts the hit values; injectivity follows from surjectivity by the pigeonhole in10the form "a list holding every number below `m` has at least `m` entries": with a collision `f i = f j`, `i ≠ j`, the11values of `f` on the `n − 1` indices other than `j` still cover `[0, n)`. No axioms.12-/1314namespace FRC.Dirac.Loss1516open FRC.Pigeonhole1718/-- The register `[0, n)` as a list, `n − 1, …, 0`. -/19
def ran : Nat → List Nat20 | 0 => []21 | n + 1 => n :: ran n2223
theorem mem_ran : ∀ n v, mem v (ran n) ↔ v < n24 | 0, v => ⟨fun h => absurd h id, fun h => absurd h (Nat.not_lt_zero v)⟩25 | n + 1, v => by26 show v = n ∨ mem v (ran n) ↔ v < n + 127 constructor28 · intro h29 cases h with30 | inl e => exact e ▸ Nat.lt_succ_self n31 | inr h' => exact Nat.lt_succ_of_lt ((mem_ran n v).1 h')32 · intro h33 cases Nat.lt_or_ge v n with34 | inl hlt => exact Or.inr ((mem_ran n v).2 hlt)35 | inr hge => exact Or.inl (Nat.le_antisymm (Nat.le_of_lt_succ h) hge)3637theorem length_ran : ∀ n, (ran n).length = n38 | 0 => rfl39 | n + 1 => by show (ran n).length + 1 = n + 1; rw [length_ran n]4041theorem mem_map (f : Nat → Nat) (v : Nat) : ∀ l : List Nat, mem v (List.map f l) ↔ ∃ i, mem i l ∧ f i = v42 | [] => ⟨fun h => absurd h id, fun ⟨_, h, _⟩ => absurd h id⟩43 | a :: l => by44 show v = f a ∨ mem v (List.map f l) ↔ ∃ i, (i = a ∨ mem i l) ∧ f i = v45 constructor46 · intro h47 cases h with48 | inl e => exact ⟨a, Or.inl rfl, e.symm⟩49 | inr h' =>50 obtain ⟨i, hi, e⟩ := (mem_map f v l).1 h'51 exact ⟨i, Or.inr hi, e⟩52 · intro ⟨i, hi, e⟩53 cases hi with54 | inl e' => exact Or.inl (by rw [← e, e'])55 | inr hi' => exact Or.inr ((mem_map f v l).2 ⟨i, hi', e⟩)5657theorem length_map (f : Nat → Nat) : ∀ l : List Nat, (List.map f l).length = l.length58 | [] => rfl59 | _ :: l => by show (List.map f l).length + 1 = l.length + 1; rw [length_map f l]6061/-- A list holding every number below `m` has at least `m` entries (erase `m − 1` and recurse). -/62theorem length_ge_of_contains : ∀ (m : Nat) (l : List Nat), (∀ v, v < m → mem v l) → m ≤ l.length63 | 0, _, _ => Nat.zero_le _64 | m + 1, l, h => by65 have hm : mem m l := h m (Nat.lt_succ_self m)66 have h' : ∀ v, v < m → mem v (erase m l) := fun v hv =>67 mem_erase_of_ne (Nat.ne_of_lt hv) (h v (Nat.lt_succ_of_lt hv))68 have := length_ge_of_contains m (erase m l) h'69 rw [← length_erase_of_mem hm]70 exact Nat.succ_le_succ this7172/-- The number of values below `n` satisfying `A`. -/73def cnt (A : Nat → Bool) : Nat → Nat74 | 0 => 075 | n + 1 => cnt A n + if A n then 1 else 07677theorem cnt_full (A : Nat → Bool) : ∀ n, (∀ v, v < n → A v = true) → cnt A n = n78 | 0, _ => rfl79 | n + 1, h => by80 show cnt A n + (if A n then 1 else 0) = n + 181 rw [cnt_full A n fun v hv => h v (Nat.lt_succ_of_lt hv), h n (Nat.lt_succ_self n)]82 rfl8384theorem cnt_le (A : Nat → Bool) : ∀ n, cnt A n ≤ n85 | 0 => Nat.le_refl 086 | n + 1 => by87 show cnt A n + (if A n then 1 else 0) ≤ n + 188 cases A n with89 | true => exact Nat.succ_le_succ (cnt_le A n)90 | false => exact Nat.le_succ_of_le (cnt_le A n)9192/-- A value below `n` missed by `A` keeps the count below `n`. -/93theorem cnt_lt_of_false (A : Nat → Bool) : ∀ n v, v < n → A v = false → cnt A n < n94 | 0, _, hv, _ => absurd hv (Nat.not_lt_zero _)95 | n + 1, v, hv, hA => by96 show cnt A n + (if A n then 1 else 0) < n + 197 cases Nat.lt_or_ge v n with98 | inl hlt =>99 have := cnt_lt_of_false A n v hlt hA100 cases A n with101 | true => exact Nat.succ_lt_succ this102 | false => exact Nat.lt_succ_of_lt this103 | inr hge =>104 have e : v = n := Nat.le_antisymm (Nat.le_of_lt_succ hv) hge105 rw [← e, hA]106 exact Nat.lt_succ_of_le (cnt_le A v)107108/-- `v` is a value of `f` on `[0, n)`. -/109def hit (f : Nat → Nat) (n v : Nat) : Bool := decide (mem v (List.map f (ran n)))110111/-- The image count of `f` on `[0, n)`: the number of values below `n` that `f` takes. -/112def imageCount (f : Nat → Nat) (n : Nat) : Nat := cnt (hit f n) n113114theorem hit_iff (f : Nat → Nat) (n v : Nat) : hit f n v = true ↔ ∃ i, i < n ∧ f i = v := by115 constructor116 · intro h117 obtain ⟨i, hi, e⟩ := (mem_map f v _).1 (of_decide_eq_true h)118 exact ⟨i, (mem_ran n i).1 hi, e⟩119 · intro ⟨i, hi, e⟩120 exact decide_eq_true ((mem_map f v _).2 ⟨i, (mem_ran n i).2 hi, e⟩)121122/-- 8:E2 — a self-map of `[0, n)` is bijective exactly when its image count is `n` (the loss factor, the count over123the image count, is one): surjectivity is the count of the hit values, and injectivity follows from surjectivity by124the pigeonhole — with a collision `f i = f j`, `i ≠ j`, the `n − 1` values of `f` off `j` would still cover `[0, n)`. -/125theorem bijective_iff_image_count (f : Nat → Nat) (n : Nat) :126 imageCount f n = n ↔127 ((∀ i j, i < n → j < n → f i = f j → i = j) ∧ (∀ v, v < n → ∃ i, i < n ∧ f i = v)) := by128 constructor129 · intro hc130 have hsurj : ∀ v, v < n → ∃ i, i < n ∧ f i = v := by131 intro v hv132 apply (hit_iff f n v).1133 cases e : hit f n v with134 | true => rfl135 | false => exact absurd hc (Nat.ne_of_lt (cnt_lt_of_false (hit f n) n v hv e))136 refine ⟨?_, hsurj⟩137 intro i j hi hj e138 cases Nat.decEq i j with139 | isTrue h => exact h140 | isFalse h =>141 -- the values of `f` on the indices other than `j` still cover `[0, n)`, on `n − 1` indices142 have hj' : mem j (ran n) := (mem_ran n j).2 hj143 have hcover : ∀ v, v < n → mem v (List.map f (erase j (ran n))) := by144 intro v hv145 obtain ⟨k, hk, ek⟩ := hsurj v hv146 apply (mem_map f v _).2147 cases Nat.decEq k j with148 | isFalse hkj => exact ⟨k, mem_erase_of_ne hkj ((mem_ran n k).2 hk), ek⟩149 | isTrue hkj => exact ⟨i, mem_erase_of_ne h ((mem_ran n i).2 hi), by rw [e, ← hkj, ek]⟩150 have hlen := length_ge_of_contains n _ hcover151 rw [length_map] at hlen152 have hlen' : n + 1 ≤ (erase j (ran n)).length + 1 := Nat.succ_le_succ hlen153 rw [length_erase_of_mem hj', length_ran] at hlen'154 exact absurd hlen' (Nat.not_succ_le_self n)155 · intro ⟨_, hsurj⟩156 exact cnt_full _ n fun v hv => (hit_iff f n v).2 (hsurj v hv)157158end FRC.Dirac.Loss159