Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual optimizers and two-price defects

Abstract

Complete original prime-layer optimizers and their two-price pressure identity.

Theorem 1.1 (The original reciprocal-log price is positive).

Lean statement: D5/S3/Arith/Robin/ActualTwoPriceDefect.price_pos

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/ActualTwoPriceDefect.price_pos (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every real x>1, price(x)=1/(x*log(x)) is positive. This existing supplier is consumed by OriginalPrimeSourceOrder when identifying complete strict inventories.

Theorem 1.2 (The original reciprocal-log price decreases).

Lean statement: D5/S3/Arith/Robin/ActualTwoPriceDefect.price_antitone

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/ActualTwoPriceDefect.price_antitone (✓ std3). ∎

Source. Repository-derived.

Commentary.

For real x,y with 1<x and x<=y, price(y)<=price(x). The equal endpoint is included. OriginalPrimeSourceOrder uses this order in the closed inventory-interval sandwich.

Theorem 1.3 (Lower positive price enlarges the complete strict inventory).

Lean statement: D5/S3/Arith/Robin/ActualTwoPriceDefect.strictInteger_dvd

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/ActualTwoPriceDefect.strictInteger_dvd (✓ std3). ∎

Source. Repository-derived.

Commentary.

For positive real prices q,r with r<=q, strictInteger(q) divides strictInteger(r). The proof compares every natural factorization coordinate, retaining complete prime stacks, zero coordinates and equality-price behavior. OriginalPrimeSourceOrder consumes this result after establishing actual source-clock order.

The objective is log(sigma(n)/n)-q*log(n). The strict integer selects every layer with marginal greater than q; the maximal integer also includes every equality layer. All primes, positive layers and simultaneous ties are retained.

Theorem 1.4 (The complete maximal optimizer).

Lean statement: D5/S3/Arith/Robin/ActualTwoPriceDefect.maximalInteger_spec

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/ActualTwoPriceDefect.maximalInteger_spec (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every positive real price, the weak layer set is finite and each prime fiber is a complete initial interval. Its finite exponent product is positive, has the stated exponents, and is the greatest original optimizer in the stated order. Finiteness and optimality follow from the existing marginal decay and local threshold suppliers, without a finite prime or exponent truncation hypothesis.

Theorem 1.5 (Pressure across all activation events).

Lean statement: D5/S3/Arith/Robin/ActualTwoPriceDefect.pressure_integral

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/ActualTwoPriceDefect.pressure_integral (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a,b>1, the oriented integral of clock(u)weight(u) is pressure(price(b))-pressure(price(a)). Here price(u)=1/(ulog(u)), weight(u)=(1+log(u))/(u^2*log(u)^2), and clock(u) is the logarithm of the same strict optimizing integer. Compact layer support proves stability on the correct side of a tie. The one-sided derivative and integrability are proved before the fundamental theorem of calculus is applied.

Theorem 1.6 (Keep the source integer at both prices).

Lean statement: D5/S3/Arith/Robin/ActualTwoPriceDefect.two_price_oriented

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/ActualTwoPriceDefect.two_price_oriented (✓ std3). ∎

Source. Repository-derived.

Commentary.

For x,a>1, the actual defect of integerAt(x) at price(a) equals the oriented integral from x to a of (clock(u)-clock(x))*weight(u). The source integer is retained rather than replaced by an independently chosen inventory.

Theorem 1.7 (The same cost for every comparison optimizer).

Lean statement: D5/S3/Arith/Robin/ActualTwoPriceDefect.npc5_any_comparison_optimizer

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/ActualTwoPriceDefect.npc5_any_comparison_optimizer (✓ std3). ∎

Source. Repository-derived.

Commentary.

When A=clock(x)>1, every positive original optimizer at price(A), including the maximal tied optimizer, has objective gain over integerAt(x) equal to the integral from min(x,A) to max(x,A) of |clock(u)-clock(x)|*weight(u). Clock monotonicity pays both price orders. This exact defect identity does not supply the strict Robin endpoint sign.

References