Cross-Engine Admission Contracts for Autonomous Formalization

Lean kernel validity, permitted axiom provenance, and statement faithfulness require distinct checks. We differentially test admission-policy adapters from three formalization pipeline snapshots on 47 declarations (39 bad, 8 good). Their strongest measured configurations admit 18/39 (46%), 10/39 (26%), and 11/39 (28%) bad cases, with false rejection of 0/8, 4/8, and 0/8 good cases. Allowlist plus fixed-target comparison admits the five constructed informal-intent mismatches. In five target-substitution cases, candidate-owned comparison admits every attack; base-owned comparison rejects every attack and accepts five matching controls. These historical closure measurements do not establish kernel integrity: the recommended contract composes independent kernel replay, allowed-dependency checks, and comparison with a trusted target. Recent trureturing cases demonstrate source-bound formal refutations and reviewed source-to-formal interpretation. The contribution is a reproducible comparison of deployed policy families and repository evidence, connecting existing verification mechanisms to the admission decisions mathematical-agent pipelines must make.