Audit final Geode5 theorem

[DomTheDeveloper]

Compiles the immutable DTD Formal Conjectures head 89a8f3c8de74039ab989100c27a6bf24234556f8 and rejects actual Lean placeholders before checking FormalConjectures/Arxiv/2508.10245/Geode5.lean. This PR contains only the audit trigger.

[github-actions]

Geode5 immutable final audit

Target: DomTheDeveloper/formal-conjectures@89a8f3c8de74039ab989100c27a6bf24234556f8
Module: FormalConjectures/Arxiv/2508.10245/Geode5.lean
Result: failure

FormalConjectures/Arxiv/2508.10245/Geode5.lean:17:0: error: unknown module prefix 'FormalConjectures'

No directory 'FormalConjectures' or file 'FormalConjectures.olean' in the search path entries:
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Cli/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/batteries/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Qq/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/aesop/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/proofwidgets/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/importGraph/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/LeanSearchClient/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/plausible/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/mathlib/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean
/home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/lib/lean
/home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/lib/lean

[github-actions]

Geode5 immutable final audit

Target: DomTheDeveloper/formal-conjectures@89a8f3c8de74039ab989100c27a6bf24234556f8
Module: FormalConjectures.Arxiv.«2508.10245».Geode5
Lake build: failure
Warnings-as-errors recheck: skipped

✖ [277/627] Building FormalConjectures.Arxiv.«2508.10245».Geode5Defs (181ms)
trace: .> LEAN_PATH=/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/bin/lean /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/FormalConjectures/Arxiv/2508.10245/Geode5Defs.lean -o /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean/FormalConjectures/Arxiv/2508.10245/Geode5Defs.olean -i /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean/FormalConjectures/Arxiv/2508.10245/Geode5Defs.ilean -c /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/ir/FormalConjectures/Arxiv/2508.10245/Geode5Defs.c --setup /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/ir/FormalConjectures/Arxiv/2508.10245/Geode5Defs.setup.json --json
error: FormalConjectures/Arxiv/2508.10245/Geode5Defs.lean:17:0: unknown module prefix 'FormalConjecturesUtil'

No directory 'FormalConjecturesUtil' or file 'FormalConjecturesUtil.olean' in the search path entries:
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Cli/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/batteries/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Qq/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/aesop/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/proofwidgets/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/importGraph/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/LeanSearchClient/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/plausible/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/mathlib/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean
/home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/lib/lean
error: Lean exited with code 1
✔ [7892/7919] Built FormalConjectures.Arxiv.«2508.10245».Geode5Proof.MoreCertificateData (5.1s)
✔ [7893/7919] Built FormalConjectures.Arxiv.«2508.10245».Geode5Proof.CertificateData (7.4s)
ℹ [7894/7919] Built FormalConjectures.Arxiv.«2508.10245».Geode5Proof.MomentAlgebra (7.5s)
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentAlgebra.lean:115:0: 'Arxiv.«2508.10245».Geode5Proof.moment_division_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentAlgebra.lean:116:0: 'Arxiv.«2508.10245».Geode5Proof.momentQuotient_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentAlgebra.lean:117:0: 'Arxiv.«2508.10245».Geode5Proof.recurrenceDiagonal_product' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [7895/7919] Built FormalConjectures.Arxiv.«2508.10245».Geode5Proof.CRT (7.1s)
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/CRT.lean:82:0: 'Arxiv.«2508.10245».Geode5Proof.residueModuli_pairwise_coprime' depends on axioms: [Lean.ofReduceBool,
 Lean.trustCompiler]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/CRT.lean:83:0: 'Arxiv.«2508.10245».Geode5Proof.answer_modEq_residue' depends on axioms: [Lean.ofReduceBool, Lean.trustCompiler]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/CRT.lean:84:0: 'Arxiv.«2508.10245».Geode5Proof.upperBound_lt_certificateModulus' depends on axioms: [propext,
 Lean.ofReduceBool,
 Lean.trustCompiler]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/CRT.lean:85:0: 'Arxiv.«2508.10245».Geode5Proof.eq_answerValue_of_residues_of_lt_upperBound' depends on axioms: [propext,
 Classical.choice,
 Lean.ofReduceBool,
 Lean.trustCompiler,
 Quot.sound]
