Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Disjoint Strict-Suffix Energy

Abstract

Distinct prefix-free stopping addresses have disjoint strict-descendant coordinates in the original increment space. Their suffix energies therefore fit inside the original energy.

Theorem 1.1 (Disjoint Original Edge Coordinates).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundarySuffixEnergy.prefix_free_suffix_energy (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let A be any finite prefix-free set of original addresses and let z be any vector in the original square-summable edge space H. Then the sum over A of the squared norms of S(p)z is at most the squared norm of z. Nonempty suffixes are used throughout, so the edge ending at p is excluded.

The map sending a pair consisting of p in A and a nonempty suffix u to the original edge pu is injective. If two such edges agreed, their prefixes would be comparable; prefix freedom would force the prefixes to agree, and cancellation would force the suffixes to agree. The resulting subseries of the nonnegative squared edge coordinates is bounded by the complete energy series. This argument applies directly to every z in H.

Theorem 1.2 (Weighted Actual Centered Suffixes).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundarySuffixEnergy.weighted_centered_suffix_energy (✓ std3). ∎

Source. Repository-derived.

Commentary.

Suppose t is nonnegative and each weight w(p), for p in A, lies between zero and t. For the actual centered trace C on the original biased boundary, the sum of w(p) times the squared norm of C(S(p)z) is at most the golden ratio times t times the squared norm of z.

Apply the actual conditional centering identity and its Hardy estimate to each suffix, use w(p) at most t, and then apply the disjoint strict-suffix energy estimate. The weights can be actual cylinder masses whenever their threshold bound has been established.

This estimate supplies the suffix-energy inequalities in a stopping argument. Identifying this weighted sum with the norm of the global atom-average residual requires the actual cylinder projection and its conditional norm decomposition. No assertion about the covariance or the spectral counting function follows here alone.

References