Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Powerful Fibonacci support bound

Abstract

A finite original odd-depth support bounds powerful Fibonacci indices.

Fix a finite set S of primes greater than five and its least Fibonacci rank closure H(S). The theorem establishes the count using the prime-index nonsquare theorem, the five-adic depth law, prime-to-index valuation, and Fibonacci square-class rigidity. Its only parameter condition is that S consists of primes greater than five.

Definition 1.1 (Odd prime support).

Lean statement: D5/S3/Arith/Primes/PowerfulFibonacciSupportBound.oddPrimeSupport

Formalization. D5/S3/Arith/Primes/PowerfulFibonacciSupportBound.oddPrimeSupport (✓ std3).

Source. Repository-derived.

Commentary.

The distinct prime factors of the original Fibonacci value F_n whose valuations in F_n are odd.

Definition 1.2 (Supported powerful index).

Lean statement: D5/S3/Arith/Primes/PowerfulFibonacciSupportBound.supportedPowerfulIndex

Formalization. D5/S3/Arith/Primes/PowerfulFibonacciSupportBound.supportedPowerfulIndex (✓ std3).

Source. Repository-derived.

Commentary.

A positive index n belongs when F_n is powerful and every prime factor of F_n with odd original depth at least three belongs to S. The condition uses the first Fibonacci zero rank of each prime, not the depth at a multiplied index.

Theorem 1.3 (Finite count with four exceptions).

Lean statement: D5/S3/Arith/Primes/PowerfulFibonacciSupportBound.powerful_fibonacci_support_bound

Proof. Machine-checked in Lean as D5/S3/Arith/Primes/PowerfulFibonacciSupportBound.powerful_fibonacci_support_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

There is a finite set containing exactly the supported powerful indices, with cardinality at most two to the size of H(S) minus four. The proof places every odd prime support inside H(S), uses the index-support descent to reduce small odd support to five-smooth indices, proves their powerful-value classification, and injects all remaining indices into the subsets of H(S) outside the eight small supports. The small group contributes at most four indices.

References