{
 "schema": "imd-lean-capacity-final/v1",
 "experiment": "A847-LEAN-CAPACITY-32549b50e95c",
 "assignment": "evidence-only join of accepted branch A and branch B outputs",
 "proofs_rerun": false,
 "checkers_rerun": false,
 "branch_scripts_executed": false,
 "verdict": {
  "reconciliation": "PASS",
  "meaning": "The reconciliation found the archived evidence of both branches consistent: pins, ownership, root sets, logs, exits, export bytes/roots/axioms and checker records agree with each other and with the pinned sources. This is not proof replay, not mathematical verification by this job, not final-theorem certification and not a comparator/registry run.",
  "evidence_supported_complete_units": 87,
  "backlog_units": 87
 },
 "lineage": {
  "method": "Named dependency inputs were present in the workspace; their SHA-256 values were checked against the declared input hashes. The jobs API was therefore not queried. Acceptance status is taken from the task's provision of these inputs as accepted dependency snapshots and was not re-checked here.",
  "inputs": {
   "replay": {
    "path": "artifacts/lean-proof-unit/replay.sh",
    "bytes": 16613,
    "sha256": "b222cca4765faeebd619a23efd48b0bc2cc2520e37333a88e5d02cd89155341f",
    "declared_sha256": "b222cca4765faeebd619a23efd48b0bc2cc2520e37333a88e5d02cd89155341f",
    "match": true
   },
   "a_replay": {
    "path": "artifacts/lean-capacity/a/replay.sh",
    "bytes": 54010,
    "sha256": "6c6ec635843dbda7d58e907db8d2080e5c3f70b2e177bdf54b22cc22eab9529d",
    "declared_sha256": "6c6ec635843dbda7d58e907db8d2080e5c3f70b2e177bdf54b22cc22eab9529d",
    "match": true
   },
   "a_receipt": {
    "path": "artifacts/lean-capacity/a/receipt.json",
    "bytes": 3923409,
    "sha256": "829c69b61d894f6376eeaa58dbe151c830b36100ac5d9b3adc63a08dd2be92f6",
    "declared_sha256": "829c69b61d894f6376eeaa58dbe151c830b36100ac5d9b3adc63a08dd2be92f6",
    "match": true
   },
   "a_report": {
    "path": "artifacts/lean-capacity/a/report.md",
    "bytes": 4755,
    "sha256": "cfcdacef274754df36cfea624e6b8824ce7e607d7a5eae7fe38dce7c638f607e",
    "declared_sha256": "cfcdacef274754df36cfea624e6b8824ce7e607d7a5eae7fe38dce7c638f607e",
    "match": true
   },
   "a_evidence": {
    "path": "artifacts/lean-capacity/a/evidence.tar.gz",
    "bytes": 26807264,
    "sha256": "be8ba54e862ebc5ad8b57d00ba3828f1dcc32eaaccdbc191c0ac405faa6f5828",
    "declared_sha256": "be8ba54e862ebc5ad8b57d00ba3828f1dcc32eaaccdbc191c0ac405faa6f5828",
    "match": true
   },
   "b_replay": {
    "path": "artifacts/lean-capacity/b/replay.sh",
    "bytes": 395091,
    "sha256": "a0a2a10fc90c5d4c4f53b855b0658cb16a2ab3454da1dea5af40f5919bf88ce5",
    "declared_sha256": "a0a2a10fc90c5d4c4f53b855b0658cb16a2ab3454da1dea5af40f5919bf88ce5",
    "match": true
   },
   "b_receipt": {
    "path": "artifacts/lean-capacity/b/receipt.json",
    "bytes": 2741149,
    "sha256": "54a2a7648fb712767074861ddfd500cc2e591d6add15183a8c8665e4a2807169",
    "declared_sha256": "54a2a7648fb712767074861ddfd500cc2e591d6add15183a8c8665e4a2807169",
    "match": true
   },
   "b_report": {
    "path": "artifacts/lean-capacity/b/report.md",
    "bytes": 1722,
    "sha256": "194f324f546d031bbba85531352b188d615f3978d46682e7efa5afe0e94fd1fe",
    "declared_sha256": "194f324f546d031bbba85531352b188d615f3978d46682e7efa5afe0e94fd1fe",
    "match": true
   },
   "b_evidence": {
    "path": "artifacts/lean-capacity/b/evidence.tar.gz",
    "bytes": 15216909,
    "sha256": "b907e67b4927d4fdc9809cedb1b9b723212937c6d6ed0fb9175677cd79e3477d",
    "declared_sha256": "b907e67b4927d4fdc9809cedb1b9b723212937c6d6ed0fb9175677cd79e3477d",
    "match": true
   }
  },
  "all_inputs_match": true,
  "reference_replay_copies": {
   "declared_sha256": "b222cca4765faeebd619a23efd48b0bc2cc2520e37333a88e5d02cd89155341f",
   "A_archived_copy_sha256": "b222cca4765faeebd619a23efd48b0bc2cc2520e37333a88e5d02cd89155341f",
   "B_archived_copy_sha256": "b222cca4765faeebd619a23efd48b0bc2cc2520e37333a88e5d02cd89155341f",
   "both_match": true
  }
 },
 "source": {
  "head_commit": "048bb245b60abce79f1a2d0c82336ff8508ec752",
  "head_tree": "c6111a7d32daf2906275ee1ac265bf6865ebd9a5",
  "commit_matches_pin": true,
  "tree_matches_pin": true,
  "lean_toolchain_file": "leanprover/lean4:v4.35.0-rc2",
  "tracked_changes": [],
  "src_files_compared_to_git_blobs": 9660,
  "src_blob_mismatches": []
 },
 "toolchain": {
  "A": {
   "nanoda_bin": "8241c5e6baa29490aa118d382f97961b208ae730fdb96545c2abed74c9ece5a8",
   "con-ron": "4e5616d94374cae37324dad2594f6230c2bb2297240249fc78ff508f3bc5acef",
   "leanexport": "c5bc1a10a21e22cbb3671d65987cdef2076833b14182d823ccb2153adf2fa954",
   "lean": "bf8d54e4714cc4b03d3f6bb34c83b7202b87e49c8bfcbff6895c085bb90ceb38",
   "leanchecker": "9e36e955a251b1313c8eb5b7fa101282d51df109d34d8bb7c1cfdf51985aba29"
  },
  "B": {
   "con-ron": "4e5616d94374cae37324dad2594f6230c2bb2297240249fc78ff508f3bc5acef",
   "lake": "8ba83c98f76562d03b8dbc33f1057151ba6cbb121679dde76b2260ccc90495e1",
   "lean": "bf8d54e4714cc4b03d3f6bb34c83b7202b87e49c8bfcbff6895c085bb90ceb38",
   "leanchecker": "9e36e955a251b1313c8eb5b7fa101282d51df109d34d8bb7c1cfdf51985aba29",
   "leanexport": "c5bc1a10a21e22cbb3671d65987cdef2076833b14182d823ccb2153adf2fa954",
   "nanoda_bin": "8241c5e6baa29490aa118d382f97961b208ae730fdb96545c2abed74c9ece5a8"
  },
  "archive_sha256_A": "b67d0e0ba959fc74e186f1b44aebca32d6ecb6a28f8e9a029fc4e9f73398a049",
  "archive_sha256_B": "b67d0e0ba959fc74e186f1b44aebca32d6ecb6a28f8e9a029fc4e9f73398a049",
  "official_release_digest_A": "sha256:b67d0e0ba959fc74e186f1b44aebca32d6ecb6a28f8e9a029fc4e9f73398a049",
  "version_A": "Lean (version 4.35.0-rc2, x86_64-unknown-linux-gnu, commit 11acb17ec6b07a8f9e9173e6845197929540936b, Release)",
  "version_B": "Lean (version 4.35.0-rc2, x86_64-unknown-linux-gnu, commit 11acb17ec6b07a8f9e9173e6845197929540936b, Release)",
  "flags_A": [
   "-j1",
   "-DElab.async=false"
  ],
  "flags_B": [
   "-j1",
   "-DElab.async=false"
  ],
  "binary_hashes_agree": true,
  "archive_hashes_agree": true,
  "lean_commit_matches_pin": true,
  "flags_match": true
 },
 "archives": {
  "A": {
   "members_listed": 936,
   "hash_mismatches": [],
   "missing": [],
   "unlisted_files": [
    "ARCHIVE-MANIFEST.json"
   ],
   "archive": "artifacts/lean-capacity/a/evidence.tar.gz",
   "archive_sha256": "be8ba54e862ebc5ad8b57d00ba3828f1dcc32eaaccdbc191c0ac405faa6f5828",
   "archive_bytes": 26807264
  },
  "B": {
   "members_listed": 685,
   "hash_mismatches": [],
   "missing": [],
   "unlisted_files": [
    "files.json"
   ],
   "archive": "artifacts/lean-capacity/b/evidence.tar.gz",
   "archive_sha256": "b907e67b4927d4fdc9809cedb1b9b723212937c6d6ed0fb9175677cd79e3477d",
   "archive_bytes": 15216909
  },
  "safe_extraction": "member list checked before extraction: regular files only, no absolute or parent paths; extracted outside the repository"
 },
 "ownership": {
  "A_count": 56,
  "B_count": 31,
  "A_unique": 56,
  "B_unique": 31,
  "overlap": [],
  "union_count": 87,
  "union_equals_expected_87": true,
  "missing_from_union": [],
  "unexpected_ids": [],
  "A_assigned_count_field": 56
 },
 "canonical_queue": {
  "A_global_queue_len": 87,
  "B_global_queue_len": 87,
  "A_equals_B": true,
  "first_eight_match_brief": true,
  "covers_expected_87": true,
  "root8_parent_segments_match_brief": true,
  "A_receipt_order_is_filtered_global": true,
  "B_receipt_queue_is_filtered_global": true
 },
 "roots": {
  "unique_unit_and_support_roots": 555,
  "role_counts": {
   "unit_or_other": 87,
   "row_bindings": 85,
   "slices": 381,
   "intermediates": 2
  },
  "unit_roots_in_root_sets": 87,
  "A_unique_roots": 374,
  "B_unique_roots": 181,
  "roots_shared_between_branches": [],
  "brief_targets": {
   "slices": 381,
   "row_bindings": 85,
   "intermediates": 2,
   "unique": 555
  }
 },
 "cache_provenance": {
  "A": {
   "entries": 622,
   "source_lean_flags_mismatches": [],
   "unit_modules_in_cache": true
  },
  "B": {
   "entries": 446,
   "source_lean_flags_mismatches": [],
   "toolchain_archive_sha256_all_match": true,
   "unit_modules_in_cache": true
  }
 },
 "tier_totals": {
  "semantics": "Distinct complete units per tier. A and B are disjoint, so the 'distinct' row is the number of distinct units in that tier across both branches. Never summed across tiers. Supports are not units.",
  "worker_claimed": {
   "A": {
    "compile": 56,
    "type": 56,
    "axioms": 56,
    "export": 56,
    "lean_replay": 56,
    "nanoda": 56,
    "con_ron": 56
   },
   "B": {
    "compile": 31,
    "type": 31,
    "axioms": 31,
    "export": 31,
    "lean_replay": 31,
    "nanoda": 31,
    "con_ron": 31
   },
   "distinct": {
    "compile": 87,
    "type": 87,
    "axioms": 87,
    "export": 87,
    "lean_replay": 87,
    "nanoda": 87,
    "con_ron": 87
   }
  },
  "receipt_fields": {
   "A_tier_totals_field": {
    "compile": 56,
    "type": 56,
    "axioms": 56,
    "export": 56,
    "lean_replay": 56,
    "nanoda": 56,
    "con_ron": 56
   },
   "B_tier_totals_field": {
    "axioms": 31,
    "compile": 31,
    "con_ron": 31,
    "export": 31,
    "lean_replay": 31,
    "nanoda": 31,
    "type": 31
   },
   "B_portable_tier_totals_field": {
    "axioms": 31,
    "compile": 31,
    "con_ron": 31,
    "export": 31,
    "lean_replay": 31,
    "nanoda": 31,
    "type": 31
   }
  },
  "evidence_supported": {
   "A": {
    "compile": 56,
    "type": 56,
    "axioms": 56,
    "export": 56,
    "lean_replay": 56,
    "nanoda": 56,
    "con_ron": 56
   },
   "B": {
    "compile": 31,
    "type": 31,
    "axioms": 31,
    "export": 31,
    "lean_replay": 31,
    "nanoda": 31,
    "con_ron": 31
   },
   "distinct": {
    "compile": 87,
    "type": 87,
    "axioms": 87,
    "export": 87,
    "lean_replay": 87,
    "nanoda": 87,
    "con_ron": 87
   }
  },
  "evidence_rules": {
   "compile": "every closure module (A) or the unit module (B) has an exit-0 compile record, and a cache entry binds pinned source bytes, the authenticated lean hash and the flags -j1 -DElab.async=false",
   "type": "audit exit 0; the raw log hash matches; the audit source has autoImplicit=false and no bypass token; it states each root's source-derived published type against the root; ROOT_OK/IMD_ROOT success line for every root",
   "axioms": "'depends on axioms' line for every root in the raw log, subset of {propext, Quot.sound, Classical.choice}",
   "export": "export payload delivered; bytes hash to the recorded raw sha256; Lean githash in meta matches; every unit root is a thm record; every axiom record in the transitive export is in the allowed set",
   "lean_replay/nanoda/con_ron": "exit 0; raw log hash matches; binary hash equals authenticated toolchain hash; recorded export hash equals delivered export hash; NanoDa config hash matches; type/axioms/export tiers PASS"
  }
 },
 "coverage": {
  "complete_units": {
   "A": 56,
   "B": 31
  },
  "remaining_ids_by_tier": {
   "compile": [],
   "type": [],
   "axioms": [],
   "export": [],
   "lean_replay": [],
   "nanoda": [],
   "con_ron": []
  },
  "remaining_ids": [],
  "all_87_evidence_supported_in_every_tier": true
 },
 "stop_reasons": {
  "A": {
   "reason": "queue exhaustion",
   "proof_deadline_unix": 1792717500.0,
   "stopped_unix": 1792713423.8041718,
   "remaining_ids": []
  },
  "B": {
   "reason": "assigned canonical queue exhausted",
   "remaining_ids": []
  }
 },
 "exports": {
  "A": {
   "payloads": 22,
   "raw_bytes_total": 152801834,
   "items": {
    "exports/cohort-root8Node0Step1Chunk8_2_checked.jsonl": {
     "sha256": "8f4a99c395c55be3f52f7b52d0e7c9cf0f6c38ebdd3e4bf3d53483ec4fe79215",
     "bytes": 6560990
    },
    "exports/cohort-root8Node0Step1Chunk8_0_checked.jsonl": {
     "sha256": "89e73c7999939f297a520ae1b23a1b047c3f3644ae444884b567eedeaf65d1e7",
     "bytes": 6744742
    },
    "exports/cohort-root8Node0Step1Chunk8_3_checked.jsonl": {
     "sha256": "16f0a3b047d2fc2e336f1991e139307c489fbc6f712bca9f02082b30dd18b633",
     "bytes": 6930722
    },
    "exports/cohort-root2Node0Step4_checked.jsonl": {
     "sha256": "4b7fa3df3a11b17faf6930f08fc64eb39d9d41c000e32bc32d1b19c3cb069c45",
     "bytes": 4005022
    },
    "exports/cohort-root0Node0Step1Chunk0_0_checked.jsonl": {
     "sha256": "1c645357a018aa1bb1ce89ff55c99f89edb65e644bb6e348bb38064df2acb924",
     "bytes": 6494878
    },
    "exports/cohort-root0Node0Step1Chunk0_1_checked.jsonl": {
     "sha256": "1bdf3237c36dc0b5d0eb54730e56ad887e9ec69a798ff7ab6267264a3fc83097",
     "bytes": 6743665
    },
    "exports/cohort-root0Node0Step1Chunk0_4_checked.jsonl": {
     "sha256": "1ef755e991a51055842303abc75f9471155641c9daced9a2ca37fa0cb49a0194",
     "bytes": 6623266
    },
    "exports/cohort-root0Node0Step2Chunk5_0_checked.jsonl": {
     "sha256": "72069de7fb23ab2321846207aa19517b156a42ac84ee16839653f1d8fa02bd78",
     "bytes": 7046260
    },
    "exports/cohort-root0Node0Step2Chunk5_3_checked.jsonl": {
     "sha256": "94535dc0682f21886f36c6be05a56df6059ed5a3eecff96f0c85ab0d80759c09",
     "bytes": 7042956
    },
    "exports/cohort-root0Node0Step2Chunk6_0_checked.jsonl": {
     "sha256": "29d6efcf527d4cf016f3fd0ca8e38d612216e1a7842c96670a9bed20babe18a2",
     "bytes": 7137190
    },
    "exports/cohort-root0Node0Step2Chunk6_3_checked.jsonl": {
     "sha256": "8fa47b2616d4ab17497df8d84e714a34dbb20e708bdbb715df62eb54074ef1a4",
     "bytes": 7140459
    },
    "exports/cohort-root0Node0Step2Chunk7_0_checked.jsonl": {
     "sha256": "dd1331570fb8ad3d456444457c5bbd75840e62e2950bbd3d8615e040687b0f6e",
     "bytes": 7538718
    },
    "exports/cohort-root0Node0Step2Chunk7_3_checked.jsonl": {
     "sha256": "9376f6ac49f843c5f8da3879e7a50c032f5f5adf606d4ce67063e5790a0695a7",
     "bytes": 7535459
    },
    "exports/cohort-root0Node0Step2Chunk8_0_checked.jsonl": {
     "sha256": "8c5d5327079ce8f948ba536ecdad781cef757c7669c3476f06b2720c6ba27fd3",
     "bytes": 7256850
    },
    "exports/cohort-root0Node0Step2Chunk8_3_checked.jsonl": {
     "sha256": "4f79dc2fa3a338c53f1bd0e751bd3c87465b5bbd8cfe54939f60a39272cf4d22",
     "bytes": 7258683
    },
    "exports/cohort-root0Node0Step3Chunk5_5_checked.jsonl": {
     "sha256": "616f4a4969f052af65397f3600b303f609071f7874929f8bf8446620bc175ee9",
     "bytes": 7118441
    },
    "exports/cohort-root0Node0Step3Chunk6_2_checked.jsonl": {
     "sha256": "d5ef311eb8aeeadd140820f8af9d477a6e2e80780997d32aa1536741fb892375",
     "bytes": 7145560
    },
    "exports/cohort-root0Node0Step3Chunk6_5_checked.jsonl": {
     "sha256": "f20bf2695af2cf3ff1e33f1b6c5bb4f757486cedae1a3c61461aa3c6ad390282",
     "bytes": 7419353
    },
    "exports/cohort-root0Node0Step3Chunk7_2_checked.jsonl": {
     "sha256": "e0aff85241c0b23d89e937284675de94c5e5254bffc3c7ac27e3e5a8c5d26d37",
     "bytes": 7542820
    },
    "exports/cohort-root0Node0Step3Chunk7_5_checked.jsonl": {
     "sha256": "8ad95a13131fd5085e23ad1d5ad7caab48fd0dd5fbefc632ec3e90ea65fd3d7c",
     "bytes": 7357809
    },
    "exports/cohort-root0Node0Step3Chunk8_2_checked.jsonl": {
     "sha256": "084ce60170c6b2a28c5c412d43376b14e5beeb5ca4f92cc0d31a0ca60e8b9030",
     "bytes": 7264402
    },
    "exports/cohort-root0Node0Step3Chunk8_5_checked.jsonl": {
     "sha256": "b6dd01fc81c7e0efbd4062a245523f9b039e1fa53e7a8484dea72e4b90cfa35a",
     "bytes": 6893589
    }
   }
  },
  "B": {
   "payloads": 12,
   "raw_bytes_total": 83879396,
   "items": {
    "exports/5841af9733b59900f36f36b14eb80be4749d2970ef0543662cbd5c580c1b2c32.export.gz": {
     "sha256": "5841af9733b59900f36f36b14eb80be4749d2970ef0543662cbd5c580c1b2c32",
     "bytes": 6748224,
     "gzip_bytes": 1130273
    },
    "exports/85eb780390916737e7c3683530708992905c6824c3bc9f0f4f9fd5da3bbf0335.export.gz": {
     "sha256": "85eb780390916737e7c3683530708992905c6824c3bc9f0f4f9fd5da3bbf0335",
     "bytes": 6749730,
     "gzip_bytes": 1130346
    },
    "exports/affaaa5679bfdaf5cc94ba0c3b315971cee73fcc7bce5f94aae1b997737e2407.export.gz": {
     "sha256": "affaaa5679bfdaf5cc94ba0c3b315971cee73fcc7bce5f94aae1b997737e2407",
     "bytes": 6596535,
     "gzip_bytes": 1106974
    },
    "exports/0a02cb437b4d6d601a2a7fff6efd76395f126648db45cde1da9edfd549bf13eb.export.gz": {
     "sha256": "0a02cb437b4d6d601a2a7fff6efd76395f126648db45cde1da9edfd549bf13eb",
     "bytes": 6702617,
     "gzip_bytes": 1123718
    },
    "exports/e234e9e8bc55757014d6b01b8775e18e574ae7e795a963bc92d0fafc4b5cf4db.export.gz": {
     "sha256": "e234e9e8bc55757014d6b01b8775e18e574ae7e795a963bc92d0fafc4b5cf4db",
     "bytes": 6482679,
     "gzip_bytes": 1088713
    },
    "exports/5c201177d32f73a79257950d279eba91cbfca6e8d459f6116455cb1b2b5ae4e4.export.gz": {
     "sha256": "5c201177d32f73a79257950d279eba91cbfca6e8d459f6116455cb1b2b5ae4e4",
     "bytes": 6716467,
     "gzip_bytes": 1125451
    },
    "exports/26d7e0498791686b0def5f8bb4b37a47d68b99868054668df9f28a4ac23b026d.export.gz": {
     "sha256": "26d7e0498791686b0def5f8bb4b37a47d68b99868054668df9f28a4ac23b026d",
     "bytes": 6713378,
     "gzip_bytes": 1125607
    },
    "exports/f666e643e24804f8c37fb845df69a9af2c5637561421f1808af93df1d1b0dc4f.export.gz": {
     "sha256": "f666e643e24804f8c37fb845df69a9af2c5637561421f1808af93df1d1b0dc4f",
     "bytes": 6809691,
     "gzip_bytes": 1139884
    },
    "exports/36cc6322ca70445948c88651586c9b856cd956ff946c3955a180a1b178f40c05.export.gz": {
     "sha256": "36cc6322ca70445948c88651586c9b856cd956ff946c3955a180a1b178f40c05",
     "bytes": 6812990,
     "gzip_bytes": 1139966
    },
    "exports/f05730ffbfa1af8e521d95cce55a4d51d0e66a692bc940ba85d068ca5fee0980.export.gz": {
     "sha256": "f05730ffbfa1af8e521d95cce55a4d51d0e66a692bc940ba85d068ca5fee0980",
     "bytes": 7212069,
     "gzip_bytes": 1201648
    },
    "exports/6ac28971e7a6054dde25ac0b9ae65f7438d48e13d5e21c2d61fa79c2087e9f64.export.gz": {
     "sha256": "6ac28971e7a6054dde25ac0b9ae65f7438d48e13d5e21c2d61fa79c2087e9f64",
     "bytes": 7208852,
     "gzip_bytes": 1201246
    },
    "exports/d0c8bb02811a5920630e83a6decc93ee5b8760e0a83d416a005480522034532a.export.gz": {
     "sha256": "d0c8bb02811a5920630e83a6decc93ee5b8760e0a83d416a005480522034532a",
     "bytes": 9126164,
     "gzip_bytes": 1463342
    }
   }
  },
  "missing_export_delivery": {
   "A": [],
   "B": []
  }
 },
 "controls": {
  "results": {
   "A": {
    "fixture_compile": {
     "status": "PASS",
     "exit": 0,
     "log_verified": true
    },
    "false_expected_type": {
     "status": "FAIL",
     "exit": 1,
     "log_verified": true
    },
    "disallowed_axiom_audit": {
     "status": "FAIL",
     "exit": 1,
     "log_verified": true
    },
    "valid_export": {
     "status": "PASS",
     "exit": 0,
     "log_verified": true
    },
    "forbidden_export": {
     "status": "PASS",
     "exit": 0,
     "log_verified": true
    },
    "valid.lean_replay": {
     "status": "PASS",
     "exit": 0,
     "log_verified": true
    },
    "valid.nanoda": {
     "status": "PASS",
     "exit": 0,
     "log_verified": true
    },
    "valid.con_ron": {
     "status": "PASS",
     "exit": 0,
     "log_verified": true
    },
    "false-proof.lean_replay": {
     "status": "FAIL",
     "exit": 1,
     "log_verified": true
    },
    "false-proof.nanoda": {
     "status": "FAIL",
     "exit": 101,
     "log_verified": true
    },
    "false-proof.con_ron": {
     "status": "FAIL",
     "exit": 1,
     "log_verified": true
    },
    "incomplete.lean_replay": {
     "status": "PASS",
     "exit": 0,
     "log_verified": true
    },
    "incomplete.nanoda": {
     "status": "PASS",
     "exit": 0,
     "log_verified": true
    },
    "incomplete.con_ron": {
     "status": "PASS",
     "exit": 0,
     "log_verified": true
    },
    "missing-dependency.lean_replay": {
     "status": "FAIL",
     "exit": 1,
     "log_verified": true
    },
    "missing-dependency.nanoda": {
     "status": "FAIL",
     "exit": 101,
     "log_verified": true
    },
    "missing-dependency.con_ron": {
     "status": "FAIL",
     "exit": 1,
     "log_verified": true
    },
    "disallowed-axiom.lean_replay": {
     "status": "PASS",
     "exit": 0,
     "log_verified": true
    },
    "disallowed-axiom.nanoda": {
     "status": "FAIL",
     "exit": 101,
     "log_verified": true
    },
    "disallowed-axiom.con_ron": {
     "status": "FAIL",
     "exit": 2,
     "log_verified": true
    }
   },
   "B": {
    "false expected type": {
     "status": "FAIL",
     "exit": 1,
     "expected_rejection_observed": true,
     "log_verified": true
    },
    "disallowed axiom": {
     "status": "FAIL",
     "exit": 1,
     "expected_rejection_observed": true,
     "log_verified": true
    },
    "incomplete-export:incomplete-lean_replay.json": {
     "recorded_status": "FAIL",
     "reconciled_status": "BLOCKED",
     "exit": 1,
     "loader_failure": true,
     "classification": "incomplete-input loader/dependency rejection; no mathematical disproof",
     "log_verified": true
    },
    "incomplete-export:incomplete-nanoda.json": {
     "recorded_status": "FAIL",
     "reconciled_status": "BLOCKED",
     "exit": 2,
     "loader_failure": true,
     "classification": "incomplete-input loader/dependency rejection; no mathematical disproof",
     "log_verified": true
    },
    "incomplete-export:incomplete-con_ron.json": {
     "recorded_status": "FAIL",
     "reconciled_status": "BLOCKED",
     "exit": 3,
     "loader_failure": true,
     "classification": "incomplete-input loader/dependency rejection; no mathematical disproof",
     "log_verified": true
    }
   }
  },
  "interpretation": "Isolated fixtures, never proof units. FAIL means an actual recorded rejection. In A, all three replay tools accepted the omitted-root export (the structural root-presence gate rejected it), and leanchecker accepted the added-axiom export while NanoDa and con-ron rejected it; the strict axiom audit rejects added axioms regardless. In B, the incomplete-export controls are recorded as FAIL by the tools but reconciled as BLOCKED (loader/dependency refusal, not a disproof)."
 },
 "phase_wall_seconds": {
  "semantics": "Sum of recorded per-process wall seconds, deduplicated by log/export path; excludes acquisition, indexing and packaging.",
  "recomputed_from_records": {
   "A": {
    "compile": {
     "processes": 622,
     "summed_wall_seconds": 1138.948
    },
    "con_ron": {
     "processes": 22,
     "summed_wall_seconds": 328.397
    },
    "controls": {
     "processes": 20,
     "summed_wall_seconds": 62.32
    },
    "export": {
     "processes": 22,
     "summed_wall_seconds": 36.607
    },
    "lean_replay": {
     "processes": 22,
     "summed_wall_seconds": 63.869
    },
    "nanoda": {
     "processes": 22,
     "summed_wall_seconds": 16.936
    },
    "type_and_axiom_audit": {
     "processes": 56,
     "summed_wall_seconds": 130.592
    }
   },
   "B": {
    "compile": {
     "processes": 446,
     "summed_wall_seconds": 1675.692
    },
    "con_ron": {
     "processes": 12,
     "summed_wall_seconds": 157.992
    },
    "controls": {
     "processes": 5,
     "summed_wall_seconds": 4.679
    },
    "export": {
     "processes": 12,
     "summed_wall_seconds": 17.195
    },
    "lean_replay": {
     "processes": 12,
     "summed_wall_seconds": 42.344
    },
    "nanoda": {
     "processes": 12,
     "summed_wall_seconds": 13.082
    },
    "type_and_axiom_audit": {
     "processes": 12,
     "summed_wall_seconds": 57.293
    }
   }
  },
  "A_phase_file_as_delivered": {
   "semantics": "Sum of recorded process wall times, counted once; excludes acquisition, source indexing and packaging. Not an end-to-end throughput guarantee.",
   "phases": {
    "compile": {
     "processes": 622,
     "summed_wall_seconds": 1138.948057
    },
    "type_and_axiom_audit": {
     "processes": 56,
     "summed_wall_seconds": 130.59228
    },
    "controls": {
     "processes": 20,
     "summed_wall_seconds": 62.319729
    },
    "export": {
     "processes": 86,
     "summed_wall_seconds": 416.624346
    },
    "con_ron": {
     "processes": 2,
     "summed_wall_seconds": 29.18453
    }
   }
  },
  "A_commands_json_by_binary": {
   "con-ron": {
    "processes": 27,
    "summed_wall_seconds": 379.456
   },
   "lean (audit/control)": {
    "processes": 58,
    "summed_wall_seconds": 134.185
   },
   "lean (compile)": {
    "processes": 623,
    "summed_wall_seconds": 1140.718
   },
   "leanchecker": {
    "processes": 27,
    "summed_wall_seconds": 65.096
   },
   "leanexport": {
    "processes": 24,
    "summed_wall_seconds": 40.953
   },
   "nanoda_bin": {
    "processes": 27,
    "summed_wall_seconds": 17.26
   }
  },
  "B_process_start_window_utc": [
   "2026-10-22T23:22:49.276466+00:00",
   "2026-10-22T23:53:57.542714+00:00"
  ]
 },
 "unit_status": {
  "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_2_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot8Part0Segment03",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows8_2⟩\n      root8Node0Domains0 root8Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_2_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_2_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_2_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_2_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_2_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_2_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_0_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot8Part0Segment03",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows8_0⟩\n      root8Node0Domains0 root8Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_0_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_0_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_0_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_0_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_0_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_0_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_1_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot8Part0Segment03",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows8_1⟩\n      root8Node0Domains0 root8Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_1_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_1_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_1_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_1_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_1_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_1_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_3_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot8Part0Segment04",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows8_3⟩\n      root8Node0Domains0 root8Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_3_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_3_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_3_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_3_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_3_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_3_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_4_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot8Part0Segment04",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows8_4⟩\n      root8Node0Domains0 root8Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_4_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_4_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_4_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_4_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_4_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_4_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_5_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot8Part0Segment04",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows8_5⟩\n      root8Node0Domains0 root8Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_5_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_5_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_5_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_5_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_5_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_5_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusThree.root2Node0Step4_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusThreeRoot2Part1",
   "published_type": "checkReplacement table22 root2Node0Domains3 root2Node0Domains4 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusThree.root2Node0Step4_checked"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root7Node110Step1_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot7Part43",
   "published_type": "checkReplacement table36 root7Node110Domains0 root7Node110Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root7Node110Step1_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_0_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot7Part0Segment03",
   "published_type": "checkNarrowing ⟨table34Scope, table34Rows7_0⟩\n      root7Node0Domains0 root7Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_0_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_0_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_0_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_0_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_0_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_0_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_0_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_0_slice6_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_1_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot7Part0Segment03",
   "published_type": "checkNarrowing ⟨table34Scope, table34Rows7_1⟩\n      root7Node0Domains0 root7Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_1_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_1_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_1_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_1_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_1_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_1_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_1_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_1_slice6_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_2_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot7Part0Segment03",
   "published_type": "checkNarrowing ⟨table34Scope, table34Rows7_2⟩\n      root7Node0Domains0 root7Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_2_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_2_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_2_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_2_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_2_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_2_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_2_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_2_slice6_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_3_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot7Part0Segment03",
   "published_type": "checkNarrowing ⟨table34Scope, table34Rows7_3⟩\n      root7Node0Domains0 root7Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_3_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_3_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_3_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_3_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_3_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_3_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_3_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_3_slice6_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_4_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot7Part0Segment03",
   "published_type": "checkNarrowing ⟨table34Scope, table34Rows7_4⟩\n      root7Node0Domains0 root7Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_4_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_4_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_4_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_4_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_4_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_4_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_4_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_4_slice6_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_5_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot7Part0Segment03",
   "published_type": "checkNarrowing ⟨table34Scope, table34Rows7_5⟩\n      root7Node0Domains0 root7Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_5_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_5_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_5_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_5_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_5_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_5_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_5_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root7Node0Step1Chunk7_5_slice6_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_0_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment01",
   "published_type": "checkNarrowing ⟨table45Scope, table45Rows0_0⟩\n      root0Node0Domains0 root0Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_0_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_0_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_0_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_0_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_0_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot4Part0Segment02",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows4_0⟩\n      root4Node0Domains0 root4Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_0_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_0_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_0_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_0_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_1_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot4Part0Segment02",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows4_1⟩\n      root4Node0Domains0 root4Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_1_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_1_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_1_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_1_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_2_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot4Part0Segment03",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows4_2⟩\n      root4Node0Domains0 root4Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_2_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_2_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_2_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_2_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_3_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot4Part0Segment03",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows4_3⟩\n      root4Node0Domains0 root4Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_3_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_3_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_3_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_3_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_4_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot4Part0Segment03",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows4_4⟩\n      root4Node0Domains0 root4Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_4_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_4_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_4_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_4_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_5_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot4Part0Segment03",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows4_5⟩\n      root4Node0Domains0 root4Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_5_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_5_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_5_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root4Node0Step1Chunk4_5_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_1_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment02",
   "published_type": "checkNarrowing ⟨table45Scope, table45Rows0_1⟩\n      root0Node0Domains0 root0Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_1_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_1_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_1_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_1_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_2_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment02",
   "published_type": "checkNarrowing ⟨table45Scope, table45Rows0_2⟩\n      root0Node0Domains0 root0Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_2_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_2_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_2_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_2_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_3_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment02",
   "published_type": "checkNarrowing ⟨table45Scope, table45Rows0_3⟩\n      root0Node0Domains0 root0Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_3_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_3_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_3_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_3_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_4_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment02",
   "published_type": "checkNarrowing ⟨table45Scope, table45Rows0_4⟩\n      root0Node0Domains0 root0Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_4_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_4_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_4_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_4_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_5_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment02",
   "published_type": "checkNarrowing ⟨table45Scope, table45Rows0_5⟩\n      root0Node0Domains0 root0Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_5_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_5_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_5_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step1Chunk0_5_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_0_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot1Part0Segment02",
   "published_type": "checkNarrowing ⟨table34Scope, table34Rows1_0⟩\n      root1Node0Domains0 root1Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_0_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_0_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_0_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_0_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_1_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot1Part0Segment02",
   "published_type": "checkNarrowing ⟨table34Scope, table34Rows1_1⟩\n      root1Node0Domains0 root1Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_1_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_1_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_1_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_1_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_2_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot1Part0Segment02",
   "published_type": "checkNarrowing ⟨table34Scope, table34Rows1_2⟩\n      root1Node0Domains0 root1Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_2_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_2_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_2_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_2_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_3_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot1Part0Segment02",
   "published_type": "checkNarrowing ⟨table34Scope, table34Rows1_3⟩\n      root1Node0Domains0 root1Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_3_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_3_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_3_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_3_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_4_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot1Part0Segment02",
   "published_type": "checkNarrowing ⟨table34Scope, table34Rows1_4⟩\n      root1Node0Domains0 root1Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_4_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_4_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_4_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_4_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_5_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot1Part0Segment02",
   "published_type": "checkNarrowing ⟨table34Scope, table34Rows1_5⟩\n      root1Node0Domains0 root1Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_5_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_5_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_5_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root1Node0Step1Chunk1_5_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_0_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot5Part0Segment03",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows5_0⟩\n      root5Node0Domains0 root5Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_0_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_0_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_0_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_0_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_1_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot5Part0Segment03",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows5_1⟩\n      root5Node0Domains0 root5Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_1_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_1_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_1_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_1_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_2_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot5Part0Segment03",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows5_2⟩\n      root5Node0Domains0 root5Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_2_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_2_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_2_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_2_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_3_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot5Part0Segment03",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows5_3⟩\n      root5Node0Domains0 root5Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_3_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_3_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_3_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_3_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_4_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot5Part0Segment03",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows5_4⟩\n      root5Node0Domains0 root5Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_4_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_4_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_4_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_4_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_5_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot5Part0Segment03",
   "published_type": "checkNarrowing ⟨table56Scope, table56Rows5_5⟩\n      root5Node0Domains0 root5Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_5_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_5_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_5_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root5Node0Step1Chunk5_5_slice2_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_0_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot6Part0Segment03",
   "published_type": "checkNarrowing ⟨table35Scope, table35Rows6_0⟩\n      root6Node0Domains0 root6Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_0_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_0_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_0_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_0_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_0_slice3_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_1_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot6Part0Segment03",
   "published_type": "checkNarrowing ⟨table35Scope, table35Rows6_1⟩\n      root6Node0Domains0 root6Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_1_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_1_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_1_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_1_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_1_slice3_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_2_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot6Part0Segment03",
   "published_type": "checkNarrowing ⟨table35Scope, table35Rows6_2⟩\n      root6Node0Domains0 root6Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_2_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_2_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_2_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_2_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_2_slice3_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_3_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot6Part0Segment03",
   "published_type": "checkNarrowing ⟨table35Scope, table35Rows6_3⟩\n      root6Node0Domains0 root6Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_3_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_3_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_3_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_3_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_3_slice3_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_4_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot6Part0Segment03",
   "published_type": "checkNarrowing ⟨table35Scope, table35Rows6_4⟩\n      root6Node0Domains0 root6Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_4_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_4_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_4_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_4_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_4_slice3_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_5_checked": {
   "branch": "B",
   "module": "SpectreFinite.RadiusFiveRoot6Part0Segment03",
   "published_type": "checkNarrowing ⟨table35Scope, table35Rows6_5⟩\n      root6Node0Domains0 root6Node0Domains1 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_5_rows_exact",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_5_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_5_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_5_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root6Node0Step1Chunk6_5_slice3_checked"
   ],
   "claimed": {
    "axioms": "PASS",
    "compile": "PASS",
    "con_ron": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "type": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_0_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment05",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows5_0⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_0_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_0_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_0_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_0_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_1_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment05",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows5_1⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_1_projected_slices_pilot_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_1_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_1_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_1_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_1_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_2_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment05",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows5_2⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_2_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_2_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_2_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_2_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_3_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment05",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows5_3⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_3_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_3_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_3_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_3_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_4_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment05",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows5_4⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_4_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_4_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_4_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_4_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_5_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment05",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows5_5⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_5_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_5_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_5_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk5_5_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_0_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment05",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows6_0⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_0_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_0_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_0_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_0_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_0_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_1_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment05",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows6_1⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_1_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_1_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_1_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_1_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_1_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_2_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment05",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows6_2⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_2_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_2_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_2_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_2_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_2_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_3_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment05",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows6_3⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_3_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_3_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_3_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_3_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_3_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_4_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment05",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows6_4⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_4_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_4_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_4_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_4_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_4_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_5_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment05",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows6_5⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_5_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_5_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_5_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_5_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk6_5_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_0_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment06",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows7_0⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_0_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_0_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_0_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_0_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_0_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_0_projected_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_0_projected_slice6_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_0_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_1_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment06",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows7_1⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_1_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_1_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_1_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_1_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_1_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_1_projected_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_1_projected_slice6_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_1_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_2_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment06",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows7_2⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_2_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_2_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_2_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_2_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_2_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_2_projected_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_2_projected_slice6_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_2_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_3_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment06",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows7_3⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_3_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_3_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_3_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_3_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_3_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_3_projected_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_3_projected_slice6_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_3_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_4_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment06",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows7_4⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_4_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_4_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_4_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_4_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_4_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_4_projected_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_4_projected_slice6_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_4_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_5_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment06",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows7_5⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_5_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_5_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_5_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_5_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_5_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_5_projected_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_5_projected_slice6_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk7_5_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_0_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment06",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows8_0⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_0_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_0_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_0_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_0_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_0_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_0_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_1_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment06",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows8_1⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_1_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_1_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_1_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_1_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_1_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_1_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_2_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment06",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows8_2⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_2_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_2_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_2_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_2_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_2_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_2_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_3_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment06",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows8_3⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_3_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_3_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_3_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_3_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_3_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_3_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_4_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment06",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows8_4⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_4_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_4_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_4_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_4_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_4_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_4_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_5_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment06",
   "published_type": "checkNarrowing ⟨table57Scope, table57Rows8_5⟩\n      root0Node0Domains1 root0Node0Domains2 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_5_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_5_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_5_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_5_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_5_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step2Chunk8_5_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk5_5_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows5_5⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk5_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk5_5_projected_slices_pilot_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk5_5_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk5_5_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk5_5_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk5_5_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_0_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows6_0⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_0_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_0_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_0_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_0_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_0_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_1_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows6_1⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_1_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_1_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_1_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_1_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_1_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_2_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows6_2⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_2_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_2_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_2_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_2_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_2_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_3_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows6_3⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_3_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_3_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_3_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_3_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_3_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_4_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows6_4⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_4_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_4_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_4_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_4_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_4_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_5_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows6_5⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_5_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_5_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_5_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_5_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk6_5_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_0_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows7_0⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_0_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_0_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_0_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_0_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_0_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_0_projected_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_0_projected_slice6_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_0_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_1_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows7_1⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_1_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_1_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_1_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_1_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_1_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_1_projected_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_1_projected_slice6_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_1_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_2_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows7_2⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_2_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_2_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_2_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_2_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_2_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_2_projected_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_2_projected_slice6_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_2_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_3_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows7_3⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_3_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_3_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_3_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_3_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_3_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_3_projected_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_3_projected_slice6_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_3_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_4_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows7_4⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_4_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_4_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_4_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_4_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_4_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_4_projected_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_4_projected_slice6_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_4_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_5_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows7_5⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_5_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_5_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_5_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_5_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_5_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_5_projected_slice5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_5_projected_slice6_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk7_5_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_0_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows8_0⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_0_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_0_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_0_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_0_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_0_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_0_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_1_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows8_1⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_1_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_1_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_1_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_1_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_1_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_1_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_2_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows8_2⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_2_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_2_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_2_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_2_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_2_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_2_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_3_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows8_3⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_3_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_3_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_3_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_3_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_3_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_3_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_4_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows8_4⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_4_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_4_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_4_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_4_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_4_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_4_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  },
  "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_5_checked": {
   "branch": "A",
   "module": "SpectreFinite.RadiusFiveRoot0Part0Segment08",
   "published_type": "checkNarrowing ⟨table33Scope, table33Rows8_5⟩\n      root0Node0Domains2 root0Node0Domains3 = true",
   "roots": [
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_5_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_5_projected_slice0_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_5_projected_slice1_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_5_projected_slice2_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_5_projected_slice3_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_5_projected_slice4_checked",
    "SpectreFinite.HexSearch.RadiusFive.root0Node0Step3Chunk8_5_projected_rows_exact"
   ],
   "claimed": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   },
   "evidence": {
    "compile": "PASS",
    "type": "PASS",
    "axioms": "PASS",
    "export": "PASS",
    "lean_replay": "PASS",
    "nanoda": "PASS",
    "con_ron": "PASS"
   }
  }
 },
 "discrepancies": [
  {
   "branch": "A",
   "unit": null,
   "issue": "phase-wall-times.json phase lean_replay = None disagrees with per-unit command records {'processes': 22, 'summed_wall_seconds': 63.869} (unit-level records retained)"
  },
  {
   "branch": "A",
   "unit": null,
   "issue": "phase-wall-times.json phase nanoda = None disagrees with per-unit command records {'processes': 22, 'summed_wall_seconds': 16.936} (unit-level records retained)"
  },
  {
   "branch": "A",
   "unit": null,
   "issue": "phase-wall-times.json phase con_ron = {'processes': 2, 'summed_wall_seconds': 29.18453} disagrees with per-unit command records {'processes': 22, 'summed_wall_seconds': 328.397} (unit-level records retained)"
  },
  {
   "branch": "A",
   "unit": null,
   "issue": "phase-wall-times.json export = 86 processes / 416.6 s, but commands.json has 24 leanexport records / 41.0 s (22 unit cohorts + 2 controls); recomputed values reported"
  }
 ],
 "limitations": [
  "No Lean, checker or branch script was run; all statuses come from archived records, raw logs and export bytes.",
  "Lean replay (leanchecker) uses the same kernel as compilation; structural export acceptance is not proof validation.",
  "Exact-type evidence is the recorded successful elaboration of the audit file; this job only verified that the audit file states the source-derived types and that the logs and exits are hash-bound.",
  "A's phase-wall-times.json leaves out its lean_replay and nanoda processes and counts only 2 con_ron processes. The per-unit records show 22 processes for each of these tools. Recomputed values are reported.",
  "Toolchain binaries and compiled caches are not in the archives (by design); a fresh run needs the authenticated official toolchain."
 ]
}