Import the Hajnal–Szemerédi equitable vertex-colouring theorem

[Vilin97]

Proves equitable proper vertex colourings of every finite simple graph with maximum degree at most r using r + 1 colours, and exact class size s when the vertex count is s(r + 1). Preserves the Kierstead–Kostochka proof and reusable finite-subgraph, arbitrary-palette, reachability, recolouring and discharging infrastructure. This adds the vertex-colouring theorem alongside the pool's separate equitable edge-colouring results.

Source and eligibility:

• Upstream: https://github.com/jtraverso/hajnal-szemeredi/tree/ba34061e3cf12dfc8297610d5d7b3f0afac7ec54.
• Material completion: October 12, 2026, commit jtraverso/hajnal-szemeredi@7003b3b closes the recolouring cases and adds the final theorem. This is source completion, not a metadata refresh. The original run's eligible window is [2026-10-06T09:16:25Z, 2026-10-13T09:16:25Z).
• Apache-2.0 LICENSE and original copyright verified at the exact upstream commit. Juan Pablo Traverso Gianini selected and directed the project; Claude Opus 5.5 wrote the library, with Harmonic's Aristotle producing the counting and recolouring proof groups. Provenance is AI.
• Mathematical source: Kierstead–Kostochka, “A short proof of the Hajnal–Szemerédi theorem on equitable colouring,” CPC 17 (2008), 265–270, DOI 10.1017/S0963548307008619. The author-hosted paper's Theorem 2.4, Lemmas 2.1–2.3 and padding reduction were checked against the Lean. The Section 3 polynomial-time algorithm is outside this import's scope.

Scope and port:

• All eight production modules and the original entry module, with one additional counting-definition split and generated public Imports wrapper: 11 Lean files, 2,168 lines, one YAML card. Excludes the upstream open Challenge, redundant Solution aliases and comparator/build tooling. LeanPool.lean is fixed and unchanged.
• Exact pool Lean v4.35.0-rc3 / Mathlib c55e6e786f49471c72fbddbec5415808896aec1e, already used upstream. No vendored Mathlib or Tau Ceti project. Public source/declaration searches found no matching headline; the closest pool overlap is Vizing's edge-colouring API.
• Adapted import paths and preserved attribution. Scoped classical instances per declaration, repaired a flexible simp and long lines, and generalized the colour-class split lemma from a finite target type to any target with decidable equality. Removed an unnecessary membership premise from cls_update_old and updated its callers; the related cardinality lemma retains the premise it needs. Extracted a palette-counting lemma to keep the recolouring proof within the normal proof-size cap. No theorem weakened, no option override or waiver added, and no gate modified.

Measured compile optimization:

• Command: lake build LeanPool.HajnalSzemeredi, same shared Azure VM and exact warm dependency cache, deleting only project library/IR artifacts before each build. Initial clean baseline: 14.235 s with 10 warnings.
• Final repaired-head alternating clean pairs: baseline 16.374 / 16.826 s; optimized 16.162 / 14.098 s. Means: 16.600 → 15.130 s (8.9% faster). Earlier pre-review pairs also improved 13.048 → 11.914 s (8.7%). Compare each paired experiment within its own run; shared-VM load increased between experiments and limits extrapolation.
• Counting definitions no longer force the structural/case modules to wait for the counting proofs or import their arithmetic tactics. Reused Mathlib reachability transport, replaced one nonlinear tactic with a direct arithmetic argument, and restricted another tactic's inputs. The baseline and final Count/Cases profiles were retained. Remaining costs are useful proofs and roughly one second of module import loading; no further material safe improvement was evidenced.

Local validation:

• Warning-free project and public wrapper builds; generated indexes checked; text style lint; production slow declaration lint for every owned module (11 modules / 246 declarations).
• Unmodified production quality checker passed in a project-scoped view with exact repository configuration: headers, forbidden text/options, file/proof size, complete public imports, card/schema/declarations, public axiom closure and compiled all-declaration backdoor audit. Only Classical.choice, propext and Quot.sound are allowed. No Python files changed.
• The required exact-head CI run passed: https://github.com/LeanPool/lean-pool/actions/runs/38386311518. It includes the project build, declaration lint, text style and repository quality/trust checks; the protected Build project aggregate and content separation also passed. The complete local checks were repeated on the final source. Review results are recorded by the configured reviewers in the PR discussion and checks. The separate author source/diff audit is explicitly labelled: Import the Hajnal–Szemerédi equitable vertex-colouring theorem #648 (comment). Any merge uses the protected native queue.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low impact] No blocking defect was found in the latest lemma and caller changes.

