Certify finite descent from source-floor corrected coefficients

.github/workflows/ci.yml

@@ -50,6 +50,8 @@ 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_floor_product_descent.py
           python3 scripts/audit_eleven_halves_clock.py
 
       - name: Check exact first-descent intervals

Collatz.lean

@@ -2123,3 +2123,5 @@ import Collatz.Exploration.AffineBandExit
 import Collatz.Exploration.FloorProductError
 import Collatz.Exploration.ProductSpreadObstruction
 import Collatz.Exploration.FloorBudgetComparison
+import Collatz.Exploration.ExactTraceProduct
+import Collatz.Exploration.FloorProductDescent

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

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

README.md

@@ -167,3 +167,27 @@ 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)<n` iff `Z 3^a < A 2^j`. This is a trace-dependent telescoping identity,
+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.

RESEARCH.md

@@ -15986,3 +15986,27 @@ 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)<n` iff `Z 3^a < A 2^j`. This is a trace-dependent telescoping identity,
+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.

scripts/audit_exact_trace_product.py

@@ -0,0 +1,30 @@
+#!/usr/bin/env python3
+"""Exact trace-product kernel and independent recurrence audit."""
+import subprocess
+from audit_barrier_kernel import ROOT,check_axioms,check_false_certificates
+from check_proof_escapes import violations
+
+def main():
+    name='Collatz.Exploration.ExactTraceProduct'
+    source=ROOT/'Collatz/Exploration/ExactTraceProduct.lean'
+    assert not violations(source.read_text())
+    subprocess.run(['lake','build',name],cwd=ROOT,check=True)
+    checks=0
+    for n in range(1001):
+        x=n; A=Z=C=D=1
+        for j in range(61):
+            assert A*D*x==Z*C*n
+            if n > 0: assert (x<n)==(Z*C<A*D)
+            checks+=1
+            if x%2:
+                A*=3*x; Z*=3*x+1; C*=3; x=(3*x+1)//2
+            else: x//=2
+            D*=2
+    count=check_axioms(source,name)
+    bad=check_false_certificates(name,[
+        'example : Collatz.Exploration.ExactTraceProduct.numerator 3 1 = 10 := by decide\n',
+        'example : Collatz.Exploration.ExactTraceProduct.denominator 3 1 = 9 := by decide\n',
+    ])
+    print(f'{checks} identities; {count} theorem footprints; {bad} false controls rejected')
+
+if __name__=='__main__':main()

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**a<D*v**a:
+                assert descended
+                certified+=1
+            checked+=1
+            if x%2: x=(3*x+1)//2;C*=3;a+=1
+            else:x//=2
+            D*=2
+            descended |= x<n
+    assert certified>0
+    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 x<n and first_desc is None:first_desc=j
+            if C*w**a<D*v**a and first_cert is None:first_cert=j
+            if x%2:x=(3*x+1)//2;C*=3;a+=1
+            else:x//=2
+            D*=2
+        if first_cert is None:missing+=1
+        else:
+            assert first_desc is not None and first_desc<=first_cert
+            gap=first_cert-first_desc
+            matched+=gap==0;delayed+=gap>0
+            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()