Positive Ledger-Length Growth

Abstract

A positive generation strictly increases every additive real ledger length.

Theorem 1.1 (Positive generation strictly increases ledger length).

$L(u)>0\Rightarrow L(a)<L(a+u)$

Proof. Machine-checked in Lean as D5/S3/Analytic/LedgerLengthGrowth.ledger_length_strict_mono_of_positive_generation (✓ std3). ∎

Source. Repository-derived.

Commentary.

正生成之正性以 length u > 0 承载(素指数求和的具体形属素账本载体,另单);推论中“逆账本/群化扩张“属 open 账,留叙事层不入定理。

References

• Truth anchor: D5/S3/Analytic/LedgerLengthGrowth.ledger_length_strict_mono_of_positive_generation
• Dependency: D5/S3/Weil/LabeledZeta