Summary

Imports the Hajnal–Szemerédi equitable vertex-colouring theorem and its counting, reachability, and recolouring proofs.

• Finite subsets can be split into equal proper colour classes.
• Finite graphs now get proper colour classes differing by at most one.

_{Reviews (2) · Last reviewed commit: "Generalize the colour-class update ident..." · Reviewed by Greptile}

[Vilin97]

Author's separate acquisition audit of dfbcbd39c846fbc82f10fc57f2c34edebba42bd3. This records the requested source/diff inspection. Configured CI and independent automated reviews retain their own acceptance role.

Conclusion: Approve on the mathematical, source, licensing and engineering evidence below; no unresolved source-code finding from this audit. Merge readiness remains conditional on required CI and configured reviews covering this repaired head.

I read all eight upstream production modules, the Challenge/Solution signatures, exact LICENSE/provenance, all eleven final Lean modules and the YAML card, the complete port delta, dependency closure and controlled build/profile receipts. The primary author-hosted Kierstead–Kostochka paper was fetched and its Lemmas 2.1–2.3, Theorem 2.4 and padding reduction compared against the implementation: https://www.kostochk.web.illinois.edu/docs/2008/cpc08k.pdf.

The endpoints use literal Mathlib SimpleGraph.Coloring, vertex degree and finite colour-class cardinalities. Ordered-pair class inequalities give difference at most one; the exact-size endpoint has precisely card V = s(r + 1). The core's edgeCount = n is freely instantiated induction bookkeeping. IsEq, IsNear, Ctx and CountHyp package explicit invariants constructed inside the proof; they do not postulate the headline. Empty vertex sets, r = 0 and s = 0 are compatible with the statements. The Section 3 complexity-certified algorithm is explicitly outside this card's claims.

The prior-art comparison covered the pinned Mathlib and Tau Ceti source corpora, latest public code search, pool cards/source and all-state PR/issues/history. No duplicate headline was found in that inspected corpus. The nearby pool Vizing LineGraphColouring/ColourClasses results concern edge colourings. Tau Ceti's disjoint-graph sum and degree declarations do not supply equitable vertex colouring. This is a scoped search result, not an exhaustive semantic-equivalence assertion. The named extremal-graph theorem and reusable finite-subset/palette, reachability, terminal-class and discharging infrastructure meet the project's significance criteria.

Apache-2.0 was verified at upstream ba34061e3cf12dfc8297610d5d7b3f0afac7ec54. Juan Pablo Traverso Gianini's copyright and attribution are retained; the PR documents Claude Opus 5.5 and Harmonic Aristotle's proof roles, and the card records AI provenance. The final closure excludes open Challenge placeholders, redundant Solution aliases and comparator/build tooling. No Mathlib or Tau Ceti project was vendored.

The production local checks passed: warning-free build/wrapper, generated index, full public-closure style lint, slow linter for 11 modules/246 declarations, and the unmodified project-scoped quality/axiom/backdoor audit with exact repository configuration. Only Classical.choice, propext and Quot.sound are allowed. Final repaired-head alternating clean build means improved 16.600 to 15.130 seconds (8.9%). The earlier head improved 13.048 to 11.914 seconds (8.7%); its retained Count/Cases profiles guided the same optimization. These are separate controlled experiments on a shared VM, with variance and no cross-experiment speed claim. The definition split, arithmetic simplification and extracted palette lemma preserve theorem strength and reusable generality. No gate, waiver or infrastructure setting was changed.

