Formalization / certificates

release check (final)

Verbatim copy of ~/prove2me_workspace/final/unified/logs/release_check_v1_1.txt (file time 2026-10-17 05:51 UTC). raw.

== (1) lake build
PASS: Build completed successfully (3475 jobs).
== (2) axioms
PASS: 12/12 main theorems use only [propext, Classical.choice, Quot.sound]
== (3) statement preservation
FAIL: preservation (0/3)
== (4) forbidden tokens
PASS: no sorry/admit/native_decide/axiom/maxHeartbeats
== (5) warnings
PASS: 0 build warnings
== lines: 50636 (SurfaceBlowup), 2238 (Tests); modules: 69
RELEASE CHECK: FAILURES
RC_EXIT=1

NOTE (orchestrator, 2026-10-17): check (3) could not run because the certified trees' build caches
(final/monolith_gen, monolith_recip, monolith: .lake) were deleted with the owner's permission after v1.0.0.
Substitute evidence: SurfaceBlowup/Basic.lean, SurfaceBlowup/Main.lean and SurfaceBlowup/Reciprocity/Main.lean
are byte-identical to tag v1.0.0 (cmp), for which the kernel-level preservation check passed 3/3
(logs/release_check_c4d.txt). The only pre-existing Lean files changed in v1.1 are the umbrella files
SurfaceBlowup.lean, Tests.lean (new imports), Checks/Axioms.lean (8 more #print axioms) and
Tests/Regression.lean (`single_two_law` made public, statement unchanged).