Golden Local Threshold
Abstract
Boundary marginal inequalities at a common price make a chosen exponent optimal within one prime direction.
Theorem 1.1 (Boundary thresholds suffice for local optimality).
Proof. Machine-checked in Lean as D5/S3/Arith/GoldenLocalThreshold.golden_prime_local_objective_maximal_of_threshold (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every prime p, real price lambda, and chosen exponent a, assume the next marginal is at most lambda. If a is positive, also assume lambda is at most the adopted boundary marginal; when a is zero, that lower-bound condition is absent. Then every competing natural exponent b has local objective at most the objective at a. Both boundary comparisons are non-strict, so equality and tied optima are retained.
The proof identifies each adjacent objective difference with log p times marginal minus price. Frozen strict decrease of the prime marginals propagates the two boundary inequalities, making the objective nondecreasing up to a and nonincreasing after a.
This is only the sufficiency direction for one fixed prime. It does not prove local necessity, combine prime directions, define the global bounds L or U, characterize highly abundant numbers, reduce absent prime checks to the smallest missing prime, or classify all endpoint ties.