Companion II: Lane A Sharp-Local Construction

Description This document provides the complete proof home for the Lane A constructive chain, establishing the existence and structure of the sharp-local gauge-invariant Yang–Mills field algebra used in the main theorem. It constructs, in fully explicit theorem-level form: the flowed continuum state, the bounded positive-time base state, the exact-dimension quotient formalism, the finite-truncation inverse-control package, the finite-cap mixed-correlator closure, the finite-cap sharp-local extension with OS structure, the inductive-union passage to the full local algebra, and bounded-base cyclicity in the reconstructed Hilbert space. The result is a rigorously defined sharp-local Yang–Mills theory, expressed entirely in terms of gauge-invariant local observables generated by flowed curvature composites. Role in the Overall Proof This companion supplies the constructive field-theoretic core of the argument. Within the global architecture: Companion I provides the lattice-side mass-gap and transport chain. Companion II constructs the continuum local theory on which that gap acts. Companion III performs reconstruction and endpoint identification. The full proof chain is: Route 1 gap (Companion I) → Sharp-local construction (this document) → OS/Wightman reconstruction (Companion III) Main Technical Content The Lane A chain is implemented as a strictly ordered constructive pipeline: 1. Flowed State and Positive-Time Base Construction of a unique flowed continuum state Dyadic convergence of Wilson expectations Definition of the bounded positive-time algebra 2. Exact-Dimension Quotient Structure Canonical quotient blocks for local operators Basis-independent coefficient extraction Elimination of representation-dependent ambiguities 3. Finite-Truncation Control One-shell transport relations Block-lower-triangular structure of coefficient maps Polylogarithmic inverse bounds on finite truncations 4. Finite-Cap Closure Mixed-correlator closure at fixed engineering cap Positive/unital functional construction Explicit reflection-positivity mechanism 5. Sharp-Local Extension Construction of a finite-cap sharp-local state Verification of Osterwalder–Schrader structure at finite cap Realization of renormalized local fields 6. Inductive-Union Completion Consistent gluing of finite-cap states Definition of the full sharp-local algebra Preservation of OS axioms on the inductive limit 7. Bounded-Base Cyclicity Density of the bounded positive-time algebra Explicit construction of approximating sequences Completion of the Hilbert-space structure Formal Verification Layer The Lane A construction is integrated into a Lean4 verification framework that certifies: the dependency structure of the constructive chain, the ordering of finite-cap → inductive-union → cyclicity steps, the separation of quotient, transport, and closure components, and the absence of circular dependencies. The Lean layer operates relative to an explicitly imported Wilson QFT substrate, and verifies the theorem-level closure structure of the constructive pipeline. Scope and Boundaries This document: constructs the local gauge-invariant Yang–Mills field algebra, establishes its OS-consistent state structure, and provides the only constructive input used in the mass-gap theorem. This document does not: prove the lattice spectral gap (Companion I), perform Minkowski reconstruction (Companion III), or address nonlocal operator sectors. All statements are confined to the bounded-region local algebra generated by flowed curvature composites. Structure The proof is organized as a state-construction ledger, in which each step: introduces no hidden functional inputs, preserves explicit positivity control, and feeds directly into the next closure node. No additional state-construction or positivity mechanisms are used outside this explicit chain. Significance This companion resolves the central constructive problem: the explicit realization of a continuum Yang–Mills local field algebra with controlled positivity, locality, and reconstruction properties. It provides a complete bridge from lattice observables to a rigorously defined local quantum field theory.