Theme/Hopf.lean — FrcCore

1import FrcCore.Theme.Field2import FrcCore.Theme.Projective34/-! # The Hopf section and the frame triple on every prime shell (38:A9, 12 October 2026)5`Theme/Projective.lean` proves them from the field laws (`Frame.Fld`), `Theme/Field.lean` proves the laws from primality;6this file joins the two (Theorem *The two fibrations and the frame triple*, "for every odd prime `p` of the totality";7the master's C22 states it on `p = 4κ + 1`). The subject theme's third core file; it imports neither `Subject.lean` nor8`Pair.lean`, so its closure stays small. -/910namespace FRC11namespace Shell1213variable {p : Nat} [Pos p]1415namespace Frame1617/-- 38:A7 — the quaternion map is a bijection of `𝔽_p⁴` onto `M₂` on a field shell with `r² = −1` and `2h = 1`, the inverse18`M ↦ ((a + d) h, (a − d)(−r) h, (b − c) h, (b + c)(−r) h)`: with `sphere_det`, the norm-one sphere is the whole of `SL₂`. -/19theorem quat_bijective (K : Fld p) {r h : Shell p} (hr : r * r = -1) (h2 : (1 + 1) * h = 1) :20    (∀ M : M2 p, quat r ((M.a + M.d) * h) ((M.a + -M.d) * (-r * h)) ((M.b + -M.c) * h) ((M.b + M.c) * (-r * h)) = M) ∧21    (∀ x y z w x' y' z' w' : Shell p, quat r x y z w = quat r x' y' z' w' → x = x' ∧ y = y' ∧ z = z' ∧ w = w') := by22  have ca : ∀ a d : Shell p, (a + d) * h + r * ((a + -d) * (-r * h)) = a := fun a d => by23    have e1 : (a + d) * h + r * ((a + -d) * (-r * h)) = (a + d) * h + -(r * r) * ((a + -d) * h) := Shell.Frame.RE.sound (Shell.Frame.look [a, d, h, r]) (.add (.mul (.add (.var 0) (.var 1)) (.var 2)) (.mul (.var 3) (.mul (.add (.var 0) (.neg (.var 1))) (.mul (.neg (.var 3)) (.var 2))))) (.add (.mul (.add (.var 0) (.var 1)) (.var 2)) (.mul (.neg (.mul (.var 3) (.var 3))) (.mul (.add (.var 0) (.neg (.var 1))) (.var 2)))) (by decide +kernel)24    have e2 : (a + d) * h + (a + -d) * h = a * ((1 + 1) * h) := Shell.Frame.RE.sound (Shell.Frame.look [a, d, h]) (.add (.mul (.add (.var 0) (.var 1)) (.var 2)) (.mul (.add (.var 0) (.neg (.var 1))) (.var 2))) (.mul (.var 0) (.mul (.add .one .one) (.var 2))) (by decide +kernel)25    rw [e1, hr, neg_neg, one_mul, e2, h2, mul_one]26  have cd : ∀ a d : Shell p, (a + d) * h + -(r * ((a + -d) * (-r * h))) = d := fun a d => by27    have e1 : (a + d) * h + -(r * ((a + -d) * (-r * h))) = (a + d) * h + -(-(r * r) * ((a + -d) * h)) := Shell.Frame.RE.sound (Shell.Frame.look [a, d, h, r]) (.add (.mul (.add (.var 0) (.var 1)) (.var 2)) (.neg (.mul (.var 3) (.mul (.add (.var 0) (.neg (.var 1))) (.mul (.neg (.var 3)) (.var 2)))))) (.add (.mul (.add (.var 0) (.var 1)) (.var 2)) (.neg (.mul (.neg (.mul (.var 3) (.var 3))) (.mul (.add (.var 0) (.neg (.var 1))) (.var 2))))) (by decide +kernel)28    have e2 : (a + d) * h + -((a + -d) * h) = d * ((1 + 1) * h) := Shell.Frame.RE.sound (Shell.Frame.look [a, d, h]) (.add (.mul (.add (.var 0) (.var 1)) (.var 2)) (.neg (.mul (.add (.var 0) (.neg (.var 1))) (.var 2)))) (.mul (.var 1) (.mul (.add .one .one) (.var 2))) (by decide +kernel)29    rw [e1, hr, neg_neg, one_mul, e2, h2, mul_one]30  have cb : ∀ b c : Shell p, (b + -c) * h + r * ((b + c) * (-r * h)) = b := fun b c => by31    have e1 : (b + -c) * h + r * ((b + c) * (-r * h)) = (b + -c) * h + -(r * r) * ((b + c) * h) := Shell.Frame.RE.sound (Shell.Frame.look [b, c, h, r]) (.add (.mul (.add (.var 0) (.neg (.var 1))) (.var 2)) (.mul (.var 3) (.mul (.add (.var 0) (.var 1)) (.mul (.neg (.var 3)) (.var 2))))) (.add (.mul (.add (.var 0) (.neg (.var 1))) (.var 2)) (.mul (.neg (.mul (.var 3) (.var 3))) (.mul (.add (.var 0) (.var 1)) (.var 2)))) (by decide +kernel)32    have e2 : (b + -c) * h + (b + c) * h = b * ((1 + 1) * h) := Shell.Frame.RE.sound (Shell.Frame.look [b, c, h]) (.add (.mul (.add (.var 0) (.neg (.var 1))) (.var 2)) (.mul (.add (.var 0) (.var 1)) (.var 2))) (.mul (.var 0) (.mul (.add .one .one) (.var 2))) (by decide +kernel)33    rw [e1, hr, neg_neg, one_mul, e2, h2, mul_one]34  have cc : ∀ b c : Shell p, -((b + -c) * h) + r * ((b + c) * (-r * h)) = c := fun b c => by35    have e1 : -((b + -c) * h) + r * ((b + c) * (-r * h)) = -((b + -c) * h) + -(r * r) * ((b + c) * h) := Shell.Frame.RE.sound (Shell.Frame.look [b, c, h, r]) (.add (.neg (.mul (.add (.var 0) (.neg (.var 1))) (.var 2))) (.mul (.var 3) (.mul (.add (.var 0) (.var 1)) (.mul (.neg (.var 3)) (.var 2))))) (.add (.neg (.mul (.add (.var 0) (.neg (.var 1))) (.var 2))) (.mul (.neg (.mul (.var 3) (.var 3))) (.mul (.add (.var 0) (.var 1)) (.var 2)))) (by decide +kernel)36    have e2 : -((b + -c) * h) + (b + c) * h = c * ((1 + 1) * h) := Shell.Frame.RE.sound (Shell.Frame.look [b, c, h]) (.add (.neg (.mul (.add (.var 0) (.neg (.var 1))) (.var 2))) (.mul (.add (.var 0) (.var 1)) (.var 2))) (.mul (.var 1) (.mul (.add .one .one) (.var 2))) (by decide +kernel)37    rw [e1, hr, neg_neg, one_mul, e2, h2, mul_one]38  have h2ne : (1 + 1 : Shell p) ≠ 0 := fun h0 => K.one_ne_zero (by rw [← h2, h0, zero_mul])39  have hrne : r ≠ 0 := fun h0 => K.one_ne_zero (by40    have := hr; rw [h0, zero_mul] at this; rw [← neg_neg (1 : Shell p), ← this, neg_zero])41  have ex : ∀ x y : Shell p, (1 + 1) * x = (x + r * y) + (x + -(r * y)) := fun x y => Shell.Frame.RE.sound (Shell.Frame.look [x, y, r]) (.mul (.add .one .one) (.var 0)) (.add (.add (.var 0) (.mul (.var 2) (.var 1))) (.add (.var 0) (.neg (.mul (.var 2) (.var 1))))) (by decide +kernel)42  have ey : ∀ x y : Shell p, (1 + 1) * (r * y) = (x + r * y) + -(x + -(r * y)) := fun x y => Shell.Frame.RE.sound (Shell.Frame.look [x, y, r]) (.mul (.add .one .one) (.mul (.var 2) (.var 1))) (.add (.add (.var 0) (.mul (.var 2) (.var 1))) (.neg (.add (.var 0) (.neg (.mul (.var 2) (.var 1)))))) (by decide +kernel)43  have ew : ∀ z w : Shell p, (1 + 1) * (r * w) = (z + r * w) + (-z + r * w) := fun z w => Shell.Frame.RE.sound (Shell.Frame.look [z, w, r]) (.mul (.add .one .one) (.mul (.var 2) (.var 1))) (.add (.add (.var 0) (.mul (.var 2) (.var 1))) (.add (.neg (.var 0)) (.mul (.var 2) (.var 1)))) (by decide +kernel)44  have ez : ∀ z w : Shell p, (1 + 1) * z = (z + r * w) + -(-z + r * w) := fun z w => Shell.Frame.RE.sound (Shell.Frame.look [z, w, r]) (.mul (.add .one .one) (.var 0)) (.add (.add (.var 0) (.mul (.var 2) (.var 1))) (.neg (.add (.neg (.var 0)) (.mul (.var 2) (.var 1))))) (by decide +kernel)45  refine ⟨fun M => M2.ext' (ca M.a M.d) (cb M.b M.c) (cc M.b M.c) (cd M.a M.d), fun x y z w x' y' z' w' e => ?_⟩46  have ha : x + r * y = x' + r * y' := M2.ext'_a e47  have hb : z + r * w = z' + r * w' := M2.ext'_b e48  have hc : -z + r * w = -z' + r * w' := M2.ext'_c e49  have hd : x + -(r * y) = x' + -(r * y') := M2.ext'_d e50  refine ⟨K.mul_left_cancel h2ne (by rw [ex x y, ex x' y', ha, hd]),51    K.mul_left_cancel hrne (K.mul_left_cancel h2ne (by rw [ey x y, ey x' y', ha, hd])),52    K.mul_left_cancel h2ne (by rw [ez z w, ez z' w', hb, hc]),53    K.mul_left_cancel hrne (K.mul_left_cancel h2ne (by rw [ew z w, ew z' w', hb, hc]))⟩5455end Frame5657namespace Prime5859open Frame6061/-- Every nonzero residue of a prime shell has an inverse: `x · x^(p − 2) = x^(p − 1) = 1` (Fermat). -/62theorem exists_inv (hp : FRC.Nat.isPrime p) {x : Shell p} (hx : x ≠ 0) : ∃ y, x * y = 1 := by63  refine ⟨x ^ (p - 2), ?_⟩64  have e : p - 1 = (p - 2) + 1 := by65    have h2 : 2 ≤ p := two_le hp66    have : p = (p - 2) + 2 := (FRC.Nat.sub_add_cancel h2).symm67    rw [this, FRC.Nat.add_sub_cancel]; rfl68  rw [mul_comm, ← pow_succ, ← e]; exact fermat hp hx6970/-- A prime shell has the field laws (`Theme/Field.lean`'s lemmas and `exists_inv`). -/71theorem fld (hp : FRC.Nat.isPrime p) : Frame.Fld p :=72  ⟨one_ne_zero hp, fun hx => exists_inv hp hx, fun h => mul_eq_zero hp h, fun ha hb => mul_ne_zero hp ha hb,73   fun ha h => mul_left_cancel hp ha h, fun h => sq_eq_one hp h⟩7475/-- 38:A9 — the Hopf section on every prime shell (`Fld.hopf_section` under primality, `ν` any nonsquare; on `𝔽₂` no76nonsquare exists, and the rows quantify over the odd primes). -/77theorem hopf_section (hp : FRC.Nat.isPrime p) {ν : Shell p} (hν : ¬ ∃ y : Shell p, y * y = ν) :78    (∀ α β x y : Shell p, β ≠ 0 → (x ≠ 0 ∨ y ≠ 0) → ¬ PEq ((boost ν α β).act x y) (x, y)) ∧79    (∀ α β a b e l : Shell p, boost ν α β = M2.smul l (borel a b e) → β = 0) ∧80    (∀ M : M2 p, M.det ≠ 0 → ∃ N a b e α β : Shell p, N ≠ 0 ∧ a * e ≠ 0 ∧ (α ≠ 0 ∨ β ≠ 0) ∧81      M2.smul N M = (borel a b e).mul (boost ν α β)) ∧82    (∀ l a1 b1 e1 α1 β1 a2 b2 e2 α2 β2 : Shell p, l ≠ 0 → e2 ≠ 0 → (α1 ≠ 0 ∨ β1 ≠ 0) →83      M2.smul l ((borel a1 b1 e1).mul (boost ν α1 β1)) = (borel a2 b2 e2).mul (boost ν α2 β2) →84      α1 * β2 = α2 * β1 ∧ e2 * a1 = e1 * a2 ∧ e2 * b1 = e1 * b2) ∧85    (∀ α β α' β' : Shell p, (α ≠ 0 ∨ β ≠ 0) → (α' ≠ 0 ∨ β' ≠ 0) →86      ((∃ μ : Shell p, μ ≠ 0 ∧ boost ν α' β' = M2.smul μ (boost ν α β)) ↔ α * β' = α' * β)) ∧87    natCount (fun _ => True) p * natCount (fun b => b ≠ 0) p = p * (p - 1) ∧88    (boost ν (-1) 0 = borel (-1) 0 (-1) ∧ (-1 : Shell p) * -1 + -(ν * (0 * 0)) = 1 ∧ (-1 : Shell p) * -1 = 1 ∧89      (∀ α β a b e : Shell p, boost ν α β = borel a b e → α * α + -(ν * (β * β)) = 1 → β = 0 ∧ (α = 1 ∨ α = -1)) ∧90      ∀ M N : M2 p, (M2.smul (-1) M).mul (M2.smul (-1) N) = M.mul N) :=91  (fld hp).hopf_section hν9293/-- 38:A9 — the frame counts on every prime shell: `Fld.hopf_counts` under primality. -/94theorem hopf_counts (hp : FRC.Nat.isPrime p) (ν : Shell p) :95    (∀ a b e : Shell p, a * e ≠ 0 → ∃ i j : Nat, i < p ∧ j < p ∧ i ≠ 0 ∧96      ∃ l : Shell p, l ≠ 0 ∧ M2.smul l (borel a b e) = borel (ofNat i) (ofNat j) 1) ∧97    (∀ i j i' j' : Nat, i < p → j < p → i' < p → j' < p → ∀ l : Shell p,98      M2.smul l (borel (ofNat i) (ofNat j) 1) = borel (ofNat i') (ofNat j') 1 → i = i' ∧ j = j') ∧99    natCount (fun _ => True) p * natCount (fun b => b ≠ 0) p = p * (p - 1) ∧100    (∀ α β : Shell p, (α ≠ 0 ∨ β ≠ 0) →101      (∃ i : Nat, i < p ∧ ∃ μ : Shell p, μ ≠ 0 ∧ M2.smul μ (boost ν α β) = boost ν (ofNat i) 1) ∨102      (∃ μ : Shell p, μ ≠ 0 ∧ M2.smul μ (boost ν α β) = boost ν 1 0)) ∧103    (∀ i i' : Nat, i < p → i' < p → ∀ μ : Shell p, M2.smul μ (boost ν (ofNat i) 1) = boost ν (ofNat i') 1 → i = i') ∧104    (∀ i : Nat, ∀ μ : Shell p, μ ≠ 0 → M2.smul μ (boost ν (ofNat i) 1) ≠ boost ν 1 0) ∧105    (∀ i : Nat, ∀ μ : Shell p, M2.smul μ (boost ν 1 0) ≠ boost ν (ofNat i) 1) ∧106    natCount (fun _ => True) p + 1 = p + 1 :=107  (fld hp).hopf_counts ν108109/-- 38:A9 — the frame triple on every prime shell (`Fld.frame_triple` under primality). -/110theorem frame_triple (hp : FRC.Nat.isPrime p) {ν : Shell p} (hν : ¬ ∃ y : Shell p, y * y = ν) :111    (∀ M : M2 p, M.det ≠ 0 → (M.a ≠ 0 ∨ M.c ≠ 0) ∧ M.act 1 0 = (M.a, M.c) ∧ (boost ν M.a M.c).act 1 0 = (M.a, M.c) ∧112      M.a * M.a + -(ν * (M.c * M.c)) ≠ 0 ∧113      M2.smul (M.a * M.a + -(ν * (M.c * M.c))) M =114        (boost ν M.a M.c).mul (borel (M.a * M.a + -(ν * (M.c * M.c))) (M.a * M.b + -(ν * (M.c * M.d))) M.det)) ∧115    (∀ a b e : Shell p, (borel a b e).act 1 0 = (a, 0)) ∧116    (∀ l α1 β1 a1 b1 e1 α2 β2 a2 b2 e2 : Shell p, l ≠ 0 → a1 ≠ 0 → a2 ≠ 0 → (α1 ≠ 0 ∨ β1 ≠ 0) →117      M2.smul l ((boost ν α1 β1).mul (borel a1 b1 e1)) = (boost ν α2 β2).mul (borel a2 b2 e2) →118      α1 * β2 = α2 * β1 ∧ e2 * a1 = e1 * a2 ∧ e2 * b1 = e1 * b2) :=119  (fld hp).frame_triple hν120121end Prime122end Shell123end FRC124