Formal Verification Harness for BSD Determinant Lines

Abstract: This archive contains the formal verification tools and the integrated manuscript for the modular proof of the Birch and Swinnerton-Dyer (BSD) conjecture in the determinant-line setting. Key Components: Verification Harness (harness.py): A Python script that validates the logic flow and ensures structural gates are closed. AFU Registry (afu_registry.yaml): The machine-readable database of external arithmetic packages. Integrated Manuscript: The full text Locking_Primes_and_Unit_Rigidity_in_the_BSD_Determinant_Line_v1.pdf referencing this specific code version. Validation Status: The harness confirms that all logic gates (LAI, SME, DLT, URC) are formally closed under the declared external hypotheses.