From d4088d946b15a25cee7a69b663f898cb804c85fb Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 7 Oct 2026 07:56:38 +0530 Subject: [PATCH] proof: formalize anchored barrier kernels and finite cycle certificates --- .github/workflows/ci.yml | 3 + Collatz.lean | 1 + Collatz/Exploration/BarrierKernel.lean | 216 +++++++++++++++++++++++++ README.md | 4 + Research/BarrierKernel.md | 104 ++++++++++++ scripts/audit_barrier_kernel.py | 53 ++++++ scripts/test_barrier_kernel.py | 76 +++++++++ 7 files changed, 457 insertions(+) create mode 100644 Collatz/Exploration/BarrierKernel.lean create mode 100644 Research/BarrierKernel.md create mode 100644 scripts/audit_barrier_kernel.py create mode 100644 scripts/test_barrier_kernel.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1a096986..f3a0a92f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -34,6 +34,9 @@ jobs: - name: Check integrity run: ./scripts/check_integrity.sh + - name: Check anchored barriers and finite cycle certificates + run: python3 scripts/audit_barrier_kernel.py + - name: Check exact first-descent intervals run: | python3 scripts/descent_intervals.py --check diff --git a/Collatz.lean b/Collatz.lean index 4411299f..0852c031 100644 --- a/Collatz.lean +++ b/Collatz.lean @@ -2105,3 +2105,4 @@ import Collatz.Strategy.ProductDescentCheck import Collatz.Research.StoppingAtlas.All import Collatz.Research.PassageAtlas.All +import Collatz.Exploration.BarrierKernel diff --git a/Collatz/Exploration/BarrierKernel.lean b/Collatz/Exploration/BarrierKernel.lean new file mode 100644 index 00000000..a62ab610 --- /dev/null +++ b/Collatz/Exploration/BarrierKernel.lean @@ -0,0 +1,216 @@ +import Collatz.Exploration.OrbitFloor +import Collatz.Core.Pigeonhole + +/-! +# Anchored barriers and sharp finite cycle extraction + +A local no-descent test moves its comparison level with its input. It is +therefore not forward invariant. Keep the barrier fixed when shifting an +orbit. The all-horizon intersection is the greatest forward invariant set +above that barrier. A finite orbit confined to [b,u] repeats after at most +u-b+1 steps, with no assumption about the unobserved future. + +These are structural reductions, not claims of literature novelty or Collatz. +-/ +namespace Collatz.Exploration.BarrierKernel + +/-- Survival above a fixed barrier through a finite, inclusive time window. -/ +def Survives (b K n : Nat) : Prop := ∀ k, k ≤ K → b ≤ orbit k n + +/-- The all-horizon kernel keeps the same barrier at every future state. -/ +def Kernel (b n : Nat) : Prop := ∀ k, b ≤ orbit k n + +theorem survives_zero (b n : Nat) : Survives b 0 n ↔ b ≤ n := by + constructor + · intro h; exact h 0 (by omega) + · intro h k hk + have he : k = 0 := by omega + subst k + exact h + +/-- Exact predecessor recursion; suitable for finite certificate checkers. -/ +theorem survives_succ (b K n : Nat) : + Survives b (K+1) n ↔ b ≤ n ∧ Survives b K (step n) := by + constructor + · intro h + refine ⟨h 0 (by omega), ?_⟩ + intro k hk + exact h (k+1) (by omega) + · rintro ⟨hn, hs⟩ k hk + cases k with + | zero => exact hn + | succ k => exact hs k (by omega) + +theorem survives_mono_time {b K L n : Nat} (h : Survives b K n) + (hLK : L ≤ K) : Survives b L n := by + intro k hk; exact h k (by omega) + +theorem survives_mono_barrier {a b K n : Nat} (h : Survives b K n) + (hab : a ≤ b) : Survives a K n := by + intro k hk; exact Nat.le_trans hab (h k hk) + +/-- Splitting a window at j preserves the anchor, including both endpoints. -/ +theorem survives_split (b j K n : Nat) : + Survives b (j+K) n ↔ Survives b j n ∧ Survives b K (orbit j n) := by + constructor + · intro h + refine ⟨survives_mono_time h (by omega), ?_⟩ + intro k hk + rw [← orbit_add] + exact h (k+j) (by omega) + · rintro ⟨hp, ht⟩ k hk + by_cases hkj : k ≤ j + · exact hp k hkj + · have hs := ht (k-j) (by omega) + rw [← orbit_add, Nat.sub_add_cancel (by omega : j ≤ k)] at hs + exact hs + +theorem kernel_iff_all_windows (b n : Nat) : + Kernel b n ↔ ∀ K, Survives b K n := by + constructor + · intro h K k _; exact h k + · intro h k; exact h k k (Nat.le_refl k) + +theorem kernel_forward {b n : Nat} (h : Kernel b n) (j : Nat) : + Kernel b (orbit j n) := by + intro k; rw [← orbit_add]; exact h (k+j) + +theorem kernel_step (b n : Nat) : Kernel b n ↔ b ≤ n ∧ Kernel b (step n) := by + constructor + · intro h; exact ⟨h 0, fun k => h (k+1)⟩ + · rintro ⟨hn, hs⟩ k + cases k with + | zero => exact hn + | succ k => exact hs k + +/-- Any invariant set above b is contained in the kernel. -/ +theorem greatest_invariant {S : Nat → Prop} {b : Nat} + (hbound : ∀ n, S n → b ≤ n) + (hclosed : ∀ n, S n → S (step n)) : + ∀ n, S n → Kernel b n := by + intro n hn k + induction k generalizing n with + | zero => exact hbound n hn + | succ k ih => exact ih (step n) (hclosed n hn) + +theorem kernel_trap {b : Nat} (hb : 1 < b) : + OrbitFloor.Trap (Kernel b) := by + refine ⟨?_, ?_, ?_⟩ + · intro n hn; have := hn 0; simp at this; omega + · intro h; have := h 0; simp at this; omega + · intro n hn; exact (kernel_step b n).mp hn |>.2 + +/-- A kernel above 1 contains only nonconvergent states. -/ +theorem kernel_failure {b n : Nat} (hb : 1 < b) (h : Kernel b n) : + ¬ OrbitFloor.Converges n := + (OrbitFloor.trap_failure (kernel_trap hb) h).2 + +/-- Nonconvergence is equivalent to membership in the single kernel b=2. -/ +theorem kernel_two_iff_failure {n : Nat} (hp : 0 < n) : + Kernel 2 n ↔ ¬ OrbitFloor.Converges n := by + constructor + · exact kernel_failure (by decide) + · intro hf k + have hpos := orbit_positive hp k + have hne : orbit k n ≠ 1 := fun he => hf ⟨k, he⟩ + omega + +/-- The empty-kernel obligation is still precisely the original conjecture. -/ +theorem empty_kernel_two_iff_collatz : + (∀ n, ¬ Kernel 2 n) ↔ CollatzConjecture := by + constructor + · intro he n hp + by_cases hc : OrbitFloor.Converges n + · exact hc + · exact False.elim (he n ((kernel_two_iff_failure hp).mpr hc)) + · intro hc n hn + have hpos : 0 < n := by have := hn 0; simp at this; omega + exact kernel_failure (by decide) hn (hc n hpos) + +/-- Fixed anchors characterize the existing attained orbit-floor reduction. -/ +theorem floor_iff_kernel (m : Nat) : + OrbitFloor.Floor m ↔ 1 < m ∧ Kernel m m := Iff.rfl + +/-- A sharp finite interval certificate extracts a closed orbit above the barrier. +There are u-b+1 available values and one more sampled orbit point. -/ +theorem cycle_of_interval_prefix {b u n : Nat} (hbu : b ≤ u) + (hlo : Survives b (u-b+1) n) + (hhi : ∀ k, k ≤ u-b+1 → orbit k n ≤ u) : + ∃ i j, i < j ∧ j ≤ u-b+1 ∧ + b ≤ orbit i n ∧ orbit (j-i) (orbit i n) = orbit i n := by + obtain ⟨i, j, hij, hj, heq⟩ := Pigeonhole.exists_repeat + (f := fun k => orbit k n - b) (B := u-b+1) (N := u-b+1) + (fun k hk => by have := hlo k hk; have := hhi k hk; omega) + (Nat.le_refl _) + have hi : i ≤ u-b+1 := by omega + have hbi := hlo i hi + have hbj := hlo j hj + have he : orbit i n = orbit j n := by omega + refine ⟨i, j, hij, hj, hbi, ?_⟩ + rw [← orbit_add, Nat.sub_add_cancel (by omega : i ≤ j), ← he] + +/-- An executable inclusive interval-prefix checker. -/ +def intervalCheck (b u : Nat) : Nat → Nat → Bool + | 0, n => decide (b ≤ n ∧ n ≤ u) + | K+1, n => decide (b ≤ n ∧ n ≤ u) && intervalCheck b u K (step n) + +/-- The checker certifies all sampled states, including time zero. -/ +theorem intervalCheck_iff (b u K n : Nat) : + intervalCheck b u K n = true ↔ + ∀ k, k ≤ K → b ≤ orbit k n ∧ orbit k n ≤ u := by + induction K generalizing n with + | zero => + simp only [intervalCheck, decide_eq_true_eq] + constructor + · intro h k hk + have he : k = 0 := by omega + subst k + exact h + · intro h; exact h 0 (by omega) + | succ K ih => + simp only [intervalCheck, Bool.and_eq_true, decide_eq_true_eq, ih] + constructor + · rintro ⟨hn, ht⟩ k hk + cases k with + | zero => exact hn + | succ k => exact ht k (by omega) + · intro h + exact ⟨h 0 (by omega), fun k hk => h (k+1) (by omega)⟩ + +/-- A successful sharp-budget computation supplies a genuine closed orbit. -/ +theorem cycle_of_intervalCheck {b u n : Nat} + (h : intervalCheck b u (u-b+1) n = true) : + ∃ i j, i < j ∧ j ≤ u-b+1 ∧ + b ≤ orbit i n ∧ orbit (j-i) (orbit i n) = orbit i n := by + have hs := (intervalCheck_iff b u (u-b+1) n).mp h + have hz := hs 0 (by omega) + have hbu : b ≤ u := by simp only [orbit_zero_steps] at hz; omega + exact cycle_of_interval_prefix hbu (fun k hk => (hs k hk).1) + (fun k hk => (hs k hk).2) + +/-- Positive control: the trivial cycle is accepted at the sharp budget. -/ +theorem trivial_cycle_control : intervalCheck 1 4 4 1 = true := by decide + +/-- A short accepted prefix is insufficient for cycle extraction. -/ +theorem short_prefix_control : + intervalCheck 3 10 1 3 = true ∧ intervalCheck 3 10 8 3 = false := by decide + +/-- Resetting the comparison level invalidates even one-step forward closure. -/ +theorem moving_barrier_counterexample : + Survives 3 1 3 ∧ ¬ Survives (step 3) 1 (step 3) := by + constructor + · intro k hk + have : k = 0 ∨ k = 1 := by omega + rcases this with rfl | rfl <;> decide + · intro h + have := h 1 (by decide) + change 10 ≤ 5 at this + omega + +/-- A fixed barrier survives that same shift for the remaining budget. -/ +theorem fixed_barrier_control : Survives 3 1 (step 3) := by + intro k hk + have : k = 0 ∨ k = 1 := by omega + rcases this with rfl | rfl <;> decide + +end Collatz.Exploration.BarrierKernel diff --git a/README.md b/README.md index 71ee0e2f..02c9878b 100644 --- a/README.md +++ b/README.md @@ -28,6 +28,10 @@ own verification instructions. ## Research entry points +- [Anchored barriers and finite cycle extraction](Research/BarrierKernel.md) — + exact window splitting, the greatest invariant barrier kernel, an executable + interval checker, and controls against invalid forward-survival reasoning. + - [First passage through 2,592 steps](Research/PassageAtlas/README.md) — a stronger conditional descent theorem, an exact residual condition equivalent to Collatz, and 32,768 new depth-fifteen class certificates. diff --git a/Research/BarrierKernel.md b/Research/BarrierKernel.md new file mode 100644 index 00000000..64e2c287 --- /dev/null +++ b/Research/BarrierKernel.md @@ -0,0 +1,104 @@ +# Anchored barrier investigation — 2026-10-07 + +The new module `Collatz/Exploration/BarrierKernel.lean` formalizes fixed-barrier +survival, an exact finite-window checker, and cycle extraction. It does not +prove Collatz or claim a new result in the published mathematical literature. +The investigation remains open. + +## Mathematical findings + +Write `C` for the ordinary map, including its totalization `C(0)=0`. +For a fixed barrier `b`, define + +`Survives(b,K,n) := ∀ k≤K, b≤C^k(n)`. + +The exact splitting law is + +`Survives(b,j+K,n) ↔ Survives(b,j,n) ∧ Survives(b,K,C^j(n))`. + +Keeping the same barrier matters. The condition `Survives(n,K,n)` cannot +be treated as forward invariant: `3→10→5` passes the one-step test at 3 +and fails the one-step test at 10. The fixed-barrier test at 3 survives +that shift. This rules out an invalid inference from local survivors +to a trapping set; it does not rule out counterexamples to Collatz. + +The intersection over all budgets is + +`Kernel(b,n) := ∀ k, b≤C^k(n)`. + +It is the greatest forward invariant subset of the naturals at least `b`. +For a positive start, membership in `Kernel(2)` is exactly nonconvergence. +Thus proving this kernel empty would still require solving Collatz. Recasting +the question as invariant-set elimination supplies no missing proof by itself. +The attained floor construction in `OrbitFloor.lean` is the diagonal +condition `m>1 ∧ Kernel(m,m)`. + +An inclusive prefix confined to `[b,u]` through time `u-b+1` contains +`u-b+2` points among `u-b+1` values. Subtracting `b` and using the project's +pigeonhole theorem yields indices `i= b + split = min(values[:j + 1]) >= b and min(values[j:]) >= b + assert whole == split, (n, b, j, k) + # Budget-preserving shift has the same anchor, not values[j]. + if whole: + assert min(trajectory(values[j], k)) >= b + checks += 1 + return checks + + +def test_cycles(): + checks = accepted = 0 + for b, u in product(range(12), range(12)): + for n in range(24): + # Natural subtraction agrees with the Lean checker, even b>u. + budget = max(u - b, 0) + 1 + values = trajectory(n, budget) + if all(b <= value <= u for value in values): + seen = {} + for j, value in enumerate(values): + if value in seen: + i = seen[value] + assert i < j <= budget + assert trajectory(value, j - i)[-1] == value + break + seen[value] = j + else: + raise AssertionError((b, u, n, values)) + accepted += 1 + checks += 1 + assert accepted > 0 + return checks, accepted + + +def test_negative_controls(): + # Resetting the barrier fails; keeping it fixed works. + assert min(trajectory(3, 1)) >= 3 + assert min(trajectory(10, 1)) < 10 + assert min(trajectory(10, 1)) >= 3 + # Insufficient budget: an accepted prefix can have no repetition. + short = trajectory(3, 1) + assert min(short) >= 3 and max(short) <= 10 + assert len(set(short)) == len(short) + assert not all(3 <= x <= 10 for x in trajectory(3, 8)) + # The same structural argument allows a genuine nontrivial 5n+1 cycle. + # This prevents treating the invariant-kernel reduction as convergence. + cycle = trajectory(13, 10, multiplier=5) + assert cycle == [13, 66, 33, 166, 83, 416, 208, 104, 52, 26, 13] + long = trajectory(13, 416 - 13 + 1, multiplier=5) + assert all(13 <= x <= 416 for x in long) + assert 1 not in long + + +if __name__ == '__main__': + windows = test_windows() + intervals, accepted = test_cycles() + test_negative_controls() + print(f'{windows} split-window checks; {intervals} interval checks ' + f'({accepted} accepted); moving-barrier, short-prefix, and 5n+1 controls passed')