Prove OEIS A261865 density formula

[DomTheDeveloper]

Verified status

The exact OEIS A261865 theorem is sorry-free and kernel-verified at immutable commit 796f5e8919a844d78e8bb683d1974e118aa263ee.

Independent verification: ProofPlaygrond PR #46, workflow run 29967706220.

The pinned Lean 4.27.0 audit successfully:

1. checked out and confirmed the immutable proof commit;
2. rejected sorry, admit, native_decide, unsafe, custom axiom declarations, Lean.trustCompiler, Lean.ofReduce, and Lean.ofReduceBool throughout the proof chain;
3. built FormalConjectures/OEIS/261865FinalAudit.lean, including the exact numbered theorem OeisA261865.density_formula;
4. printed the axioms of the solution theorem, public theorem, and final audit wrapper.

All three theorems depend only on the standard axioms propext, Classical.choice, and Quot.sound. No sorryAx or unsupported trust mechanism is present.

Implemented proof chain

• Exact Formal Conjectures statement for Peter Kagey's Problem 13.
• Equivalence between square-root interval hits and terminal fractional-part arcs.
• Reduction from arbitrary smaller radicands to positive squarefree competitors.
• Rational linear independence of distinct squarefree radicals and their reciprocal square roots, including the constant coordinate 1.
• Multidimensional Weyl equidistribution for finite additive tori.
• Empirical probability measures and the Portmanteau continuity-set bridge.
• Terminal arcs and finite torus boxes, including null-frontier and exact Haar-mass calculations.
• Identification of the terminal-box orbit event with the least-radicand event.
• Exact product conversion to
  (1 / sqrt j) * ∏_{2 ≤ s < j, Squarefree s} (1 - 1 / sqrt s).

Packaging

• FormalConjectures/OEIS/A261865Base.lean: definitions and arithmetic/algebraic reductions.
• FormalConjectures/OEIS/261865Solution.lean: terminal-box density proof.
• FormalConjectures/OEIS/261865.lean: exact numbered theorem, without placeholders.
• FormalConjectures/OEIS/261865FinalAudit.lean: exact-statement wrapper and axiom reports.

The clean upstream-format catalog submission is PR #110 and links to this immutable verified proof.