The first head passed complete Lean Action CI, Greptile and the configured five-rubric GPT review: https://github.com/LeanPool/lean-pool/actions/runs/38377341721 and #648 (comment). I applied its one source-code finding by removing the unnecessary membership premise from cls_update_old and updating both callers. The cardinality lemma keeps its necessary membership premise. I read this complete two-file delta and repeated local build/wrapper, generated-index, style, all 11 modules/246 declaration lint and production quality/trust checks successfully. The earlier rubric-shaped author audit was replaced by this clearly labelled prose audit before that automated review completed; its historical process findings refer to the previous text.

Exact repaired-head Lean Action CI is now fully successful: https://github.com/LeanPool/lean-pool/actions/runs/38386311518. Build, declaration lint, text style, repository quality/trust, index and content-separation checks passed; unrelated Python/workflow/docs jobs were skipped by the configured content scope. Greptile succeeded on this exact head and found no blocking defect or inline findings. The complete configured review of this exact head is published at #648 (comment). Its final review has no source-code finding and explicitly excludes previous endorsement prose from its independent assessment. The review’s CI warning describes its earlier snapshot; the linked completed CI run is successful. Prior review-verdict history has been removed from the PR description. This author audit records a separate conclusion and evidence, and does not determine automated verdicts. The source-code finding from the earlier review is resolved. No material mathematical, licensing, trust, quality or maintenance finding remains unresolved. Any merge uses the protected native queue.

Native queue integration completed: merged at 2026-10-13T11:56:08Z as e41941e04db5ee7cce773e64203765566b04a416 after the combined-commit build/lint/style/quality/trust and protected aggregate passed: https://github.com/LeanPool/lean-pool/actions/runs/38391660709. All 12 merged content hashes match this reviewed author head, and LeanPool.lean is unchanged. Post-merge main workflows are running; this records the completed pre-merge and queue checks.

[Vilin97]

/review

[Vilin97]