ℹ [7896/7919] Built FormalConjectures.Arxiv.«2508.10245».Geode5Proof.Integral (9.4s)
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/Integral.lean:91:0: 'Arxiv.«2508.10245».Geode5Proof.integral01_derivative' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [7897/7919] Built FormalConjectures.Arxiv.«2508.10245».Geode5Proof.Recurrence (11s)
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/Recurrence.lean:130:0: 'Arxiv.«2508.10245».Geode5Proof.qMoment_recurrence_raw' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [7901/7919] Built FormalConjectures.Arxiv.«2508.10245».Geode5Proof.RemainderTables (23s)
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RemainderTables.lean:168:0: 'Arxiv.«2508.10245».Geode5Proof.momentRemainder_eq_r0' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RemainderTables.lean:169:0: 'Arxiv.«2508.10245».Geode5Proof.momentRemainder_eq_r1' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RemainderTables.lean:170:0: 'Arxiv.«2508.10245».Geode5Proof.momentRemainder_eq_r2' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RemainderTables.lean:171:0: 'Arxiv.«2508.10245».Geode5Proof.momentRemainder_eq_r3' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RemainderTables.lean:172:0: 'Arxiv.«2508.10245».Geode5Proof.momentRemainder_eq_r4' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [7902/7919] Built FormalConjectures.Arxiv.«2508.10245».Geode5Proof.RecurrenceStep (18s)
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceStep.lean:168:0: 'Arxiv.«2508.10245».Geode5Proof.integral01_qSparsePolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceStep.lean:169:0: 'Arxiv.«2508.10245».Geode5Proof.integral01_qMomentQuotient' depends on axioms: [propext, Classical.choice, Quot.sound]
✖ [7903/7919] Building FormalConjectures.Arxiv.«2508.10245».Geode5Proof.MomentFormula (6.9s)
trace: .> LEAN_PATH=/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/bin/lean /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.lean -o /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean/FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.olean -i /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean/FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.ilean -c /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/ir/FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.c --setup /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/ir/FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.setup.json --json
error: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.lean:54:18: unsolved goals
case add.h_add
A m : ℕ
p q : Polynomial ℚ
hp : ((Polynomial.X + 1) ^ A * p.comp (Polynomial.X + 1)).coeff m = p.sum fun j a ↦ a * ↑((A + j).choose m)
hq : ((Polynomial.X + 1) ^ A * q.comp (Polynomial.X + 1)).coeff m = q.sum fun j a ↦ a * ↑((A + j).choose m)
⊢ ∀ (a : ℕ) (b₁ b₂ : ℚ), (b₁ + b₂) * ↑((A + a).choose m) = b₁ * ↑((A + a).choose m) + b₂ * ↑((A + a).choose m)
error: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.lean:61:23: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  Polynomial.C ?m.120 * Polynomial.C ?m.121
in the target expression
  ((Polynomial.X + 1) ^ A * Polynomial.C a * (Polynomial.X + 1) ^ n).coeff m =
    ((Polynomial.monomial n) a).sum fun j a ↦ a * ↑((A + j).choose m)

case monomial
A m n : ℕ
a : ℚ
⊢ ((Polynomial.X + 1) ^ A * Polynomial.C a * (Polynomial.X + 1) ^ n).coeff m =
    ((Polynomial.monomial n) a).sum fun j a ↦ a * ↑((A + j).choose m)
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.lean:75:0: 'Arxiv.«2508.10245».Geode5Proof.shifted_coefficient_eq_sum' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.lean:76:0: 'Arxiv.«2508.10245».Geode5Proof.momentCoefficient_eq_extractionSum' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
error: Lean exited with code 1
✖ [7906/7919] Building FormalConjectures.Arxiv.«2508.10245».Geode5Proof.RecurrenceCorrect (8.5s)
trace: .> LEAN_PATH=/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/bin/lean /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceCorrect.lean -o /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean/FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceCorrect.olean -i /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean/FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceCorrect.ilean -c /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/ir/FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceCorrect.c --setup /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/ir/FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceCorrect.setup.json --json
error: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceCorrect.lean:37:31: unsolved goals
d : ℕ
hd : 0 < d
rhs x : QYPoly
h : ↑d * x = rhs
⊢ Polynomial.C (↑d)⁻¹ * (↑d * x) = x
warning: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceCorrect.lean:39:23: This simp argument is unused:
  ← Polynomial.C_mul

