Serial checkpointed-image final3 on Modal

• Verdict: FULL PASS: every layer checkpointed, verification clean
• Run id 20260928t220203, Modal app id ap-7zxzQj0YqTwlQUP6P06ecn (profile teal-sea)
• Source HEAD 5522b96314f7f63198ae3ec4e71d954255f93d1a; client: client exit 0
• Wall (image prep + build + teardown): 920.9 s of 9600 s bound; after teardown: none active

Layer receipts (exact, in build order; one lake build at a time)

Source hashes

• local fp a72e89fc0b5f1d72a41d17ef5f5b7be892b238f15668384dd866382fe8962c82 / bridge a4931d8311da41b1a41cba4f63cda6a0313167bc447ad1674d28159a92f8d2ff
• remote (preflight, before any Lean) fp a72e89fc0b5f1d72a41d17ef5f5b7be892b238f15668384dd866382fe8962c82 / bridge a4931d8311da41b1a41cba4f63cda6a0313167bc447ad1674d28159a92f8d2ff, equal: True
• remote token scan: {'fp_hits': [], 'bridge_hits': [], 'string_hits': [], 'unterminated': []}
• remote (final verify) fp a72e89fc0b5f1d72a41d17ef5f5b7be892b238f15668384dd866382fe8962c82 / bridge a4931d8311da41b1a41cba4f63cda6a0313167bc447ad1674d28159a92f8d2ff
• toolchain file leanprover/lean4:v4.33.0-rc2; lean --version: Lean (version 4.33.0-rc2, x86_64-unknown-linux-gnu, commit d8b18978322de05a8f3dba51ef03cf5461676c17, Release)
• oleans unchanged since their layer: {'/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Base.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells0.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells1.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells2.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells3.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells4.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells5.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells6.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells7.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells8.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells9.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells10.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells11.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells12.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells13.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells14.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells15.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells16.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells17.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells18.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells19.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells20.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells21.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells22.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells23.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells24.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells25.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cells.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Cover.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks0.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks1.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks2.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks3.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks4.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks5.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks6.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks7.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks8.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks9.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks10.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks11.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks12.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks13.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks14.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Chunks15.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Boxes.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand/Main.olean': True, '/repo/hunts/ainta_seven_point/lean-four-point/.lake/build/lib/lean/FourPointCand.olean': True}
• oleans for targets that should NOT exist: []
• verify problems: []
• axiom audit ok: True

Raw axiom lines from Main:

info: FourPointCand/Main.lean:206:0: 'Zeta23Ext.Bridge.FourPoint.F4_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FourPointCand/Main.lean:207:0: 'Zeta23Ext.Bridge.FourPoint.cover1' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FourPointCand/Main.lean:208:0: 'Zeta23Ext.Bridge.FourPoint.four_point_cert' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FourPointCand/Main.lean:209:0: 'Zeta23Ext.Bridge.FourPoint.Phi_four' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FourPointCand/Main.lean:210:0: 'Zeta23Ext.Bridge.FourPoint.four_point_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FourPointCand/Main.lean:211:0: 'Zeta23Ext.Bridge.FourPoint.four_point_bound_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]

Exact Main theorem statements (from the verified sources):

-- Main.lean
theorem F4_eq (p : ℕ) (g : Fin 3 → ℝ) :
    F 4 p g = (1/(p:ℝ)) * (g 0 + g 1 + g 2)
      + 2/3 * wfun (g 0) + 2/3 * wfun (g 1) + 2/3 * wfun (g 2)
      + wfun (g 0 + g 1) + wfun (g 1 + g 2) + 2 * wfun (g 0 + g 1 + g 2)
-- Cover.lean
theorem cover1 (x : ℝ) (h0 : 0 ≤ x) (hS : x ≤ (233/40:ℝ)) :
    (699/200000:ℝ) ≤ wfun x ∨ ((63/64:ℝ) ≤ x ∧ x ≤ (73/64:ℝ)) ∨ ((121/64:ℝ) ≤ x ∧ x ≤ (141/64:ℝ)) ∨ ((179/64:ℝ) ≤ x ∧ x ≤ (105/32:ℝ)) ∨ ((237/64:ℝ) ≤ x ∧ x ≤ (233/40:ℝ))
-- Main.lean
theorem four_point_cert :
    ∀ g : Fin (4-1) → ℝ, (∀ i, 0 ≤ g i) → (2330/1000000:ℝ) ≤ F 4 2500 g
-- Main.lean
theorem Phi_four : Phi_n 4 (2330/1000000:ℝ) 432 2500 = (14400000 * HD 1 - 17240) / 14366681
-- Main.lean
theorem four_point_bound :
    ∀ ε > 0, ∃ T₀ : ℝ, ∀ T ≥ T₀,
      ((14400000 * HD 1 - 17240) / 14366681 - ε) * (Ncount T (2 * T) : ℝ)
        ≤ N0simple T (2 * T)
-- Main.lean
theorem four_point_bound_ratio :
    ∀ ε > 0, ∃ T₀ : ℝ, ∀ T ≥ T₀,
      (14400000 * HD 1 - 17240) / 14366681 - ε
        ≤ (N0simple T (2 * T) : ℝ) / (Ncount T (2 * T) : ℝ)

Cost

• Metered lower bound from receipts: 20886 s x $4.396e-05/s (2 cores, 8 GiB, live modal.com/pricing) = $0.918; excludes image prep and container start.
• Worst case at the wall bound: 9600 s x $4.396e-05/s = $0.422.

Scope

Local compile record only. No publication, no PR, no public claim. Pending external verification.

Complete client stdout+stderr: <PRIVATE-LOCAL-SCRATCH>/zeta-fourpoint-serial/logs/launch-20260928t220203.log

Driver

driver 20260928t220203

• app: fourpoint-serial-20260928t220203 id ap-7zxzQj0YqTwlQUP6P06ecn
• client exit 0
• wall elapsed (incl. teardown): 920.9 s (bound 9600 s)
• after teardown: none active
• full client stdout+stderr: <PRIVATE-LOCAL-SCRATCH>/zeta-fourpoint-serial/logs/launch-20260928t220203.log
• last receipt in log: 48 WholeLibrary
• last saved image in log: im-6OZMQf9oFxqLnic4UBo4mf
• FPVERIFY ok: True (client exit code alone is not proof; only FPVERIFY ok=True over all receipts is)