# A847-LEAN-CAPACITY-32549b50e95c: final evidence reconciliation

**Result:** the reconciliation passes. Both accepted branches have consistent, hash-bound evidence for 87 distinct complete units out of the 87-unit backlog, in every tier. Branch A has 56 and Branch B has 31, with no overlap.

This job joined existing evidence only. It did not run Lean, any checker or any branch script. It does not verify the mathematics, certify the final theorem or run the comparator or registry. Machine-readable details are in `summary.json` (schema `imd-lean-capacity-final/v1`).

## Inputs and lineage
- All nine named dependency inputs were present, and their SHA-256 values match the declared hashes. The inputs are the A and B `receipt.json`, `report.md`, `replay.sh` and `evidence.tar.gz`, plus the reference `lean-proof-unit/replay.sh`.
- Because the inputs were present, the jobs API was not queried. Acceptance status comes from the task supplying these inputs as accepted snapshots. It was not checked again here.
- Both archives carry a copy of the reference replay script. Each copy hashes to the declared `b222cca4…341f` and is labelled as reference data only.
- Archive A has 936 listed members and archive B has 685. Every member was present with the listed size and SHA-256, and there were no unlisted files apart from the manifest itself.
- Before extracting, I checked the member lists: regular files only, no absolute paths and no `..` paths. The archives were extracted outside the repository.

## Source and toolchain pins
- **Source:** HEAD is `048bb245b60abce79f1a2d0c82336ff8508ec752` and its tree is `c6111a7d32daf2906275ee1ac265bf6865ebd9a5`. Both match the pin and both receipts.
- **Source bytes:** there are no tracked changes. All 9,660 tracked `src/` files were compared against their Git blobs with `git hash-object --no-filters`, not just the index status. There were 0 mismatches.
- **Toolchain:** `lean-toolchain` is `leanprover/lean4:v4.35.0-rc2`. Both branches record the official archive SHA-256 `b67d0e0b…a049`, which equals the GitHub release digest recorded by A. Both record version commit `11acb17ec6b0…936b`.
- **Binaries:** both branches record identical hashes for `lean`, `leanexport`, `leanchecker`, `nanoda_bin` and `con-ron`. B also records `lake`.
- **Flags:** both branches used `-j1 -DElab.async=false`.
- **Compile cache:** every entry binds pinned source bytes (recomputed here), the authenticated `lean` hash and those flags. That is 622 modules for A and 446 for B, with 0 mismatches. B's entries also bind the toolchain archive hash. No binaries were delivered.

## Ownership, queue and roots
- A has 56 unique IDs and B has 31. There is no overlap, and the union equals exactly the 87 IDs generated from the brief's patterns (a)–(d).
- Every root name was located in the pinned sources inside its exact namespace, which separates it from same-named RadiusThree and RadiusFour declarations.
- For every unit, the published type matches the type in the source declaration. No root body contains `native_decide`, `sorry`, `ofReduceBool`, `implemented_by`, `extern` or `axiom`.
- **Root counts:** 555 unique unit and support roots. That is 87 unit roots, 381 slices (including the `projected_slice` slices), 85 row bindings (including `projected_rows_exact`) and 2 `projected_slices_pilot` intermediates. A has 374 and B has 181, with none shared. All four counts match the brief.
- **Canonical queue:** A's and B's global queues are identical (87 entries). The first eight entries match the brief: Root8 chunks 8_2, 8_0, 8_1, 8_3, 8_4, 8_5, then `RadiusThree.root2Node0Step4`, then `root7Node110Step1`. The first three Root8 parents are in `Part0Segment03` and the next three in `Segment04`. Each branch's order is the global queue filtered to that branch.

## Tier totals (distinct complete units; never summed across tiers)

| Tier | A claimed | A supported by evidence | B claimed | B supported by evidence | Distinct supported (of 87) |
|---|---:|---:|---:|---:|---:|
| compile | 56 | 56 | 31 | 31 | 87 |
| type | 56 | 56 | 31 | 31 | 87 |
| axioms | 56 | 56 | 31 | 31 | 87 |
| export | 56 | 56 | 31 | 31 | 87 |
| lean_replay | 56 | 56 | 31 | 31 | 87 |
| nanoda | 56 | 56 | 31 | 31 | 87 |
| con_ron | 56 | 56 | 31 | 31 | 87 |

"Claimed" is each branch's own per-unit status. It agrees with the branch's `tier_totals` field, and with B's `portable_tier_totals`. "Supported by evidence" was recomputed here from the archived bytes:

