Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual Cylinder Averages

Abstract

Actual normalized cylinder integrals define a finite average operator on the original biased boundary Hilbert space. Prefix freedom makes it the orthogonal projection onto the cylinder span.

Definition 1.1 (atomMean).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCylinderProjection.atomMean

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCylinderProjection.atomMean (✓ std3).

Source. Repository-derived.

Commentary.

For a nonempty original address p, atomMean(p) is the inner product with the actual cylinder indicator, divided by the actual M mass of that cylinder. It is a continuous real functional on the original L2(M).

Definition 1.2 (Q).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCylinderProjection.Q

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCylinderProjection.Q (✓ std3).

Source. Repository-derived.

Commentary.

For a finite set A of original nonempty addresses, Q(A) is the sum over p in A of the actual cylinder indicator multiplied by atomMean(p). The operator is constructed as a finite sum of continuous linear maps.

Definition 1.3 (V).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCylinderProjection.V

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCylinderProjection.V (✓ std3).

Source. Repository-derived.

Commentary.

V(A) is the real linear span in the original L2(M) of the actual indicators of the cylinders with addresses in A.

Definition 1.4 (V0).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCylinderProjection.V0

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCylinderProjection.V0 (✓ std3).

Source. Repository-derived.

Commentary.

V0(A) is the kernel of the actual mean restricted to V(A). Its elements are exactly the vectors in the actual cylinder span whose original M mean is zero.

Theorem 1.5 (Original Cylinders and Ray Prefixes).

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

Source. Repository-derived.

Commentary.

For every original address p and ray omega, omega lies in the actual cylinder of p precisely when p is the prefix of omega of length length(p). This includes the empty address. The cylinder prescribes the same initial coordinates as the list constructed by rayPrefix, so equality follows by comparing every list entry.

This correspondence converts a unique prefix on each ray into a unique actual cylinder containing that ray. In particular it identifies the product-tree mass frontier with a covering of the original Bernoulli boundary.

Theorem 1.6 (Normalized Means and Orthogonal Projection).

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

Source. Repository-derived.

Commentary.

For every finite A whose original addresses are prefix-free, atomMean(p)(F) equals the integral of F over the actual cylinder divided by its actual positive M mass, for every original nonempty p and every F in the original G. It also equals the mean of the actual conditional pullback of F to suffix rays.

For every original F, Q(A)F is exactly the orthogonal projection of F onto V(A). In particular Q(A) fixes each indicator indexed by A. The cylinder span is finite dimensional.

Two distinct prefix-free addresses have disjoint actual cylinders. Their indicators are therefore orthogonal, their squared norms are their actual cylinder masses, and each normalized atom mean extracts its own indicator coefficient. Thus Q(A)F lies in the span and F minus Q(A)F is orthogonal to that span, which characterizes the projection.

The actual normalized integral is related to suffix composition by the original measure-preserving map from M to the conditional cylinder law. No preservation of the ambient measure M by prepending is asserted.

Theorem 1.7 (The Exact Partition Residual).

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

Source. Repository-derived.

Commentary.

Suppose the finite prefix-free family A covers every original infinite ray. For every p in A and every F in G, the conditional pullback of Q(A)F is the actual constant with value atomMean(p)(F). Consequently, for every original z in H, the conditional pullback of Cz minus Q(A)Cz equals exactly C(S(p)z).

For every F in the original G, its squared norm equals the sum over A of the actual cylinder mass times the squared norm of its conditional pullback. Apply the measure-preserving identification with the normalized restriction separately on each cylinder, then sum the disjoint cylinder integrals over the covering partition. Applying this identity to Cz minus Q(A)Cz gives exactly the weighted sum of the squared norms of C(S(p)z).

The same constructed Q(A) fixes every actual constant and commutes with Pi. The constant identity follows by summing its actual atom values on the partition. Orthogonal symmetry then shows that Q(A) preserves the actual mean, and the formula for Pi gives commutation.

The dimension of V(A) is exactly the number of addresses in A. Indeed applying each actual atom mean to a linear relation among the indicators extracts that indicator’s coefficient, so the indicators are linearly independent. The actual mean restricted to V(A) is nonzero because the actual constant one lies in V(A) and has mean one. Rank-nullity therefore gives dimension card(A) minus one for the actual mean-zero subspace V0(A).

Theorem 1.8 (An Actual Mass Threshold Bound).

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

Source. Repository-derived.

Commentary.

Let t be nonnegative. If every actual M cylinder mass in the finite prefix-free covering family A is at most t, then for every original z in H the squared norm of Cz minus Q(A)Cz is at most the golden ratio times t times the squared norm of z. This follows by applying the weighted disjoint-suffix estimate to the exact residual decomposition.

The hypothesis is a bound on the actual cylinder masses. Applying this theorem to every weak first mass crossing for zero less than t less than one additionally requires identifying the actual Bernoulli cylinder masses with the frozen product-mass frontier. The all-threshold specialization, the covariance equality and the spectral counting conclusions are not asserted here.

References