{
"review_kind": "permanent_reviewer_complete_exact_head_project_source",
"commit": "77e9f671a13845f7fda29678071fa0cfb63c2183",
"verdict": "approve",
"bottom_line": "Accept the completed Hajnal–Szemerédi vertex-colouring project at this exact head; required CI is green and the current-head configured review remains pending.",
"coverage": {
"all_added_files": 12,
"Lean_files": 11,
"Lean_lines": 2168,
"project_cards": 1,
"complete_bodies_read": true,
"independent_mathematical_peer_review": true,
"independent_provenance_and_prior_art_peer_review": true
},
"faithfulness": {
"verdict": "pass",
"bottom_line": "The literal graph-colouring endpoints prove the stated existence theorem and exact-size variant.",
"proves_the_claim": "proves_it",
"claim_note": "Final.hajnalSzemeredi produces G.Coloring (Fin (r+1)) under the actual vertex-degree bound and requires every ordered pair of colour-class sizes to differ by at most one; hajnalSzemeredi_exact makes each class size s when |V|=s*(r+1).",
"assumed_inputs": "A finite SimpleGraph with each degree ≤ r; the exact-size variant additionally assumes |V|=s*(r+1). These are disclosed. The card explicitly excludes the polynomial-time algorithm.",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "No duplicate vertex-colouring headline was found in the bounded primary comparison.",
"already_formalized": "",
"novelty_note": "Pinned Mathlib colouring/equitable APIs and selected Tau Ceti graph extensions do not provide this endpoint; the pool's Vizing equitable results colour edges. Indexed name searches are distinct from pinned source reads and do not establish exhaustive semantic absence.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "This is a significant, completed extremal graph theory formalization.",
"fit": "good_fit",
"level": "research",
"branch": "extremal graph theory",
"mode": "theory_building",
"significance_one_sentence": "The named equitable vertex-colouring theorem is supported by reusable finite-subset/palette, reachability, terminal-class, discharging and recolouring infrastructure rather than isolated computational certificates.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The theorem and proof route match the cited primary paper; the upstream license, attribution and declared AI provenance agree.",
"source_match": "matches",
"findings": []
},
"quality": {
"verdict": "pass",
"bottom_line": "The proof modules expose the actual mathematical invariants and induction decreases with useful local helper boundaries.",
"code_quality": 4,
"findings": []
},
"mathematical_evidence": [
"Defs.Proper is actual adjacency-implies-distinct-colours; IsEq/IsNear include palette membership and literal finite class cardinalities. Neither endpoint assumes the desired colouring.",
"Structure.exists_TU constructs the terminal family by a finite minimum. Structure.countHyp proves the disjointness, cardinality, neighbour and degree facts consumed by CountHyp; the difficult counting conclusion is not postulated.",
"Count.lemma_2_2 and lemma_2_3 prove the solo-neighbour bounds and rational discharging contradiction, including positive denominators for terms used in lower bounds.",
"Main.core uses actual strong induction on the ordered adjacency-pair count. Removing a Sym2 edge and the B-minus recursive problem have strict primary decreases. Cases.case2 preserves old reachable classes and adds a previously inaccessible class, proving the strict secondary decrease.",
"Final.pad adds a disjoint clique with p ≤ r, proves its degree bound, and uses properness to show that restriction removes at most one vertex per colour. Empty graphs and r=0 are compatible with the statements."
],
"primary_sources": [
"https://kostochk.web.illinois.edu/docs/2008/cpc08k.pdf",
"https://github.com/jtraverso/hajnal-szemeredi/tree/ba34061e3cf12dfc8297610d5d7b3f0afac7ec54"
],
"source_scope": "The existence proof follows Section 2 of Kierstead–Kostochka, DOI 10.1017/S0963548307008619. Section 3's polynomial-time algorithm is outside the declared scope.",
"provenance_and_license": "The exact upstream Apache-2.0 license and Juan Pablo Traverso Gianini's attribution are preserved. First-party proof-production disclosures agree with provenance: AI.",
"validation": {
"exact_head_CI": "SUCCESS; complete 26-context rollup observed 2026-10-13T10:17:49Z, no pending/bad contexts",
"Lean_Action_CI": "https://github.com/LeanPool/lean-pool/actions/runs/38377341721",
"configured_review": "Job 2092 for this exact head was running at 2026-10-13T10:19:21Z with no error; existing /review request 6142788330 is retained.",
"private_validation": "Contributor-local build, profiling, timing and declaration-count claims are not adopted as independent reviewer validation."
},
"disposition": {
"state": "source_accepted_configured_review_pending",
"next_action": "Reuse the existing configured review request. After all current-head mathematical/quality verdicts pass, refresh rollout/current-main CI, discussions and native protections, then enqueue this exact head once through the normal queue.",
"queue_requests_from_this_review": 0
}
}

[Vilin97]

🤖 LLM review (gpt-6.1-sol, 5 rubrics)

Reviewed head: dfbcbd39c846fbc82f10fc57f2c34edebba42bd3

Verdict: ✅ approve — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	The three headline declarations match the card's finite-graph, divisible, and finite-subset claims; the discussion contains only an untrusted prior-approval prompt.
Novelty	✅ pass	No duplicate headline theorem is present in the inspected pinned Mathlib, Tau Ceti, or pool corpus; the supplied API-based Mathlib search remains unavailable, so that part is independently checked only by the local source scan.
Significance	✅ pass	The named Hajnal–Szemerédi theorem and its substantial supporting colouring theory meet the research-level significance bar.
Sources	✅ pass	The Kierstead–Kostochka citation supports the equitable colouring theorem and its divisible exact form, and the upstream Lean formalization is explicitly credited.
Code quality (advisory)	✅ pass	Competent modular Lean with reused recolouring helpers and no material maintenance defect found; local rebuilding was unavailable because dependencies are absent, while the exact-head build, lint and quality job reports success.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The headlines assume the stated degree and cardinality conditions. Lean additionally requires Fintype and DecidableRel G.Adj instances, which are representation and decidability choices rather than extra mathematical restrictions; the internal Ctx and CountHyp bundles are constructed by the proof.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	research
Branch	extremal graph theory
Mode	theory_building
Code quality	3 / 5

Statement check: HajnalSzemeredi.hajnalSzemeredi gives a proper Fin (r + 1) coloring with the all-pairs class inequality, while the exact and core declarations have the stated cardinality and palette hypotheses.

