diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a31c072e..9e09d6c6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -54,6 +54,7 @@ jobs: python3 scripts/audit_floor_product_descent.py python3 scripts/audit_product_delay_certificates.py python3 scripts/audit_product_thresholds.py + python3 scripts/audit_coefficient_gap_threshold.py python3 scripts/audit_eleven_halves_clock.py - name: Check exact first-descent intervals diff --git a/Collatz.lean b/Collatz.lean index a64ddec9..403861a4 100644 --- a/Collatz.lean +++ b/Collatz.lean @@ -2127,3 +2127,4 @@ import Collatz.Exploration.ExactTraceProduct import Collatz.Exploration.FloorProductDescent import Collatz.Exploration.ProductDelayCertificates import Collatz.Exploration.ProductThresholds +import Collatz.Exploration.CoefficientGapThreshold diff --git a/Collatz/Exploration/CoefficientGapThreshold.lean b/Collatz/Exploration/CoefficientGapThreshold.lean new file mode 100644 index 00000000..d11e7f2d --- /dev/null +++ b/Collatz/Exploration/CoefficientGapThreshold.lean @@ -0,0 +1,58 @@ +import Collatz.Exploration.ProductThresholds +import Collatz.Exploration.FloorBudgetComparison +import Collatz.Strategy.FirstLightDescent + +/-! A linear sufficient source-floor threshold for each light coefficient pair. +These are conditional descent tools based on classical Bernoulli bounds. -/ +namespace Collatz.Exploration.CoefficientGapThreshold +open FloorAffineError FloorProductError ProductThresholds FloorBudgetComparison + +/-- A scalar margin implies the full powered product test. -/ +theorem passes_of_scalar {C D k b : Nat} + (hc : C*weight b < D*(weight b-k)) : Passes C D k b := by + have hw : 0 < weight b^k := Nat.pow_pos (by unfold weight; omega) + have h1 := Nat.mul_lt_mul_of_pos_right hc hw + have h2 := Nat.mul_le_mul_left D (ratio_comparison b k) + simp only [Nat.mul_assoc,Nat.mul_left_comm,Nat.mul_comm] at h1 h2 + have hh : (C*weight b^k)*weight b < (D*base b^k)*weight b := by + simp only [Nat.mul_left_comm,Nat.mul_comm] + omega + exact Nat.lt_of_mul_lt_mul_right hh + +/-- The required floor weight scales with odd count and reciprocal coefficient gap. -/ +theorem passes_of_gap {C D k b : Nat} (hl : C ≤ D) + (hg : k*D < (D-C)*weight b) : Passes C D k b := by + apply passes_of_scalar + have he : (D-C)*weight b = D*weight b-C*weight b := Nat.sub_mul _ _ _ + have hm : D*(weight b-k) = D*weight b-D*k := Nat.mul_sub _ _ _ + have hc := Nat.mul_le_mul_right (weight b) hl + rw [he] at hg + rw [hm] + have hk : k*D=D*k := Nat.mul_comm _ _ + omega + +/-- Gap-specific scalar source thresholds certify descent, with no individual trace products. -/ +theorem descent_of_gap {n j : Nat} (hn : 0 < n) + (hl : 3^oddCount n j ≤ 2^j) + (hg : oddCount n j*2^j < (2^j-3^oddCount n j)*weight n) : + ∃ i, i ≤ j ∧ acceleratedOrbit i n < n := by + apply FloorProductDescent.descent_before hn + exact passes_of_gap hl hg + +/-- Improve the existing H*3^H cutoff using the first-light accumulator bound. -/ +theorem first_light_below_horizon {H n j : Nat} (hj : j ≤ H) + (hn : H*2^H < 3*n) + (hf : FirstLightDescent.FirstLight n j) : acceleratedOrbit j n < n := by + by_cases hd : acceleratedOrbit j n < n + · exact hd + · have hb := FirstLightDescent.failure_bound hf (by omega) + have ha := Nat.le_trans (AffineExact.oddCount_le_self n j) hj + have hp : 3^oddCount n j ≤ 2^H := Nat.le_trans (Nat.le_of_lt hf.1) + (Nat.pow_le_pow_right (by decide) hj) + have hm := Nat.mul_le_mul ha hp + have hg : 1 ≤ 2^j-3^oddCount n j := by have := hf.1; omega + have hl := Nat.mul_le_mul_left (3*n) hg + simp only [Nat.mul_assoc,Nat.mul_left_comm,Nat.mul_comm] at hl hb + omega + +end Collatz.Exploration.CoefficientGapThreshold diff --git a/README.md b/README.md index ad73fa39..4031a3e9 100644 --- a/README.md +++ b/README.md @@ -216,3 +216,17 @@ the thresholds are exact for this test, not optimal for actual descent. Audit: eight theorem footprints, 12,006 threshold checks, 1,893 matching odd-count descent cases, two false controls rejected. The method remains a specialization of known product bounds, with no established frontier novelty. + +### Scalar gap criterion and improved finite first-light cutoff + +`CoefficientGapThreshold.lean` proves that `a D < (D-C) w(n)` suffices +for descent by j when C=3^a≤D=2^j. The scalar margin implies the full +product test by the classical Bernoulli comparison. +A separate corollary uses the existing first-light accumulator bound to +improve the coarse repository cutoff n>H*3^H to 3*n>H*2^H: +if a first coefficient crossing occurs by H, descent occurs at that crossing. +It proves no existence of a crossing and no universal convergence. +No frontier novelty has been established for this elementary improvement. +Audit: four theorem footprints, 53,361 scalar cases, 16,043 valid scalar +certificates, 179,303 descent cases, 2,924 first-light cutoff cases, +and two false controls rejected. diff --git a/RESEARCH.md b/RESEARCH.md index 323945a3..84d6f82d 100644 --- a/RESEARCH.md +++ b/RESEARCH.md @@ -16058,3 +16058,17 @@ the thresholds are exact for this test, not optimal for actual descent. Audit: eight theorem footprints, 12,006 threshold checks, 1,893 matching odd-count descent cases, two false controls rejected. The method remains a specialization of known product bounds, with no established frontier novelty. + +### Scalar gap criterion and improved finite first-light cutoff + +`CoefficientGapThreshold.lean` proves that `a D < (D-C) w(n)` suffices +for descent by j when C=3^a≤D=2^j. The scalar margin implies the full +product test by the classical Bernoulli comparison. +A separate corollary uses the existing first-light accumulator bound to +improve the coarse repository cutoff n>H*3^H to 3*n>H*2^H: +if a first coefficient crossing occurs by H, descent occurs at that crossing. +It proves no existence of a crossing and no universal convergence. +No frontier novelty has been established for this elementary improvement. +Audit: four theorem footprints, 53,361 scalar cases, 16,043 valid scalar +certificates, 179,303 descent cases, 2,924 first-light cutoff cases, +and two false controls rejected. diff --git a/scripts/audit_coefficient_gap_threshold.py b/scripts/audit_coefficient_gap_threshold.py new file mode 100644 index 00000000..1c85fbee --- /dev/null +++ b/scripts/audit_coefficient_gap_threshold.py @@ -0,0 +1,56 @@ +#!/usr/bin/env python3 +"""Exact scalar-to-product and conditional descent 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.CoefficientGapThreshold' + source=ROOT/'Collatz/Exploration/CoefficientGapThreshold.lean' + assert not violations(source.read_text()) + subprocess.run(['lake','build',name],cwd=ROOT,check=True) + tested=certified=0 + for C in range(11): + for D in range(11): + for k in range(21): + for b in range(21): + v=3*(b+1 if b%2==0 else b);w=v+1 + if C*w