Audit A261865 proof commit 02688846

[DomTheDeveloper]

Independent verification of the A261865 Lean proof from DomTheDeveloper/formal-conjectures.

The workflow checks the pinned proof commit 02688846b7a0d44e208cef7581bbdbb3978813c6 in two ways:

• AXLE validation of the foundational torus and squarefree-radical modules.
• Lean 4.27 compilation of FormalConjectures/OEIS/261865FinalAudit.lean, rejection of placeholders/trust escapes, and a sorryAx axiom check.

This PR exists only as a stable checker surface in ProofPlaygrond; no proof source is duplicated here.

[DomTheDeveloper]

/audit-a261865-f5d289e

[DomTheDeveloper]

/audit-a261865-report-f5d289e

[github-actions]

A261865 audit started for immutable proof commit f5d289e074dc692ab75eb6050128339ef95861c2.

[github-actions]

A261865 AXLE audit failed at f5d289e074dc692ab75eb6050128339ef95861c2.

## FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorus.lean
okay=True
failed_declarations=["UnitAddTorus.integral_mFourier", "UnitAddTorus.mFourier_coe_ne_one", "UnitAddTorus.tendsto_geom_average_zero", "UnitAddTorus.tendsto_average_rotation", "UnitAddTorus.unitAddCircleVolume_isProbabilityMeasure", "UnitAddTorus.mFourier_add_point", "UnitAddTorus.mFourier_nsmul", "UnitAddTorus.NoIntegerRelation", "UnitAddTorus.volume_eq_fourierVolume", "UnitAddTorus.mFourier_eq_toCircle_sum", "UnitAddTorus.tendsto_average_of_tendsto_mFourier"]
## FormalConjecturesForMathlib/NumberTheory/SquarefreeRadical.lean
okay=True
## FormalConjecturesForMathlib/MeasureTheory/Group/UnitAddCircleArc.lean
okay=True
failed_declarations=["UnitAddCircle.coe_mem_terminalArc_iff", "UnitAddCircle.volume_frontier_terminalArc", "UnitAddCircle.volume_terminalArc_compl", "UnitAddCircle.volume_terminalArc", "UnitAddCircle.volume_sphere_eq_zero", "UnitAddCircle.coe_fract_eq", "UnitAddCircle.coe_preimage_ball_eq_iUnion", "UnitAddCircle.volume_frontier_terminalArc_compl", "UnitAddCircle.terminalArc", "UnitAddCircle.measurableSet_terminalArc", "UnitAddCircle.nsmul_mem_terminalArc_iff"]
## FormalConjecturesForMathlib/MeasureTheory/Probability/PiContinuitySet.lean
okay=True
failed_declarations=["Set.frontier_pi_subset_iUnion", "MeasureTheory.measure_frontier_pi_eq_zero"]
## FormalConjecturesForMathlib/MeasureTheory/Probability/Empirical.lean
okay=False
-:16:0: error: unknown module prefix 'FormalConjecturesForMathlib'

No directory 'FormalConjecturesForMathlib' or file 'FormalConjecturesForMathlib.olean' in the search path entries:
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/batteries
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/Qq
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/LeanSearchClient
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/aesop
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/importGraph
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/plausible
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/toolchain
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/proofwidgets
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/mathlib
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/toolchain/lib/lean

## FormalConjecturesForMathlib/NumberTheory/SquarefreeRadicals.lean
okay=False
-:16:0: error: unknown module prefix 'FormalConjecturesForMathlib'

No directory 'FormalConjecturesForMathlib' or file 'FormalConjecturesForMathlib.olean' in the search path entries:
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/batteries
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/Qq
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/LeanSearchClient
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/aesop
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/importGraph
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/plausible
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/toolchain
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/proofwidgets
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/mathlib
/opt/prover_tools/.versions/lean-4.27.0-21cbc2e2a4e977f67b250578dc1af4770a30c3393bf724c1d53d2b714d18c2e3/libs/toolchain/lib/lean