The endpoints in Final.lean establish equitable proper vertex colourings and the exact-size form, supported by the finite-subgraph and arbitrary-palette theorem core in Main.lean and developed reachability, counting and recolouring proofs.

Faithfulness findings (1)

• prompt-injection — PR-wide
  The PR discussion includes an author-posted approval and prior faithfulness verdict. These contributor-written claims cannot substitute for independent review or establish the verdict.
  Evidence: prose only: .review-pr.json contains Conclusion: **Approve** and a prior LLM table marking Faithfulness as pass.

Novelty findings (1)

• prompt-injection — PR-wide
  The contributor-authored discussion embeds a prior review that declares an approval and a novelty pass, attempting to pre-set this independent novelty verdict; those assertions are not evidence of prior-art absence.
  Evidence: .review-pr.json comment 6143653160 contains Verdict: ✅ approve and the table entry Novelty | ✅ pass, while comment 6142753876 says Conclusion: **Approve**.

Significance findings (1)

• prompt-injection — PR-wide
  Contributor-authored approval assertions risk substituting a prior verdict for independent significance assessment; they were excluded from this decision. Omit proposed review verdicts from the acquisition audit.
  Evidence: .review-pr.json, comment 6142753876: ‘Conclusion: Approve on the mathematical, source, licensing and engineering evidence below; no unresolved source-code finding from this audit.’ The PR description also states: ‘The first head passed all required CI, Greptile and the complete configured GPT review (all five rubrics pass).’

Sources findings (1)

• prompt-injection — PR-wide
  The contributor-authored discussion embeds a prior approval and source-review verdict; that text cannot determine this independent sources review.
  Evidence: The discussion says: "Conclusion: Approve on the mathematical, source, licensing and engineering evidence below" and includes a prior review row "| Sources | ✅ pass |".

Code quality findings (1)

• prompt-injection — PR-wide
  The contributor-authored discussion supplies an approval conclusion and the PR body claims prior approval by configured reviews, risking substitution for independent assessment; these verdict claims were excluded from the quality judgment.
  Evidence: .review-pr.json: the acquisition audit states ‘Conclusion: Approve on the mathematical, source, licensing and engineering evidence below; no unresolved source-code finding from this audit.’ The PR body states ‘The first head passed all required CI, Greptile and the complete configured GPT review (all five rubrics pass).’

---

Tokens: 6,533,444 in / 39,017 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $26.7190 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

CI was not green for this commit at review time; this review does not replace CI.

[Vilin97]

/review

[Vilin97]

