The core module lean/FrcCore/Parity.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/Horizon, Theme/Shift, Theme/Lattice, Theme/Drift, Theme/Observation, Theme/Interference, Theme/Composite, Theme/Ladder, Meridian, Fourier, Algebra, Epi, Dimensions, Poly, Quaternion, Causality, Representation, Reductio, Godel, Finitism, Geometry, Complex, Instances, Rh, Entropy, Dirac, Gravity, S13, Qm, Pnp, 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): 9 theorems (0 definitions): 9 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.FrameCore23/-!4# FrcCore.Parity — the square class of the drive is the parity of its exponent (the frame theme)56On every frame `g^m` is a square exactly when the drive-step count `m` is even (8:B5, `parity_iff`); the drive and its7inverse are nonsquares (8:B3, 8:B6). Split from `Orbit.lean` by the ledger migration (task LM24), every name unchanged,8so that a theme needing the square class does not carry the orbit of the generators; `Orbit.lean` imports this file.9No axioms.10-/1112namespace FRC13namespace Shell14namespace Frame15variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}1617/-! ## The square class of the drive is the parity of its exponent (moved from 8-dirac, task LM17) -/1819
theorem two_mul_mod (l : Nat) : (2 * l) % 2 = 0 := by20 rw [← Nat.add_zero (2 * l)]; exact FRC.Nat.add_mul_mod_self_left 0 l 2 (Nat.zero_lt_succ 1)2122theorem mod_two_of_mod_four_mul (m q : Nat) : (4 * q + m) % 2 = m % 2 := by23 have : 4 * q + m = 2 * (2 * q) + m := by rw [← FRC.Nat.mul_assoc]24 rw [this, FRC.Nat.add_mul_mod_self_left m (2 * q) 2 (Nat.zero_lt_succ 1)]2526theorem mod_n_mod_two (F : Frame p κ g) (m : Nat) : (m % (p - 1)) % 2 = m % 2 := by27 match FRC.Nat.mod_spec (p - 1) F.n_pos m with28 | ⟨q, hq⟩ =>29 have e : m = 4 * (κ * q) + m % (p - 1) := by30 rw [← FRC.Nat.mul_assoc, ← F.n_eq]; exact hq31 calc (m % (p - 1)) % 2 = (4 * (κ * q) + m % (p - 1)) % 2 := (mod_two_of_mod_four_mul _ _).symm32 _ = m % 2 := by rw [← e]3334/-- 8:B5 — the square class is chronon parity: on every frame, `g^m` is a square exactly when the drive-step35count `m` is even (Theorem `parity`). -/36theorem parity_iff (F : Frame p κ g) (m : Nat) : (∃ y : Shell p, y * y = g ^ m) ↔ m % 2 = 0 := by37 constructor38 · rintro ⟨y, hy⟩39 have hy0 : y ≠ 0 := fun h0 => F.pow_ne_zero m (by rw [← hy, h0, Shell.mul_zero])40 obtain ⟨l, hl, hgl⟩ := F.eq_pow_of_ne_zero hy041 have h2 : g ^ (2 * l) = g ^ m := by42 rw [Nat.mul_comm, Shell.pow_mul, Shell.pow_two, hgl]; exact hy43 rw [F.pow_mod, F.pow_mod m] at h244 have h3 := F.pow_inj (Nat.mod_lt _ F.n_pos) (Nat.mod_lt _ F.n_pos) h245 rw [← mod_n_mod_two F m, ← h3, mod_n_mod_two F]46 exact two_mul_mod l47 · intro h48 match FRC.Nat.mod_spec 2 (Nat.zero_lt_succ 1) m with49 | ⟨q, hq⟩ =>50 rw [h, Nat.add_zero] at hq51 exact ⟨g ^ q, by rw [hq, Nat.mul_comm, Shell.pow_mul, Shell.pow_two]⟩5253/-- 8:B3 — the drive is a nonsquare on every frame (`m = 1`). -/54theorem drive_nonsquare (F : Frame p κ g) : ¬ ∃ y : Shell p, y * y = g := fun ⟨y, hy⟩ =>55 Nat.noConfusion ((parity_iff F 1).1 ⟨y, by rw [Shell.pow_one]; exact hy⟩)5657theorem mod_two_cases (m : Nat) : m % 2 = 0 ∨ m % 2 = 1 := by58 have := Nat.mod_lt m (Nat.zero_lt_succ 1)59 match m % 2, this with60 | 0, _ => exact .inl rfl61 | 1, _ => exact .inr rfl62 | k + 2, hk => exact absurd hk (Nat.not_lt_of_le (Nat.le_add_left 2 k))6364theorem succ_mod_two_eq_zero_iff (m : Nat) : (m + 1) % 2 = 0 ↔ m % 2 = 1 := by65 rw [FRC.Nat.add_mod m 1 2 (Nat.zero_lt_succ 1)]66 rcases mod_two_cases m with h | h <;> rw [h]67 · exact ⟨fun e => Nat.noConfusion e, fun e => Nat.noConfusion e⟩68 · exact ⟨fun _ => rfl, fun _ => rfl⟩6970/-- The inverse of the drive is `g^{p−2}`: every `y` with `g y = 1` is an odd power of `g`. -/71theorem inv_drive_odd (F : Frame p κ g) {y : Shell p} (hy : g * y = 1) :72 ∃ l, l < p - 1 ∧ g ^ l = y ∧ l % 2 = 1 := by73 have hy0 : y ≠ 0 := fun h0 => F.one_ne_zero (by rw [← hy, h0, Shell.mul_zero])74 obtain ⟨l, hl, hgl⟩ := F.eq_pow_of_ne_zero hy075 refine ⟨l, hl, hgl, ?_⟩76 have h1 : g ^ (l + 1) = 1 := by rw [Shell.pow_succ, hgl, Shell.mul_comm]; exact hy77 have h2 := F.mod_eq_zero_of_pow_eq_one h178 have h3 : l + 1 = p - 1 := by79 match Nat.lt_or_ge (l + 1) (p - 1) with80 | .inl hlt => exact absurd (by rw [FRC.Nat.mod_eq_of_lt hlt] at h2; exact h2) (Nat.succ_ne_zero l)81 | .inr hge => exact Nat.le_antisymm (Nat.succ_le_of_lt hl) hge82 have h4 : (l + 1) % 2 = 0 := by83 rw [h3, F.n_eq, ← Nat.add_zero (4 * κ), mod_two_of_mod_four_mul]84 exact (succ_mod_two_eq_zero_iff l).1 h48586/-- 8:B3, 8:B6 — the reframing flip preserves the class: the inverse of the drive is a nonsquare (an odd87power of `g`), so `[g⁻¹] = [g]`. -/88theorem inv_drive_nonsquare (F : Frame p κ g) {y : Shell p} (hy : g * y = 1) :89 ¬ ∃ r : Shell p, r * r = y := fun h => by90 obtain ⟨l, _, hgl, hodd⟩ := inv_drive_odd F hy91 rw [← hgl] at h92 have h2 := (parity_iff F l).1 h93 rw [hodd] at h294 exact Nat.noConfusion h29596end Frame97end Shell98end FRC99