Off-Line Scaling Ledger Growth

Abstract

Off-line nonempty ledger entries share a sign and grow unbounded under scaling.

Theorem 1.1 (Off-line nonempty ledgers have one sign and unbounded multiples).

$$\forall A[\mathrm{AddMonoid}(A)],\forall \ell :A{\to }_{+}\mathbb{R},\forall s\in \mathbb{C},\Re (s)\ne \frac{1}{2}\Rightarrow (\forall a\in A,0<\ell (a)\Rightarrow \mathrm{scalingLedger}(\ell ,s,a)\ne 0)\wedge (\forall a,b\in A,0<\ell (a)\Rightarrow 0<\ell (b)\Rightarrow (0<\mathrm{scalingLedger}(\ell ,s,a)\iff 0<\mathrm{scalingLedger}(\ell ,s,b)))\wedge (\forall a\in A,\forall m\in \mathbb{N},\mathrm{scalingLedger}(\ell ,s,m\cdot a)=m\mathrm{scalingLedger}(\ell ,s,a))\wedge (\forall a\in A,0<\ell (a)\Rightarrow \forall C\in \mathbb{R},\exists m\in \mathbb{N},C<|\mathrm{scalingLedger}(\ell ,s,m\cdot a)|)$$

Proof. Machine-checked in Lean as D5/S3/Midline/OffLineScaling.off_line_scaling_ledger_growth (✓ std3). ∎

Source. Repository-derived.

Commentary.

For an additive ledger length and a spectral parameter off the critical line, every positive-length entry is nonzero, any two positive-length entries have the same sign, natural scaling multiplies each entry by the same natural number, and the absolute values along those multiples are unbounded. This is a coordinatewise fact only, not a claim about the sum after analytic continuation; cancellation of that sum is treated separately.

References

• Truth anchor: D5/S3/Midline/OffLineScaling.off_line_scaling_ledger_growth
• Dependency: D5/S3/Zeros/ZeroGeometry