INDEPENDENT REBUILD AUDIT: Lean formalization of Paper II, Traverso Gianini, "Triangle decompositions II: Robust absorption for typed triangles" (doi:10.5281/zenodo.23502224)
=====================================================================================================

Status: FINAL (audit complete). An independent rebuild of an outside result that has not been refereed. The mathematics and the
Lean formalization are by Juan Pablo Traverso Gianini, written with AI assistance as disclosed in its
formalization.yaml (Aristotle/Harmonic, Claude, ChatGPT/Codex). This receipt only records what one machine checked.
It is not a review of the paper and it is not an endorsement.

Auditor: Ford (P42), on a redacted research machine, Mon Nov 2 2026, 8:14 AM – 10:45 AM MST (UTC-7).
Everything ran at nice 19, limited to cores 12-19 (taskset), inside ~/ford/nashwilliams2.
The audited clone was not modified: `git status --porcelain` was empty (0 lines) before the build and after.

0. FALSIFIERS (fixed by the task brief before the build started)
  F1  `lake build` fails at the pinned commit with the repo's own toolchain and Mathlib pin.
  F2  `#print axioms` on any main theorem shows something besides propext / Quot.sound / Classical.choice
      (for example sorryAx, Lean.ofReduceBool from native_decide, or a custom axiom).
  F3  The modules Paper I (jtraverso/nash-williams-lean @ 2603197) imports from Paper II differ from what this
      repo proves, or the imported statements elaborate differently.
  F4  The Challenge (statement) file and the Solution file elaborate to different statements.
  F5  An independent kernel (not Lean's own) rejects the exported proof terms.
  Result: F1-F5 did not fire. nanoda, con-ron and leanchecker --fresh all accepted (last finished 10:45:07 AM MST).

1. PINNED SOURCE
  Repo:       https://github.com/jtraverso/typed-triangle-absorption
  Commit:     673c6d4118b5679783bafa7606fd2c611161a254
              (2026-10-23 1:04 AM MDT; "Add Palomar mechanical preflight workflow")
  Registry:   none. formalization.yaml says Palomar's Comparator, NanoDa verification and editorial review
              "have not yet been requested", so there are no registry hashes to compare against.
  Toolchain:  leanprover/lean4:v4.35.0-rc3 (release candidate; same as Paper I). Module system.
  Mathlib:    c55e6e786f49471c72fbddbec5415808896aec1e (the repo's own pin; same pin as Paper I)
  Size:       1,514 tracked .lean files, 812,935 lines. Solution's local import closure is 1,513 modules
              (everything except Challenge).
  sha256:     Challenge.lean 6b5464784fd38e2624fc0ad7a76e5625b224cb2dff7a53c82c9ff2d3589c4ff2 (18,441 bytes)
              Solution.lean  6b67b5e5cb3d1926c659247ead73f765815d683464b50c7faaf699c77db1c874 (525 bytes;
              it only re-exports PaperII.Core, PaperII.Families and PaperII.PaperIApplications)

2. BUILD  (F1: did not fire)
  `lake exe cache get`: 8,942 Mathlib files decompressed, 0 downloaded, rc 0.
  `lake build PartitionedTriangleAbsorption Challenge Solution`: rc 0. "Build completed successfully (10475 jobs)."
  Started 8:16:21 AM MST and ended 9:11:01 AM MST, so the wall time was 3,280 s (54.7 min) on 8 cores
  at nice 19, with Mathlib coming from cache. No `error` lines in the log.
  The only `declaration uses sorry` warnings (6 total) are in Challenge.lean (lines 211, 228, 248, 261, 320,
  379). That is the statement-only file, so they are expected; Solution does not import it.
  Log: ~/ford/nashwilliams2/build_full.log (58.7 MB; summary in build.out)

3. AXIOMS  (F2: did not fire)   [AuditAxioms2.lean, `lake env lean`, 79.1 s, rc 0]
  The six statements listed in formalization.yaml (Theorems A-D, balanced B, Lemma SC):
  'PartitionedTriangleAbsorption.BlowupB.teoremaB_of_keevash' (Thm B)               : [propext, Classical.choice, Quot.sound]
  'PartitionedTriangleAbsorption.BlowupB.teoremaB_balanced' (balanced B)            : [propext, Classical.choice, Quot.sound]
  'PaddedGeneral.RealInverse.keevashTypedSpec_of_threeStepLinks' (Thm A)            : [propext, Classical.choice, Quot.sound]
  'PartitionedTriangleAbsorption.BlowupB.FiniteCensus.keevashTypedSpec_of_admissible' (Thm D) : [propext, Classical.choice, Quot.sound]
  'PartitionedTriangleAbsorption.BlowupB.F0Direct.theorem146_ordered' (Thm C)       : [propext, Classical.choice, Quot.sound]
  'PartitionedTriangleAbsorption.BlowupB.LemmaSC.absorber_onePart' (Lemma SC)       : [propext, Classical.choice, Quot.sound]
  Plus the declarations Paper I routes through:
  'PaddedGeneral.RealInverse.idealized_F12'                                         : [propext, Classical.choice, Quot.sound]
  'PaddedGeneral.RealInverse.keevashTypedSpec_F123'                                 : [propext, Classical.choice, Quot.sound]
  'PaddedGeneral.RealInverse.nearlyComplete_F123'                                   : [propext, Classical.choice, Quot.sound]
  'NashWilliams18.PaperII.margin_four_colour_decomposition'                         : [propext, Classical.choice, Quot.sound]
  None of these depend on sorryAx, Lean.ofReduceBool or a custom axiom.
  The source's own `#print axioms` lines in the build log show only subsets of the standard three.

  Escape-hatch grep over all 1,514 tracked .lean files (grep.out):
  - Zero hits for native_decide, implemented_by, unsafe, opaque, @[csimp], run_cmd, #eval, ofReduceBool,
    debug options, `syntax`, and top-level `axiom` declarations.
  - `sorry`: 6 in Challenge.lean; the other 4 are in doc comments ("without `sorry`", "no sorry").
  - `admit`: 4 hits, all the English word "admit".
  - `extern`: 12 hits, all the English word "external" in comments.
  - `Lean.Elab`: 9 hits, all `public import Lean.Elab.Tactic.{Omega,NormCast}` (core tactics).
  - 11 local tactic `macro` shorthands (fanclose, tclose, kcls, ...), which are benign.
  - set_option only for maxHeartbeats, maxRecDepth, synthInstance.*, Elab.async, hygiene,
    linter.unusedSectionVars and exponentiation.threshold.
  - 1,434 x `decide := true`, which is kernel decide, not native.
  - Side note: LatinCore/Cycles/DenseSpec.lean describes a `DenseRefiner` spec as OPEN. It is not a
    hypothesis of any of the six exported theorems, and the axiom output shows nothing is left assumed.

4. INDEPENDENT KERNELS  (F5: did not fire)
  `leanexport Solution -- <the 6 theorems>`: rc 0, 757.9 s, max RSS 17.3 GiB. Export 6,563,420,845 bytes,
  sha256 fcc6c12256d6f48bae23805fc284387cb697223b75d6979c87bd055fd69c8423 (/data/ford/nashwilliams2/solution_export.ndjson).
  - nanoda (independent Rust kernel), permitted_axioms = [propext, Classical.choice, Quot.sound],
    unpermitted_axiom_hard_error = true, Nat/String extensions on (nanoda2.json):
    ACCEPTED. rc 0, "Checked 203860 declarations with no errors", wall 3,741.4 s, max RSS 6.0 GiB
    (started 9:24:00 AM MST, finished ~10:26 AM MST). The only axioms printed are propext, Quot.sound and
    Classical.choice. Log ~/ford/nashwilliams2/nanoda.out.
  - con-ron --verified --jobs=4 --progress: ACCEPTED. rc 0, checked 201,069 / 201,069, "accepted 201943
    declarations (--verified)", wall 2,724.5 s, max RSS 10.7 GiB, finished 10:24:05 AM MST.
    Log ~/ford/nashwilliams2/conron_parallel.out. (A second, sequential con-ron run started by post.sh at
    10:26:21 AM MST, log conron.out, is a redundant repeat; it was stopped unfinished at ~10:53 AM MST once the verdict was final.)
  - leanchecker --fresh Solution (Lean's own kernel replaying the whole import closure):
    ACCEPTED. Exit status 0 (LC_RC 0), no error lines, started 9:11:19 AM MST, finished 10:45:07 AM MST
    (wall 1:33:47, user 5,111.5 s, max RSS 13.3 GiB; nice 19, cores 12-15). Log ~/ford/nashwilliams2/leanchecker.out.

5. STATEMENT MATCH
  Challenge vs Solution (F4: did not fire): `#check` with pp.all of the 6 theorems and `#print` of 40 supporting
  definitions (IdChallenge.lean vs IdSolution.lean, which differ only in `import Challenge` / `import Solution`):
  both rc 0, 0 errors, outputs identical except the final timing line (line 1574, "WALL 6.53 s" vs "7.04 s").
  The Challenge uses the source definitions (not opaque holes) and imports Mathlib only, per formalization.yaml.

  Paper I imports vs Paper II (F3: did not fire):
  - Paper I @ 2603197 imports Paper II through two modules:
    PartitionedTriangleAbsorption.BlowupB.PaddedGeneral.RealInverse.RoutedPaper and
    PartitionedTriangleAbsorption.F0OrderedTheorem.
    Their joint Paper I closure has 574 PartitionedTriangleAbsorption modules: 573 byte-identical to this repo
    (CRLF-normalised), 0 different, 1 missing (the root aggregator PartitionedTriangleAbsorption.lean, which is
    not part of the closure in this repo). No non-PTA local modules (closure_match.out).
  - Whole-tree comparison (tree_diff.out): Paper I's Solution closure has 819 PTA modules; 622 also exist here and
    all 622 are identical; 197 are Paper-I-only staging modules (e.g. *Stage121.lean) that are built and checked
    in the Paper I audit (receipt nash_williams_paper1_lean_audit_20261101.txt), not here. 0 files differ.
  - Cross-projection (XProj.lean: pp.all `#check` of idealized_F12, theorem146_ordered, keevashTypedSpec_F123,
    theorem147_of_keevash, plus `#print` of 45 definitions, run against both trees): outputs are byte-identical
    for all 1,622 lines; Paper II's file only has the extra timing lines. Both runs give rc 1 for the same
    reason: my audit file asked for LemmaSC.onePart and LemmaSC.K3fam, which are not in the two imported
    modules' closure (Paper I does not use Lemma SC). That is an error in my audit file, not in either repo.
    In both trees idealized_F12 and theorem146_ordered depend only on the standard three axioms.

  Scope (from the Challenge statements, as disclosed in formalization.yaml):
  - Theorem B and balanced B keep `KeevashTypedSpec F` (the typical-host property) as a hypothesis.
    Theorems A and D prove KeevashTypedSpec for four-label families (A: under FamilyFacts + ThreeStepLinks;
    D: every family of 3-label multisets on Fin 4 using every label, each label with a forbidden partner).
  - Theorem C keeps its semidense and non-extremality assumptions (ordered edit cost).
  - Lemma SC keeps explicit physical hinge supply and two explicit budgets.
  - No decomposition theorem for arbitrary divisible hosts and no equivalence with Keevash's labelled-complex
    framework is claimed. Delcourt-Postle Theorem 13.16 and their unpublished ref. 17 are "not assumed".

6. PALOMAR COMPARISON
  Not applicable: no Palomar entry yet (Comparator/NanoDa/editorial review "not yet requested").
  formalization.yaml: sorry_count 0, axioms [], review "agent-reviewed" (ChatGPT/Codex acting for the author),
  "No independent human review of this formalization is claimed." author_endorsement for Paper II: "participated".
  Its related_formalizations entry points to nash-williams-lean @ aa032bb (not 2603197); the file-level match
  in section 5 was done against 2603197, the commit audited for Paper I.

7. VERDICT
  PASS on build, axioms, Challenge/Solution identity and the Paper I to Paper II match. It builds cleanly at
  the pinned commit. All six exported theorems and the four Paper I route declarations depend only on the
  standard axioms. Everything Paper I imports from Paper II is byte-identical here and elaborates identically.
  Two independent kernels (nanoda and con-ron) accepted the exported proof terms of all six theorems, and
  Lean's own kernel (leanchecker --fresh) re-checked the whole Solution import closure with exit status 0.
  None of the falsifiers F1-F5 fired. Scope limits in sections 5 and 8 still apply.

8. CAVEATS / OPEN ITEMS
  - The paper is a preprint and has not been refereed. The Lean code is AI-assisted and agent-reviewed only.
    Lean checks the logic of the stated theorems; it does not check that they say what the paper says.
    I did not do a line-by-line comparison of the six statements with the preprint text.
  - Theorem D is computer-assisted: Python generated finite candidate certificates; per the yaml, Lean proves
    their coverage, uniqueness and use. The axiom check confirms nothing is assumed.
  - Thresholds (ε, N, δ, η) are existential, not explicit. Vertex types are in universe 0 where required.
  - The toolchain is a release candidate (v4.35.0-rc3) and the project uses the module system.
  - I did not run the author's tools/check_palomar.py, because it writes tools/check_report.txt into the repo.
  - nanoda and con-ron are both pinned to cores 16-19, so they share 4 cores; expect long wall times.
  - post.sh started a second, sequential con-ron run (log conron.out); it was redundant and was stopped
    unfinished after the parallel run had already accepted.
  - A first elaboration pass (post.sh) failed with rc 1 because of a relative-path error in my scripts
    (outputs kept in failed_relpath/); elab.sh reran them with absolute paths, and those are the results above.

9. REPRODUCE
  git clone https://github.com/jtraverso/typed-triangle-absorption && cd typed-triangle-absorption
  git checkout 673c6d4118b5679783bafa7606fd2c611161a254
  nice -n 19 lake exe cache get && nice -n 19 lake build PartitionedTriangleAbsorption Challenge Solution
  nice -n 19 lake env lean ../AuditAxioms2.lean
  nice -n 19 lake env lean ../IdChallenge.lean > a; nice -n 19 lake env lean ../IdSolution.lean > b; diff a b
  nice -n 19 lake env lean ../XProj.lean    # in both this repo and nash-williams-lean @ 2603197; diff outputs
  python3 ../cmp_trees.py; python3 ../cmp2.py   # file-level closure match against Paper I
  lake env leanexport Solution -- <the 6 theorems> > solution_export.ndjson
  nanoda_bin nanoda2.json ; con-ron --verified --jobs=4 solution_export.ndjson ; lake env leanchecker --fresh Solution
  (Audit files: ~/ford/nashwilliams2/{AuditAxioms2,IdChallenge,IdSolution,XProj}.lean, cmp_trees.py, cmp2.py,
   nanoda2.json and *.out)

10. CREDITS
  Mathematics and formalization: Juan Pablo Traverso Gianini (jtraverso), with AI assistance as disclosed.
  Background: Keevash (arXiv:1802.05900); Delcourt-Postle (arXiv:2402.17855, arXiv:2606.11178);
  Barber-Kühn-Lo-Osthus-Taylor (JCTA 151, 2017).
  Independent kernels: nanoda (ammkrn), con-ron. Mathlib community.