Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Centering and Conditional Suffix Residuals

Abstract

Actual integral centering on the biased boundary cancels both the finite prefix constant and the global centering constant in every conditional suffix trace.

Definition 1.1 (mean).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCentering.mean

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCentering.mean (✓ std3).

Source. Repository-derived.

Commentary.

The mean functional is the L2 inner product with the actual constant one. Since M is a probability measure, this constant has norm one and the functional equals the actual integral with respect to M.

Definition 1.2 (Pi).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCentering.Pi

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCentering.Pi (✓ std3).

Source. Repository-derived.

Commentary.

Pi is the orthogonal projection onto the orthogonal complement of the span of the actual constant one. Its ambient formula is F minus the constant function with value mean(F).

Definition 1.3 (C).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCentering.C

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryCentering.C (✓ std3).

Source. Repository-derived.

Commentary.

The centered trace is C=Pi composed with the original J. Its values are included in the original ambient G when conditional pullbacks are applied.

Theorem 1.4 (The Boundary Constant Has Unit Norm).

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

Source. Repository-derived.

Commentary.

The original Bernoulli boundary law is a probability measure, so its constant one has L2 norm one.

Theorem 1.5 (Constants Are Removed by Centering).

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

Source. Repository-derived.

Commentary.

For every real c, the original mean of constG(c) is c. The formula for Pi subtracts that same constant and gives zero. This identity removes constants in the centered suffix, free-root form and boundary operator.

Theorem 1.6 (The Actual Centered Suffix).

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

Source. Repository-derived.

Commentary.

For every F in G the mean equals its M integral, mean sends the constant c to c, and Pi subtracts that constant mean. Orthogonal projection makes Pi a contraction.

For every original finite prefix p and every original z in H, first pulling back Cz and then centering in the suffix L2(M) gives exactly C applied to the strict suffix vector S(p)z. Conditional composition fixes constants. The all-vector path split therefore cancels both the finite prefix sum and the constant subtracted by global centering.

The squared norm of this centered conditional suffix is at most the golden ratio times the squared norm of S(p)z. This follows from the contraction of Pi and the original all-vector Hardy bound for J, using the original golden biased parameter.

This statement concerns centering in a fixed conditional suffix space for each p. Identifying the global stopping-cylinder atom-average operator, summing the weighted conditional norms, and proving the global threshold bound require further results. No covariance or spectral counting assertion is made.

References