Proof. Machine-checked in Lean as D5/S3/Analytic/Dilation/PartialCircleBoundaryDefect.partial_circle_boundary_defect (✓ std3). ∎
Source. Repository-derived.
Commentary.
The two real embeddings, anisotropic form, golden-unit zeta, break field, and accumulated arc defect are all constructed explicitly on the nonzero integer-pair lattice.
The source restricts the identity to a convergence region where termwise differentiation is permitted. The displayed derivative and interval-integrability premises encode exactly that analytic scope, including the necessary nonzero spectral parameter.
The fundamental theorem of calculus gives the endpoint difference. For an arc of one complete regulator period, the imported exact lattice reindexing identifies the endpoints and the defect vanishes.