From daf9c70817e879ba94a94c17ffe3e493d17f7401 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 7 Oct 2026 16:02:50 +0530 Subject: [PATCH 1/2] Prove exact odd-state telescoping products and finite descent equivalence --- .github/workflows/ci.yml | 1 + Collatz.lean | 1 + Collatz/Exploration/ExactTraceProduct.lean | 69 ++++++++++++++++++++++ README.md | 11 ++++ RESEARCH.md | 11 ++++ scripts/audit_exact_trace_product.py | 30 ++++++++++ 6 files changed, 123 insertions(+) create mode 100644 Collatz/Exploration/ExactTraceProduct.lean create mode 100644 scripts/audit_exact_trace_product.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ecb59a64..b679e372 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -50,6 +50,7 @@ jobs: python3 scripts/audit_floor_product_error.py python3 scripts/audit_product_spread_obstruction.py python3 scripts/audit_floor_budget_comparison.py + python3 scripts/audit_exact_trace_product.py python3 scripts/audit_eleven_halves_clock.py - name: Check exact first-descent intervals diff --git a/Collatz.lean b/Collatz.lean index f7be25ce..e8ad7953 100644 --- a/Collatz.lean +++ b/Collatz.lean @@ -2123,3 +2123,4 @@ import Collatz.Exploration.AffineBandExit import Collatz.Exploration.FloorProductError import Collatz.Exploration.ProductSpreadObstruction import Collatz.Exploration.FloorBudgetComparison +import Collatz.Exploration.ExactTraceProduct diff --git a/Collatz/Exploration/ExactTraceProduct.lean b/Collatz/Exploration/ExactTraceProduct.lean new file mode 100644 index 00000000..e8f1ae16 --- /dev/null +++ b/Collatz/Exploration/ExactTraceProduct.lean @@ -0,0 +1,69 @@ +import Collatz.Exploration.FloorProductError + +/-! Exact finite telescoping product of odd-state error factors. +This is a classical product identity formalized without division. -/ +namespace Collatz.Exploration.ExactTraceProduct + +def numerator (n : Nat) : Nat → Nat + | 0 => 1 + | j+1 => numerator n j * + (if acceleratedOrbit j n%2=0 then 1 else 3*acceleratedOrbit j n) + +def denominator (n : Nat) : Nat → Nat + | 0 => 1 + | j+1 => denominator n j * + (if acceleratedOrbit j n%2=0 then 1 else 3*acceleratedOrbit j n+1) + +/-- Every odd-state correction is retained exactly in this finite identity. -/ +theorem exact_product (n j : Nat) : + numerator n j*(2^j*acceleratedOrbit j n) = + denominator n j*(3^oddCount n j*n) := by + induction j with + | zero => simp [numerator,denominator] + | succ j ih => + rcases Arith.mod_two_eq_zero_or_one (acceleratedOrbit j n) with he | ho + · rw [numerator,denominator,he] + simp only [↓reduceIte,Nat.mul_one] + rw [acceleratedOrbit_succ_step,Density.oddCount_succ_last,he,Nat.add_zero,Nat.pow_succ] + have hx : 2*acceleratedStep (acceleratedOrbit j n) = acceleratedOrbit j n := by + simp only [acceleratedStep,he,↓reduceIte] + omega + rw [Nat.mul_assoc (2^j),hx] + exact ih + · rw [numerator,denominator] + simp only [show acceleratedOrbit j n%2 ≠ 0 by omega,↓reduceIte] + rw [acceleratedOrbit_succ_step,Density.oddCount_succ_last,ho,Nat.pow_succ,Nat.pow_succ] + have hx : 2*acceleratedStep (acceleratedOrbit j n) = 3*acceleratedOrbit j n+1 := by + simp only [acceleratedStep,show acceleratedOrbit j n%2 ≠ 0 by omega,↓reduceIte] + omega + rw [Nat.mul_assoc (2^j),hx] + have hh := congrArg (fun z => z*(3*(3*acceleratedOrbit j n+1))) ih + simp only [Nat.mul_assoc,Nat.mul_left_comm,Nat.mul_comm] at hh ⊢ + exact hh + +theorem numerator_positive {n : Nat} (hn : 0 < n) (j : Nat) : 0 < numerator n j := by + induction j with + | zero => simp [numerator] + | succ j ih => + rw [numerator] + split + · simpa using ih + · exact Nat.mul_pos ih (Nat.mul_pos (by decide) (acceleratedOrbit_positive hn j)) + +/-- Exact finite descent test. It uses the actual trace, not an orbit-independent prediction. -/ +theorem descent_iff {n : Nat} (hn : 0 < n) (j : Nat) : + acceleratedOrbit j n < n ↔ + denominator n j*3^oddCount n j < numerator n j*2^j := by + have ha := numerator_positive hn j + have hd : 0 < 2^j := Nat.pow_pos (by decide) + have hmul : 0 < numerator n j*2^j := Nat.mul_pos ha hd + have hi := exact_product n j + rw [← Nat.mul_assoc] at hi + have h1 := Nat.mul_lt_mul_left hmul (b := acceleratedOrbit j n) (c := n) + have h2 := Nat.mul_lt_mul_right hn + (b := denominator n j*3^oddCount n j) (c := numerator n j*2^j) + rw [hi] at h1 + rw [← Nat.mul_assoc (denominator n j)] at h1 + exact h1.symm.trans h2 + +end Collatz.Exploration.ExactTraceProduct diff --git a/README.md b/README.md index efc63841..37ed873f 100644 --- a/README.md +++ b/README.md @@ -167,3 +167,14 @@ where the linear denominator is positive. This compares bounds, not exit certificate sets (the sets use different additional assumptions). Audit: 20,301 exact integer comparisons including v=0, three theorem footprints, and two false controls rejected. This is classical mathematics, not frontier novelty. + +### Exact trace-product descent test + +`ExactTraceProduct.lean` retains A = product of 3x and Z = product of 3x+1 +at the odd states of a finite accelerated trace. It proves +`A 2^j T_j(n) = Z 3^a n`, positivity of A for n>0, and the exact test +`T_j(n)0, and the exact test +`T_j(n) 0: assert (x Date: Wed, 7 Oct 2026 16:06:04 +0530 Subject: [PATCH 2/2] Certify descent from source-floor factors and measure first-certificate delays --- .github/workflows/ci.yml | 1 + Collatz.lean | 1 + Collatz/Exploration/FloorProductDescent.lean | 38 +++++++++++++++ README.md | 13 +++++ RESEARCH.md | 13 +++++ scripts/audit_floor_product_descent.py | 51 ++++++++++++++++++++ 6 files changed, 117 insertions(+) create mode 100644 Collatz/Exploration/FloorProductDescent.lean create mode 100644 scripts/audit_floor_product_descent.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b679e372..44e7edac 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -51,6 +51,7 @@ jobs: python3 scripts/audit_product_spread_obstruction.py python3 scripts/audit_floor_budget_comparison.py python3 scripts/audit_exact_trace_product.py + python3 scripts/audit_floor_product_descent.py python3 scripts/audit_eleven_halves_clock.py - name: Check exact first-descent intervals diff --git a/Collatz.lean b/Collatz.lean index e8ad7953..b11d68b9 100644 --- a/Collatz.lean +++ b/Collatz.lean @@ -2124,3 +2124,4 @@ import Collatz.Exploration.FloorProductError import Collatz.Exploration.ProductSpreadObstruction import Collatz.Exploration.FloorBudgetComparison import Collatz.Exploration.ExactTraceProduct +import Collatz.Exploration.FloorProductDescent diff --git a/Collatz/Exploration/FloorProductDescent.lean b/Collatz/Exploration/FloorProductDescent.lean new file mode 100644 index 00000000..42cb7ecc --- /dev/null +++ b/Collatz/Exploration/FloorProductDescent.lean @@ -0,0 +1,38 @@ +import Collatz.Exploration.FloorProductError + +/-! Finite descent from odd count and source-dependent floor factors. +No individual odd-state product is required by this sufficient criterion. -/ +namespace Collatz.Exploration.FloorProductDescent +open FloorAffineError FloorProductError + +/-- The floor-product criterion forces descent somewhere before the selected endpoint. -/ +theorem descent_before {n j : Nat} (hn : 0 < n) + (hs : 3^oddCount n j*weight n^oddCount n j < + 2^j*base n^oddCount n j) : + ∃ i, i ≤ j ∧ acceleratedOrbit i n < n := by + apply Classical.byContradiction + intro hno + have hf : ∀ i, i ≤ j → n ≤ acceleratedOrbit i n := by + intro i hi + by_cases hd : acceleratedOrbit i n < n + · exact False.elim (hno ⟨i,hi,hd⟩) + · omega + have hb := product_band_budget (n := n) (b := n) (a := j) (c := 0) + (P := 1) (Q := 1) hn (fun i hi => hf i (by omega)) (hf j (by omega)) (by simp) + have hbound : 2^j*base n^oddCount n j ≤ + 3^oddCount n j*weight n^oddCount n j := by simpa using hb + omega + +/-- Certified descent transfers to the ordinary orbit with an explicit time bound. -/ +theorem standard_descent_before {n j : Nat} (hn : 0 < n) + (hs : 3^oddCount n j*weight n^oddCount n j < + 2^j*base n^oddCount n j) : + ∃ t, t ≤ 2*j ∧ orbit t n < n := by + obtain ⟨i,hi,hd⟩ := descent_before hn hs + refine ⟨TimeChange.clock n i,?_,?_⟩ + · have ht := (TimeChange.clock_bounds n i).2 + omega + · rw [TimeChange.orbit_at_clock] + exact hd + +end Collatz.Exploration.FloorProductDescent diff --git a/README.md b/README.md index 37ed873f..51925a96 100644 --- a/README.md +++ b/README.md @@ -178,3 +178,16 @@ not a prediction independent of the orbit, and establishes no universal descent. The product method is classical; no novelty claim is made. Audit: 61,061 exact identities including n=0; 61,000 positive-source descent equivalences; three theorem footprints; two false controls rejected. + +### Descent from source floor and odd count + +`FloorProductDescent.lean` proves that `3^a w(n)^a < 2^j v(n)^a` +forces some accelerated descent by j and ordinary descent by 2j. +Here a is the actual prefix odd count and v(n),w(n) are the floor bases. +The criterion requires no individual odd-state product, but still uses the +actual prefix odd count. No universal eventual certificate is proved. +Audit: 202,000 horizons, 179,921 valid certificates, two theorem footprints, +and two false controls. For sources 2..2000 through horizon 200, 1995 first +certificates matched actual first descent, four lagged, none was missing; +the largest lag was six accelerated steps (n=27, descent 59, certificate 65). +These finite measurements are not density or completeness results. diff --git a/RESEARCH.md b/RESEARCH.md index 457d2eb3..ebe0aeee 100644 --- a/RESEARCH.md +++ b/RESEARCH.md @@ -15997,3 +15997,16 @@ not a prediction independent of the orbit, and establishes no universal descent. The product method is classical; no novelty claim is made. Audit: 61,061 exact identities including n=0; 61,000 positive-source descent equivalences; three theorem footprints; two false controls rejected. + +### Descent from source floor and odd count + +`FloorProductDescent.lean` proves that `3^a w(n)^a < 2^j v(n)^a` +forces some accelerated descent by j and ordinary descent by 2j. +Here a is the actual prefix odd count and v(n),w(n) are the floor bases. +The criterion requires no individual odd-state product, but still uses the +actual prefix odd count. No universal eventual certificate is proved. +Audit: 202,000 horizons, 179,921 valid certificates, two theorem footprints, +and two false controls. For sources 2..2000 through horizon 200, 1995 first +certificates matched actual first descent, four lagged, none was missing; +the largest lag was six accelerated steps (n=27, descent 59, certificate 65). +These finite measurements are not density or completeness results. diff --git a/scripts/audit_floor_product_descent.py b/scripts/audit_floor_product_descent.py new file mode 100644 index 00000000..9781908e --- /dev/null +++ b/scripts/audit_floor_product_descent.py @@ -0,0 +1,51 @@ +#!/usr/bin/env python3 +"""Kernel and independent finite descent-certificate tests.""" +import subprocess +from audit_barrier_kernel import ROOT,check_axioms,check_false_certificates +from check_proof_escapes import violations + +def main(): + name='Collatz.Exploration.FloorProductDescent' + source=ROOT/'Collatz/Exploration/FloorProductDescent.lean' + assert not violations(source.read_text()) + subprocess.run(['lake','build',name],cwd=ROOT,check=True) + checked=certified=0 + for n in range(1,2001): + v=3*(n+1 if n%2==0 else n);w=v+1 + x=n; C=D=1; a=0; descended=False + for j in range(101): + if C*w**a0 + missing=delayed=matched=0 + maxgap=(0,0,0,0) + for n in range(2,2001): + v=3*(n+1 if n%2==0 else n);w=v+1 + x=n;C=D=1;a=0;first_desc=first_cert=None + for j in range(201): + if x0 + maxgap=max(maxgap,(gap,n,first_desc,first_cert)) + print(f'First-certificate comparison through 200: {matched} exact; {delayed} delayed; {missing} missing; max gap {maxgap}') + axioms=check_axioms(source,name) + bad=check_false_certificates(name,[ + 'example : 3^1*4^1 < 2^1*3^1 := by decide\n', + 'example : Collatz.acceleratedOrbit 0 4 < 4 := by decide\n', + ]) + print(f'{checked} horizons; {certified} valid descent certificates; {axioms} theorem footprints; {bad} false controls') + +if __name__=='__main__':main()