Hint: Omit it from the simp argument list.
  simp [solveDiagonal, ←̵ ̵P̵o̵l̵y̵n̵o̵m̵i̵a̵l̵.̵C̵_̵m̵u̵l̵,̵ ̵hd.ne']

Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning.

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceCorrect.lean:39:43: This simp argument is unused:
  hd.ne'

Hint: Omit it from the simp argument list.
  simp [solveDiagonal, ← Polynomial.C_mul,̵ ̵h̵d̵.̵n̵e̵'̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceCorrect.lean:50:4: This simp argument is unused:
  Finset.sum_range_succ

Hint: Omit it from the simp argument list.
  simp [qQuotientAction, qPowerSum_zero, recurrenceDiagonal,̵
  ̵ ̵ ̵ ̵ ̵F̵i̵n̵s̵e̵t̵.̵s̵u̵m̵_̵r̵a̵n̵g̵e̵_̵s̵u̵c̵c̵] at h ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceCorrect.lean:112:0: 'Arxiv.«2508.10245».Geode5Proof.qRecurrenceStep_correct' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
error: Lean exited with code 1
✖ [7913/7919] Building FormalConjectures.Arxiv.«2508.10245».Geode5Proof.ExtendedCertificate (9342s)
trace: .> LEAN_PATH=/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/bin/lean /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/FormalConjectures/Arxiv/2508.10245/Geode5Proof/ExtendedCertificate.lean -o /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean/FormalConjectures/Arxiv/2508.10245/Geode5Proof/ExtendedCertificate.olean -i /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean/FormalConjectures/Arxiv/2508.10245/Geode5Proof/ExtendedCertificate.ilean -c /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/ir/FormalConjectures/Arxiv/2508.10245/Geode5Proof/ExtendedCertificate.c --setup /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/ir/FormalConjectures/Arxiv/2508.10245/Geode5Proof/ExtendedCertificate.setup.json --json
error: FormalConjectures/Arxiv/2508.10245/Geode5Proof/ExtendedCertificate.lean:74:47: Unknown identifier `on`

Note: It is not possible to treat `on` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
error: FormalConjectures/Arxiv/2508.10245/Geode5Proof/ExtendedCertificate.lean:91:37: Unknown identifier `extendedModuli_pairwise_coprime`
error: FormalConjectures/Arxiv/2508.10245/Geode5Proof/ExtendedCertificate.lean:95:14: Unknown constant `extendedModuli_pairwise_coprime`
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/ExtendedCertificate.lean:96:0: 'Arxiv.«2508.10245».Geode5Proof.answer_modEq_extendedResidue' depends on axioms: [Lean.ofReduceBool, Lean.trustCompiler]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/ExtendedCertificate.lean:97:0: 'Arxiv.«2508.10245».Geode5Proof.two_pow_35620_lt_extendedCertificateModulus' depends on axioms: [propext,
 Lean.ofReduceBool,
 Lean.trustCompiler]
error: Lean exited with code 1
Some required targets logged failures:
- FormalConjectures.Arxiv.«2508.10245».Geode5Defs
- FormalConjectures.Arxiv.«2508.10245».Geode5Proof.MomentFormula
- FormalConjectures.Arxiv.«2508.10245».Geode5Proof.RecurrenceCorrect
- FormalConjectures.Arxiv.«2508.10245».Geode5Proof.ExtendedCertificate
error: build failed