Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Strict Euler Inventory Second-Order Root Correction

Abstract

The strict Euler inventory has a uniform next logarithmic root coefficient.

For every positive real epsilon there is one real threshold T>1 such that, for every real t>=T and every positive natural U satisfying the exact strict prime factorization law at 1/(t*log(t)), the normalized root correction has the next coefficient.

Theorem 1.1 (Uniform second-order strict inventory law).

Lean statement: D5/S3/Arith/Robin/EulerLayer/EulerLayerRootSecondOrder.strict_inventory_root_second_order

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/EulerLayer/EulerLayerRootSecondOrder.strict_inventory_root_second_order (✓ std3). ∎

Source. Repository-derived.

Commentary.

The conclusion retains every real clock, every prime binder, the strict optimalLayerCount equality, and every positive natural inventory witness. It asserts abs(log(t)*((log(U)-psi(t))/sqrt(t)-(sqrt(2)-1)) +sqrt(2)*log(2)/2)<epsilon.

The proof reuses the existing MediumPNT and the first-layer and third-layer inventory bounds. The second layer is bracketed between theta(rho-1) and theta(rho), where rho is the unique real solution with rho>1 of rho^2log(rho)=tlog(t). Writing s=rho/sqrt(2t) and using the exact equation gives log(t)(s-1) tending to -log(2)/2 without assuming an expansion. The resulting coefficient is -sqrt(2)*log(2)/2.

The one-unit bracket contains equality events and contributes only O(log(rho)). The prime-power terms above the square layer and the third-and-higher actual inventory are retained in the remainder at the smaller sqrt(t)/log(t) scale. No RH, JY, signed-tail, Robin, or attainment assertion is included.

Theorem 1.2 (The consumed strict real cutoff comparison).

Lean statement: D5/S3/Arith/Robin/EulerLayer/EulerLayerRootSecondOrder.second_cutoff_strictMono

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/EulerLayer/EulerLayerRootSecondOrder.second_cutoff_strictMono (✓ std3). ∎

Source. Repository-derived.

Commentary.

Strict monotonicity of x^2*log(x) on x>1 is exposed with its original proof. The new finite prime-min consumer applies it only to rho<p, retaining the strict lower endpoint of the tail.

Theorem 1.3 (The consumed canonical root and its brackets).

Lean statement: D5/S3/Arith/Robin/EulerLayer/EulerLayerRootSecondOrder.second_cutoff_root_spec

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/EulerLayer/EulerLayerRootSecondOrder.second_cutoff_root_spec (✓ std3). ∎

Source. Repository-derived.

Commentary.

The canonical root definition and this exact specification are exposed unchanged. The new consumer keeps the Classical.choose root opaque and uses the equation and square-root brackets to obtain a quantitative normalized root error. The qualitative limits in this module are not substituted for that error.

References