- **type and axioms:** the audit exited 0 and its raw log matches the recorded hash. The audit source sets `autoImplicit false`, has no bypass token, and states the source-derived type of every root. Every root has a success line, and its "depends on axioms" set is within {propext, Quot.sound, Classical.choice}.
- **export:** the delivered payload hashes to the recorded raw SHA-256 and its meta records Lean githash `11acb17…`. Every unit root is a `thm` record. Every `axiom` record in the transitive export is in the allowed set.
- **lean_replay, nanoda, con_ron:** the process exited 0 with a hash-matched raw log. The binary hash equals the authenticated toolchain hash and the export hash equals the delivered payload. For NanoDa, the config hash also matches. These tiers also require type, axioms and export to pass.

Supports are not counted as units. Each replacement is one unit.

**Remaining IDs:** none in any tier.

## Exports
- **A:** 22 cohort exports in uncompressed JSONL, 152,801,834 raw bytes in total, inside a 26,807,264-byte archive.
- **B:** 12 deduplicated cohort exports, gzip-compressed, 83,879,396 raw bytes in total, inside a 15,216,909-byte archive.

Every unit's roots were found in its delivered export. Neither branch has missing export deliveries, and nothing was truncated. A cohort export covers several units of the same module, so each export was parsed once and checked for every unit it covers.

## Stop reasons
- **A:** "queue exhaustion", with no remaining IDs. It stopped at unix 1792713423.8, before its proof deadline of 1792717500.
- **B:** "assigned canonical queue exhausted", with no remaining IDs. Its recorded process starts run from 2026-10-22T23:22:49Z to 23:53:57Z. Its budget record shows no fixed 1200-second cutoff.

## Phase wall times (summed per process, recomputed from records)

| Phase | A processes / seconds | B processes / seconds |
|---|---|---|
| compile | 622 / 1138.9 | 446 / 1675.7 |
| type and axiom audit | 56 / 130.6 | 12 / 57.3 |
| export | 22 / 36.6 | 12 / 17.2 |
| lean_replay | 22 / 63.9 | 12 / 42.3 |
| nanoda | 22 / 16.9 | 12 / 13.1 |
| con_ron | 22 / 328.4 | 12 / 158.0 |
| controls | 20 / 62.3 | 5 / 4.7 |

These sums exclude toolchain acquisition, source indexing and packaging. They are not a throughput guarantee.

**Discrepancy, kept as delivered:** A's `phase-wall-times.json` does not match A's own records:
- It has no lean_replay or nanoda entries.
- It reports con_ron as 2 processes / 29.2 s.
- It reports export as 86 processes / 416.6 s.

A's `commands.json` has 27 records each for leanchecker, nanoda_bin and con-ron (22 unit cohorts plus 5 controls) and 24 leanexport records totalling 41.0 s. The per-unit records are self-consistent and are what this report uses. The discrepancy affects timing only, not any unit status.

## Controls (isolated fixtures, not units; raw log hashes verified)
- **A, false expected type and added axiom:** the Lean audits actually rejected both (FAIL, exit 1).
- **A, ill-typed proof and missing-dependency exports:** all three replay tools rejected both.
- **A, omitted-root export:** all three tools accepted it. Only the structural root-presence gate rejected it.
- **A, added-axiom export:** leanchecker accepted it, while NanoDa (exit 101) and con-ron (exit 2) rejected it. The strict per-root axiom audit rejects added axioms regardless of what the replay tools do.
- **B, false type and disallowed axiom:** both were actually rejected (FAIL, exit 1).
- **B, incomplete export:** leanchecker, NanoDa and con-ron all refused it (exits 1, 2 and 3). The tools recorded FAIL, but B reconciled these as BLOCKED because they are loader/dependency refusals, not disproofs.

None of these outcomes was inferred. Each comes from a recorded exit and a hash-verified log.

## Checks run by this job
- An independent Python validator was run over the extracted archives and pinned sources. It rebuilds the 87-unit backlog from the brief and checks all of the above.
- As a sanity check, the validator's export parser was run on A's control fixtures. It flags the extra axiom in the forbidden-axiom export and the missing root in the omitted-root export, and parses the valid export cleanly.
- Final result: 4 discrepancies, all limited to A's timing summary. There are 0 discrepancies in ownership, pins, roots, logs, exports or tier statuses.
- No build or test of the Lean project was run, because the assignment forbids rerunning proofs.

## Limitations
- Exact-type and axiom results come from the branches' recorded audit runs. This job checked that those runs are hash-bound and state the right types; it did not re-elaborate them.
- Lean replay uses the same kernel as compilation. Structural export acceptance is not proof validation.
- Toolchain and cache binaries are not archived. A fresh run needs the authenticated official v4.35.0-rc2 release.
- Normal job delivery of all 87 units is not, by itself, a claim of mathematical verification.
- Only `artifacts/lean-capacity/final/summary.json` and `report.md` were written. The branch artifacts and mathematical sources are unchanged.