Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual Covariance and the Free-Root Form

Abstract

The infinite path trace on the fixed biased boundary has compact covariance. The original free-root energy infimum is attained in the effective increment space, and its weak variational graph is determined by the actual covariance.

Definition 1.1 (v).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.v

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.v (✓ std3).

Source. Repository-derived.

Commentary.

The vector v is the adjoint of the actual bounded path trace J applied to the constant one in G=L2(M). The biased product measure and the infinite square-summable increment space are fixed throughout.

Definition 1.2 (Sigma).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.Sigma

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.Sigma (✓ std3).

Source. Repository-derived.

Commentary.

Sigma=C* C acts on the original infinite increment space H, where C=Pi J is included in the original ambient G. Taking this ambient adjoint is the same as extending the adjoint from the mean-zero boundary subspace by zero on constants.

Definition 1.3 (K).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.K

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.K (✓ std3).

Source. Repository-derived.

Commentary.

K is the orthogonal complement of the kernel of Sigma. Vectors in the edge kernel are excluded from this effective increment space.

Theorem 1.4 (Mean of a Boundary Cylinder Indicator).

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

Source. Repository-derived.

Commentary.

For every nonempty edge address p, the mean of its original boundary cylinder indicator is the real measure M([p]). The mean and indicator use the same biased boundary measure M.

Applying the cylinder mass formula gives the corresponding edge coordinate of v=J*1. These coordinates identify the limiting mean vector and distinguish its nonzero boundary values.

Theorem 1.5 (Compact Trace and Actual Covariance).

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

Source. Repository-derived.

Commentary.

For every positive epsilon, choose a stopping threshold at most both one half and epsilon squared divided by four times the golden ratio. The all-vector stopping residual bounds the operator norm of C minus Qt C by epsilon over two. The actual stopping range is finite dimensional, so norm closure of compact operators gives compactness of C. The difference J-C factors through the one-dimensional constant space; consequently J is compact too, and composing C with its bounded adjoint makes Sigma compact.

Self-adjoint centering and its idempotence give Sigma=J* J-v tensor v. For all z,w in H the bilinear covariance equals the inner product of their actual centered traces. In particular its quadratic form is the squared centered trace norm, and its kernel is exactly the kernel of C. On every pair of original unit edge vectors p,q, its entry is M([p] intersect [q])-M([p])M([q]).

Theorem 1.6 (Centering Has Zero Mean).

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

Source. Repository-derived.

Commentary.

Orthogonal centering subtracts the original integral mean, so every centered boundary vector has mean zero.

This is the mean-zero codomain condition for the actual centered trace.

The original BiasedBoundaryCentering.Pi_const identity removes every actual constant. In the free-root form, constants therefore require no effective increment.

Theorem 1.7 (Idempotent Centering).

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

Source. Repository-derived.

Commentary.

A centered vector already has zero mean, so centering it again leaves it fixed.

This identity identifies covariance graph coordinates with centered boundary vectors.

Theorem 1.8 (The Adjoint Lies in the Effective Edge Space).

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

Source. Repository-derived.

Commentary.

Every vector C*h is orthogonal to the original covariance kernel because pairing it with an edge vector z equals pairing h with Cz.

This effective-space inclusion is consumed by the positive eigenspace identification of the original boundary operator.

Theorem 1.9 (Pairing with a Mean-Zero Vector).

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

Source. Repository-derived.

Commentary.

A vector with zero mean is orthogonal to constants. Its inner product with any centered test vector equals its inner product with the original test vector.

The identity applies to every test vector in the original boundary L2 space.

Theorem 1.10 (Projection Removes Only the Trace Kernel).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.C_project

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

Source. Repository-derived.

Commentary.

For every original edge vector z, the centered trace of the orthogonal projection of z onto K equals C(z). The removed vector lies in the covariance kernel, which equals the kernel of the centered trace.

Definition 1.11 (D).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.D

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.D (✓ std3).

Source. Repository-derived.

Commentary.

The domain D is exactly the subspace of all F=c times the constant one plus Jz, with arbitrary real root value c and arbitrary z in the original infinite H. No finite-level restriction or replacement measure enters this domain.

Definition 1.12 (energy).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.energy

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.energy (✓ std3).

Source. Repository-derived.

Commentary.

For an ambient F in G, energy(F) is the real infimum of the set of squared increment norms over all original representations F=constG(c)+Jz. Its asserted energy interpretation is restricted to F in D, where the set is nonempty and the infimum is attained.

Definition 1.13 (lift).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.lift

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.lift (✓ std3).

Source. Repository-derived.

Commentary.

For each F in D, lift(F) is the unique z in K such that Cz=Pi F. Orthogonal projection onto K removes exactly the redundant edge kernel.

Theorem 1.14 (Attainment of the Original Energy).

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

Source. Repository-derived.

Commentary.

For any representation F=constG(c)+Jz, the least increment is the orthogonal projection of z onto K. Projection leaves its centered trace unchanged and decreases its norm. Injectivity of C on K makes this increment independent of the chosen representation and unique in K.

The root coefficient is restored as mean(F)-mean(J lift(F)). This is an actual original representation and attains the infimum, so energy(F)=the squared norm of lift(F). Every other representation is included in the comparison.

Definition 1.15 (form).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.form

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.form (✓ std3).

Source. Repository-derived.

Commentary.

The form pairing of F and T in D is the real inner product of their least increments. Its diagonal is the original infimum energy, and its value is one quarter of energy(F+T)-energy(F-T), so it is the polarization of that original energy.

Definition 1.16 (weakGraph).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.weakGraph

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.weakGraph (✓ std3).

Source. Repository-derived.

Commentary.

The pair (u,h) lies in the weak graph when u belongs to the original D and the form pairing of u with every F in D equals the G inner product of h with F.

Definition 1.17 (formSpace).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.formSpace

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.formSpace (✓ std3).

Source. Repository-derived.

Commentary.

The form domain in graph coordinates consists exactly of pairs (F,z) in G times the original H with z in K and Cz=Pi F. It is the closed graph of the unique least increment, hence is complete for the inherited product norm. Its increment norm squared is the original energy.

Definition 1.18 (formInclusion).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.formInclusion

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryFreeRootForm.formInclusion (✓ std3).

Source. Repository-derived.

Commentary.

The inclusion of the original form domain into G is the first-coordinate map on formSpace. Its second-coordinate map is the unique least increment.

Theorem 1.19 (The Entire Weak Variational Graph).

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

Source. Repository-derived.

Commentary.

The form diagonal equals the original free-root energy on every element of D. Uniqueness of the effective lift makes it additive and subtractive; the real inner-product polarization identity identifies this pairing with the polarization of the original infimum. The graph of F mapped to (F,lift(F)) is closed in G times H: it is exactly the closed constraint set z in K and Cz=Pi F. In these complete graph coordinates, the actual inclusion equals the compact map C applied to the increment coordinate plus the constant map applied to the mean of the trace coordinate. Thus the original form-domain inclusion is compact. The weak equation holds for all original traces exactly when mean(h)=0 and u=constG(mean(u))+CCh. Testing constants forces mean(h)=0; testing every Jz identifies the least increment of u with Ch. Conversely C*h belongs to K, and the stated covariance representation satisfies the equation against every F in D.

This module characterizes the entire weak graph without assuming an operator realization. BiasedBoundaryOperator constructs its dense self-adjoint realization, compact resolvent and positive covariance eigenspace identification. The complete ordered spectral sequence, the unitary polar map, its two range-domain identities and global eigenvalue counting require additional arguments.

References