{
  "schema": "lean-proof-unit/receipt/v1",
  "result": "PASS",
  "result_reason": "declaration elaborated and kernel-checked by Lean 4.35.0-rc2; axioms within allowed set",
  "harness_exit_status": 0,
  "lean_check_exit_status": 0,
  "checked_at_utc": "2026-10-22T21:21:27Z",
  "source": {
    "repository_head": "048bb245b60abce79f1a2d0c82336ff8508ec752",
    "pinned_commit": "048bb245b60abce79f1a2d0c82336ff8508ec752",
    "tree_matches_pinned_commit_for": [
      "src/",
      "lean-toolchain",
      "lakefile.lean",
      "lake-manifest.json"
    ],
    "module": "SpectreFinite.RadiusFiveRoot8Step1Chunk8_2Slice3",
    "module_file": "src/SpectreFinite/RadiusFiveRoot8Step1Chunk8_2Slice3.lean",
    "module_file_sha256": "19dbe58ae5381c55582e39f8809d2cdb3b59a54dcede4a6a58aa82f4acd85a45",
    "declaration": "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_2_slice3_checked"
  },
  "pins": {
    "lean_toolchain_file": "leanprover/lean4:v4.35.0-rc2",
    "lean_toolchain_file_sha256": "8dc8d6f560141069d9073e370611716ef77ada0da8ffa37e2149f44b2e63ac7a",
    "lean_release_url": "https://github.com/leanprover/lean4/releases/download/v4.35.0-rc2/lean-4.35.0-rc2-linux.tar.zst",
    "lean_release_sha256": "b67d0e0ba959fc74e186f1b44aebca32d6ecb6a28f8e9a029fc4e9f73398a049",
    "lean_version_reported": "Lean (version 4.35.0-rc2, x86_64-unknown-linux-gnu, commit 11acb17ec6b07a8f9e9173e6845197929540936b, Release)",
    "lakefile_lean_sha256": "93980e47f49d49b6e37eaa23f13d801b8cf71effc43ec6b93b95940bdae178d9",
    "lake_manifest_json_sha256": "ad06e9c9eddef177a0dfc84064848dae13385444b57b9eb531448fa4c9f73110",
    "mathlib_rev": "065356127b1dc0016f66b7283ce0ce2c4055aa55",
    "mathlib_loaded_by_this_check": false,
    "lean_args": [
      "-j1",
      "-DElab.async=false"
    ]
  },
  "check": {
    "method": "lean -o (direct compile of transitive import closure, then audit file)",
    "modules_compiled": 219,
    "timeout_seconds": 1200,
    "elapsed_seconds": 15,
    "allowed_axioms": [
      "propext",
      "Classical.choice",
      "Quot.sound"
    ],
    "axioms_reported": [
      "Classical.choice",
      "Quot.sound",
      "propext"
    ]
  },
  "not_performed": [
    "final all-dimensional theorem comparison (comparator Challenge/Solution)",
    "independent-kernel replay (e.g. lean4checker / external kernel)",
    "Lake build of the full PalomarAllDimensions library",
    "official Palomar preflight"
  ],
  "scope_note": "Checks one helper declaration only. It does not establish the all-dimensional theorem or Palomar verification.",
  "evidence_file": "evidence.txt"
}