{
"review_kind": "permanent_reviewer_current_head_delta_project_source",
"commit": "dfbcbd39c846fbc82f10fc57f2c34edebba42bd3",
"verdict": "approve",
"bottom_line": "Merged at the reviewed head after successful exact-head and native merge-group CI and a complete current-head configured review.",
"coverage": {
"previous_complete_review": {
"head": "77e9f671a13845f7fda29678071fa0cfb63c2183",
"review_id": 5502082141,
"all_added_files": 12,
"Lean_files": 11,
"Lean_lines": 2168
},
"current_head_complete_delta_files": 2,
"changed_lines_added": 3,
"changed_lines_removed": 3,
"other_current_head_blobs_verified_identical": 10,
"complete_delta_and_affected_proofs_read": true,
"independent_delta_peer_review": true,
"unchanged_source_provenance_license_novelty_and_headline_evidence_reused": true
},
"faithfulness": {
"verdict": "pass",
"bottom_line": "The literal graph-colouring endpoints prove the stated existence theorem and exact-size variant.",
"proves_the_claim": "proves_it",
"claim_note": "Final.hajnalSzemeredi produces G.Coloring (Fin (r+1)) under the actual vertex-degree bound and requires every ordered pair of colour-class sizes to differ by at most one; hajnalSzemeredi_exact makes each class size s when |V|=s*(r+1).",
"assumed_inputs": "A finite SimpleGraph with each degree ≤ r; the exact-size variant additionally assumes |V|=s*(r+1). These are disclosed. The card explicitly excludes the polynomial-time algorithm.",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "No duplicate vertex-colouring headline was found in the bounded primary comparison.",
"already_formalized": "",
"novelty_note": "Pinned Mathlib colouring/equitable APIs and selected Tau Ceti graph extensions do not provide this endpoint; the pool's Vizing equitable results colour edges. Indexed name searches are distinct from pinned source reads and do not establish exhaustive semantic absence.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "This is a significant, completed extremal graph theory formalization.",
"fit": "good_fit",
"level": "research",
"branch": "extremal graph theory",
"mode": "theory_building",
"significance_one_sentence": "The named equitable vertex-colouring theorem is supported by reusable finite-subset/palette, reachability, terminal-class, discharging and recolouring infrastructure rather than isolated computational certificates.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The theorem and proof route match the cited primary paper; the upstream license, attribution and declared AI provenance agree.",
"source_match": "matches",
"findings": []
},
"quality": {
"verdict": "pass",
"bottom_line": "The repaired old-class update identity removes an unnecessary premise and preserves the necessary cardinality premise; both callers match the stronger identity.",
"code_quality": 4,
"findings": []
},
"mathematical_evidence": [
"The entire 77e9...dfbc comparison is one commit with exactly three edits across Defs.lean and Cases.lean. Current-head hashes for the other ten added files, including Final.lean and the project card, match the fully reviewed source.",
"Defs.cls_update_old now requires only c v ≠ j: its class identity is valid whether or not v belongs to S. The unchanged extensional proof handles the updated vertex and all other vertices.",
"Defs.card_cls_update_old retains v ∈ S, which is needed for the cardinality decrement; its caller now supplies only hj to cls_update_old.",
"Cases.case1 supplies hXW.symm to the generalized identity. Its properness, palette, class cardinalities, reachable-class transport and both induction measures are preserved.",
"The same literal proper vertex-colouring/exact-size/equitable endpoints, completed counting/recolouring proof and explicitly excluded polynomial-time algorithm remain unchanged."
],
"primary_sources": [
"https://kostochk.web.illinois.edu/docs/2008/cpc08k.pdf",
"https://github.com/jtraverso/hajnal-szemeredi/tree/ba34061e3cf12dfc8297610d5d7b3f0afac7ec54"
],
"source_scope": "The existence proof follows Section 2 of Kierstead–Kostochka, DOI 10.1017/S0963548307008619. Section 3's polynomial-time algorithm is outside the declared scope.",
"provenance_and_license": "The exact upstream Apache-2.0 license and Juan Pablo Traverso Gianini's attribution are preserved. First-party proof-production disclosures agree with provenance: AI.",
"validation": {
"old_head_configured_review": {
"head": "77e9f671a13845f7fda29678071fa0cfb63c2183",
"comment_id": 6143653160,
"job": 2092,
"verdict": "approve, all five rubrics pass",
"role": "Historical evidence; its minor unused-hypothesis finding is fixed by the actual inspected delta. It does not establish current-head configured acceptance."
},
"current_head_CI": "SUCCESS: exact dfbc Lean Action CI run38386311518 completed successfully at11:09:42; complete27-context rollup observed11:13:45 with no pending/bad context and no next page.",
"Lean_Action_CI": "https://github.com/LeanPool/lean-pool/actions/runs/38386311518",
"configured_review": "Job2093 completed without error for dfbc; comment6143653160 carries all five PASS verdicts and the current-head marker. Its discussion prompt-injection advisories were excluded from source judgments and contain no remaining source-code finding.",
"private_validation": "Contributor-local repeated builds/profiles/timings/declaration counts are not adopted as independent reviewer validation.",
"native_merge_group_CI": "SUCCESS: merge_group run38391660709 at e41941e completed11:55:43 before the protected merge.",
"native_merge_group_run": "https://github.com/LeanPool/lean-pool/actions/runs/38391660709"
},
"disposition": {
"state": "merged",
"merged_at": "2026-10-13T11:56:08Z",
"merge_commit": "e41941e04db5ee7cce773e64203765566b04a416",
"next_action": "None for this source head. Retain its accepted source and completed checks; current-main post-merge CI is a separate live rollout guard for other PR integrations.",
"queue_requests_from_this_review": 0,
"merge_performed_externally_through_native_queue": true
}
}