[Vilin97]

This imports the complete classification of minimum universal collections of MacMahon cubes: twelve cubes are necessary and sufficient, exactly ten labelled inventories attain the minimum, and those inventories are the two-triangle collections in Conway's tableau. Repeated physical varieties are allowed initially and proved absent at the minimum. The classification resolves Johnson and Roldán's Conjectures 4 and 8 and preserves the geometric verification that connects the combinatorial model to physical face matching.

The preserved infrastructure includes the thirty varieties, all proper signed-axis rotations, coverage and uniqueness of all six-colour face assignments, injective allocations of physical cube copies, corner incidence/counting bounds, the degree-two classification, and explicit constructions for all 300 candidate/target pairs. Inventories have zero diagonal in the tableau; the thirty off-diagonal positions are the actual varieties. Only exterior faces must match. The model uses finite coordinate face directions and proper rotations. The upstream numerical target-count histograms are outside the Lean theorem claims.

Source and eligibility:

• Public upstream: jasondavies/macmahon-min-universal-sets, pinned at d8856c97e43e6fa66383c81b8ac4f5bd1c285bc8.
• Author: Jason Davies. Apache-2.0 license. provenance: AI, following the explicit proof-authorship disclosure: GPT-6-Astra developed the proof and Lean code under the author's direction; Claude Opus 5.5 contributed to manuscript review.
• Daily acquisition window: 2026-10-26 11:25:51 UTC ≤ completion < 2026-11-02 11:25:51 UTC. The substantive complete formalization first appears in b4bfe74, committed 2026-10-31 22:10:30 UTC, with proof simplification later that night. The selected snapshot's upstream check passed on 1 November, 00:01:06–00:02:53 UTC. Eligibility uses actual proof history and completion evidence.
• The current upstream README reports Palomar registration on 1 November. I could read the entry HTML, but the registry data endpoint returned HTTP 403, so that acceptance is reported from upstream rather than independently certified here.
• Primary sources read directly: Johnson–Roldán, arXiv:2407.13208v1, Conjectures 4 and 8; Haraguchi, arXiv:1408.3696v2, the prior minimum-size result. The multiset extension and the different Lean proof route are disclosed.

The import retains all sixteen upstream proof modules, now arranged as twenty-two proof modules. Comparator statement/bridge wrappers, diagnostic audits, numerical enumeration programs, manuscript and non-formal histograms are omitted. No additional Lake dependency is introduced. Exact-name, upstream-URL and mathematical-concept searches covered pool cards/code, all-state issues/PRs and history, and the pinned Mathlib/Tau Ceti sources. No duplicate classification was found; Mathlib's documentation mention of the MacMahon Master theorem concerns a different result.

Porting and measured optimization:

• Port from upstream Lean/Mathlib v4.35.0 to the pool's exact v4.35.0-rc3, Mathlib c55e6e786f49471c72fbddbec5415808896aec1e. Retarget imports and add headers, module/definition documentation, precise attribution, one YAML card and the generated public Imports.lean. LeanPool.lean is unchanged.
• Replace the broad Mathlib import with focused imports. Remove every heartbeat and recursion-depth override. Replace repeated classification normalization with a proved row-exhaustion lemma and direct row equalities. Split the thirty unchanged finite geometric checks into six independent target-row modules so their kernel work can run concurrently. An alternative that split each theorem into many tactic cases measured slower and was discarded.
• Preserve all 137 original named declaration statement texts modulo whitespace and module placement. Format generated data without changing any numeric entry, checked by parsing and comparing the complete tables. The 300 constructions and forty corner types are rechecked in the kernel. Generated tables use ordinary finite data, and their upstream generator is identified at the pinned source revision; they do not rely on unstable elaborator internals.
• Clean measurements use LEAN_NUM_THREADS=4 lake build LeanPool.MacMahon.Submission, the same VM/toolchain/options, prebuilt exact-pin dependency caches, and removal of this project's own build artifacts. Baseline 302.813 s; optimized mathematical code 198.486 s, 34.45% less wall time. Baseline file timings: Geometry 269 s, Rotations 75 s, Classification 53 s, Arithmetic 41 s. Optimized geometry checks occupy six modules (57–91 s in the clean run), aggregate 3.9 s; Classification 36 s and Arithmetic 33 s. Module timings overlap and are not additive. This VM is shared; these are observed measurements, not a guaranteed speedup. The final clean rebuild, including all definition documentation, passed in 247.889 s (18.14% below baseline); a contemporaneous host sample showed load averages about 51 on 16 logical CPUs. Both optimized measurements are disclosed because shared load affects wall time.

Local validation: the complete project/public-wrapper build is warning-free; generated indexes, Mathlib linters, style, full-repository static quality checks, all ten headline declaration resolutions, the axiom audit of 136 public declarations, and the compiled-environment audit of all 24 project modules pass. The upstream independent Python cube checker passes. All 137 original named type signatures and every numeric data entry were independently compared against the pinned upstream. No Python production files change. Hosted CI and configured reviews remain authoritative and will be reported separately. No merge or auto-merge is requested: the infrastructure priority hold remains respected until current-main validation is established, and any later accepted entry must use the protected native queue.

Recovery preserved the staged import and its measurements from the interrupted attempt, inspected the prior job log and current remote PRs/comments/announcements, and found no existing MacMahon import. Existing unrelated acquisition PRs, author branches and reviews are untouched. No announcement is posted before deployed documentation exists.

[Vilin97]

Comprehensive source and engineering review of 9ddc427022b708c6220c86a558eb2e2802f1f908. Conclusion: approve on source and local validation. Hosted CI and configured independent reviews remain required; the infrastructure hold prohibits queue and merge actions.

{
  "kind": "Separate comprehensive acquisition review; does not replace configured GPT or Greptile reviews",
  "reviewed_head": "9ddc427022b708c6220c86a558eb2e2802f1f908",
  "conclusion": "approve",
  "qualification": "Source and local engineering review approves. Hosted validation and configured independent reviews remain required. The current-main infrastructure hold prohibits queue, auto-merge and merge actions.",
  "coverage": {
    "changed_files": 25,
    "lean_modules": 24,
    "original_named_declarations_compared": 137,
    "original_type_signature_differences": 0,
    "numeric_tables": "Every entry compared against the pinned upstream; upstream independent geometric regeneration and all 300 explicit target solutions pass.",
    "partial_diff": false,
    "method": "Read every mathematical module, all endpoint declarations and their dependency closure; inspect all six geometry shards and generated-data structure and representative slices, with exhaustive numeric comparison and independent regeneration for the tables. Compare upstream source and the final port, rather than relying on its README."
  },
  "faithfulness": {
    "verdict": "pass",
    "bottom_line": "The ten advertised results agree with the Lean statements and the finite signed-axis geometric model.",
    "proves_the_claim": "proves_it",
    "claim_note": "minimum_size is an attained IsLeast, physical_exactly_ten counts the subtype of size-twelve zero-diagonal physically universal inventories, and physical_iff_two_triangles classifies those inventories structurally. Multiplicities range over all natural numbers; minimum_has_no_repeats is proved, not assumed.",
    "assumed_inputs": "Six distinct face colours; proper rotations; eight distinct physical copies; only exterior faces must match. DiagonalZero removes the six invalid tableau placeholders, as the card explicitly states. These are definitions of the puzzle, not imported classification assumptions.",
    "evidence": "PhysicalBuilds uses an embedding Slot \u21aa Stock a and \u2200 k, \u2203 r : Fin 24, FaceFits t (f k).1 k r. proper_rotation_iff, exposed_face_rule, face_assignment_coverage, face_assignment_unique and face_corner_equivalence establish the geometric interpretation. winner_properties and winner_universal supply nonvacuous minimum witnesses.",
    "findings": []
  },
  "novelty": {
    "verdict": "pass",
    "bottom_line": "No duplicate MacMahon cube classification was found in the inspected pool, Mathlib or Tau Ceti sources.",
    "already_formalized": "",
    "novelty_note": "Exact source URL, name and mathematical-concept searches covered current cards/code, all-state issues and PRs, main history, GitHub code search, and pinned Mathlib/Tau Ceti Lean sources. Mathlib's MacMahon Master theorem documentation concerns another theorem. This is bounded negative search evidence; unrestricted semantic equivalence across the entire dependency corpus is not certified.",
    "findings": []
  },
  "significance": {
    "verdict": "pass",
    "bottom_line": "A complete paper-anchored classification resolving Johnson\u2013Rold\u00e1n Conjectures 4 and 8, with independently reusable finite geometric infrastructure, merits preservation.",
    "fit": "good_fit",
    "level": "research",
    "branch": "finite combinatorics",
    "mode": "mixed",
    "significance_one_sentence": "The development strengthens the published distinct-variety conjectures to arbitrary inventories, proves the minimum is attained at twelve, and identifies exactly the ten two-triangle inventories.",
    "maintenance_note": "Data and WitnessData occupy 739 of the 2095 added lines, about 35%, including comments and formatting. These are ordinary finite numeric arrays; the pinned upstream generator and independent checker are identified. Regeneration requires the upstream scripts, which are not vendored into this content-only PR. All generated data is revalidated by ordinary kernel proofs and uses no unstable elaborator interface.",
    "findings": []
  },
  "sources": {
    "verdict": "pass",
    "bottom_line": "The two primary papers support the attributed claims, and the stronger multiset conclusion and finite geometry scope are disclosed.",
    "source_match": "matches",
    "evidence": "Read Johnson\u2013Rold\u00e1n arXiv:2407.13208v1, Conjectures 4 and 8, and Haraguchi arXiv:1408.3696v2, Theorem 4. Attribution names Jason Davies, the pinned upstream d8856c97e43e6fa66383c81b8ac4f5bd1c285bc8, Apache-2.0 licensing and AI proof authorship. Upstream's claimed Palomar acceptance is explicitly not independently certified because its data endpoint returned HTTP 403.",
    "findings": []
  },
  "quality": {
    "verdict": "pass",
    "bottom_line": "The port has coherent abstraction boundaries, removes all option escapes, and preserves statements while reducing measured compile cost.",
    "code_quality": 3,
    "evidence": "Reusable row_eq_of_two_unit_entries replaces repeated arithmetic normalization; six independent geometry modules expose finite checks for parallel compilation. Focused imports reduce the dependency graph substantially. Classification, arithmetic necessity, explicit sufficiency, and physical-model bridges remain separate. All 137 original named type signatures are preserved. The public axiom audit and compiled-environment audit pass with no exceptions.",
    "measurements": {
      "command": "LEAN_NUM_THREADS=4 lake build LeanPool.MacMahon.Submission",
      "conditions": "Same VM, exact pool pins and dependency cache, project build artifacts removed. Shared VM load is uncontrolled; overlapping module times are not additive.",
      "baseline_seconds": 302.8133360459469,
      "optimized_mathematics_seconds": 198.48630694672465,
      "final_documented_source_seconds": 247.88869902165607,
      "final_reduction_percent": 18.138116947384695,
      "baseline_hot_modules_seconds": {
        "Geometry": 269,
        "Rotations": 75,
        "Classification": 53,
        "Arithmetic": 41
      },
      "optimization_limit": "The baseline's broad import and oversized arithmetic normalization were repaired. Further splitting of individual geometry decisions was measured slower and rejected. No further material safe improvement was established; statements, readable proofs and kernel trust take precedence over speculative timing changes."
    },
    "findings": []
  }
}

[Vilin97]

/review

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 153.67 s (= 2.56 min) — user 439.90 s, sys 29.48 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 1,602,543 maxHeartbeats units across 22 valid files (2,055 added LOC).

Sum of lean --profile: 810947.5 ms (= 810.95 s) across 24 valid files. Import-excluded time: 793638.5 ms (= 793.64 s).

Count-heartbeats wall-clock total: 358.52 s. Repeated import cost inside lean --profile: 17309.0 ms (= 17.31 s).

Heartbeat values sum disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted from raw allocations to maxHeartbeats units by dividing by 1000. They include command elaboration and kernel checking, exclude imports, and include profiler overhead; they are not comparable to the deprecated linter's totals. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Commands	Errors
LeanPool/MacMahon/Geometry/TargetOne.lean	39	211,410	47.69	100.68	100.02	0.66	10	0
LeanPool/MacMahon/Geometry/TargetTwo.lean	39	211,397	41.55	102.59	101.92	0.67	10	0
LeanPool/MacMahon/Geometry/TargetFive.lean	39	211,335	36.19	101.10	100.42	0.68	10	0
LeanPool/MacMahon/Geometry/TargetThree.lean	39	211,323	37.08	99.88	99.23	0.65	10	0
LeanPool/MacMahon/Geometry/TargetFour.lean	39	211,310	47.93	101.98	101.32	0.67	10	0
LeanPool/MacMahon/Geometry/TargetZero.lean	39	211,235	45.41	102.39	101.72	0.66	10	0
LeanPool/MacMahon/Rotations.lean	82	144,813	33.77	86.96	86.28	0.68	21	0
LeanPool/MacMahon/Witness.lean	33	70,853	16.48	12.33	11.60	0.73	7	0
LeanPool/MacMahon/WitnessData.lean	523	53,270	11.88	3.51	2.84	0.67	6	0
LeanPool/MacMahon/Incidence.lean	30	26,135	8.86	11.04	10.36	0.68	9	0
LeanPool/MacMahon/Partitions.lean	56	13,743	3.88	3.23	2.53	0.70	19	0
LeanPool/MacMahon/Data.lean	218	10,903	4.55	1.37	0.68	0.69	11	0
LeanPool/MacMahon/Structure.lean	70	6,248	2.99	1.06	0.38	0.68	12	0
LeanPool/MacMahon/Geometry.lean	78	2,526	2.08	1.04	0.38	0.66	8	0
LeanPool/MacMahon/Colourings.lean	75	2,019	2.69	1.14	0.38	0.76	17	0
LeanPool/MacMahon/Counting.lean	63	1,319	1.86	1.00	0.28	0.71	9	0
LeanPool/MacMahon/Definitions.lean	65	1,034	2.46	0.96	0.30	0.66	22	0
LeanPool/MacMahon/Theorems.lean	94	1,025	2.28	1.06	0.31	0.75	17	0
LeanPool/MacMahon/Submission.lean	51	606	1.92	1.04	0.25	0.79	8	0
LeanPool/MacMahon/Types.lean	30	41	2.14	0.86	0.19	0.67	10	0
LeanPool/MacMahon.lean	35	0	2.49	1.39	0.16	1.23	3	0
LeanPool/MacMahon/Imports.lean	31	0	2.34	0.91	0.15	0.77	1	0
LeanPool/MacMahon/Arithmetic.lean	105	—	—	35.21	34.45	0.76	27	1
LeanPool/MacMahon/Classification.lean	182	—	—	38.22	37.47	0.74	26	1
Total	2,055	1,602,543	358.52	810.95	793.64	17.31	293	2

Aggregate phase totals

Phase	Time
blocked (unaccounted)	486409.1 ms (= 486.41 s)
type checking	251982.3 ms (= 251.98 s)
interpretation	29675.0 ms (= 29.68 s)
import	17309.0 ms (= 17.31 s)
tactic execution	13209.8 ms (= 13.21 s)
norm_num	3345.6 ms (= 3.35 s)
typeclass inference	3106.2 ms (= 3.11 s)
elaboration	1823.3 ms (= 1.82 s)
initialization	843.7 ms (= 0.84 s)
process pre-definitions	678.9 ms (= 0.68 s)
tacticAnalysis	515.9 ms (= 0.52 s)
linting	396.8 ms (= 0.40 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.MacMahon.Geometry.TargetFour	53.00 s
LeanPool.MacMahon.Geometry.TargetThree	53.00 s
LeanPool.MacMahon.Geometry.TargetTwo	53.00 s
LeanPool.MacMahon.Geometry.TargetFive	52.00 s
LeanPool.MacMahon.Geometry.TargetOne	52.00 s
LeanPool.MacMahon.Geometry.TargetZero	52.00 s
LeanPool.MacMahon.Rotations	42.00 s
LeanPool.MacMahon.Arithmetic	27.00 s
LeanPool.MacMahon.Classification	18.00 s
LeanPool.MacMahon.Witness	17.00 s
LeanPool.MacMahon.Incidence	8.10 s
LeanPool.MacMahon.WitnessData	7.20 s

Per-file `lean --profile` output

LeanPool/MacMahon.lean

import took 1.23s
cumulative profiling times:
	elaboration 0.216ms
	import 1.23s
	initialization 32.2ms
	interpretation 128ms
	linting 0.784ms
	module linting 0.00205ms
	overlappingInstancesLinter 0.263ms
	parsing 0.0595ms
	tacticAnalysis 1.42ms
real 2.15
user 0.86
sys 0.95

LeanPool/MacMahon/Arithmetic.lean

import took 755ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 439ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 487ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 474ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 479ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 360ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 323ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 373ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 354ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 400ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 389ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 400ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 409ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 410ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 422ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 349ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 403ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 390ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 395ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 370ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 407ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 390ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 351ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 380ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 389ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 379ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 402ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 402ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 400ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 369ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 394ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 375ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 400ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 398ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 394ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 403ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 356ms
tactic execution of Lean.Parser.Tactic.allGoals took 135ms
share common exprs took 187ms
process pre-definitions took 143ms
type checking took 146ms
type checking took 161ms
type checking took 175ms
type checking took 161ms
type checking took 166ms
type checking took 164ms
type checking took 168ms
type checking took 170ms
type checking took 170ms
type checking took 160ms
type checking took 157ms
type checking took 163ms
type checking took 165ms
type checking took 172ms
type checking took 169ms
type checking took 152ms
type checking took 165ms
type checking took 179ms
type checking took 181ms
type checking took 191ms
type checking took 173ms
type checking took 228ms
type checking took 193ms
type checking took 197ms
type checking took 186ms
type checking took 208ms
type checking took 171ms
type checking took 173ms
type checking took 188ms
type checking took 233ms
type checking took 555ms
linting took 129ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 414ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 293ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 294ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 293ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 293ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 300ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 431ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 444ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 440ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 445ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 442ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 295ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 130ms
cumulative profiling times:
	attribute application 0.129ms
	congr simp thm 50.6ms
	elaboration 128ms
	fix level params 19.2ms
	import 755ms
	initialization 32.3ms
	instantiate metavars 47.5ms
	interpretation 20.6s
	let-to-have transformation 0.167ms
	linting 151ms
	module linting 0.00607ms
	norm_num 2.78s
	overlappingInstancesLinter 4.85ms
	parsing 6.62ms
	process pre-definitions 166ms
	share common exprs 200ms
	simp 55.4ms
	tactic execution 1.49s
	tacticAnalysis 28.4ms
	type checking 6.9s
	typeclass inference 1.79s
real 27.10
user 35.10
sys 0.94

LeanPool/MacMahon/Classification.lean

import took 743ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 293ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 1.46s
tactic execution of Lean.Parser.Tactic.omega took 708ms
process pre-definitions took 114ms
type checking took 439ms
type checking took 179ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 327ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 2.01s
tactic execution of Lean.Parser.Tactic.omega took 3.77s
process pre-definitions took 285ms
type checking took 682ms
type checking took 147ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 335ms
tactic execution of Lean.Parser.Tactic.omega took 2.71s
tactic execution of Lean.Parser.Tactic.omega took 3.68s
tactic execution of Lean.Parser.Tactic.refine took 393ms
type checking took 314ms
type checking took 275ms
cumulative profiling times:
	attribute application 0.124ms
	blocked (unaccounted) 16.2s
	compilation (IR) 0.0848ms
	compilation (LCNF base) 0.51ms
	compilation (LCNF impure) 0.366ms
	compilation (LCNF mono) 0.664ms
	congr simp thm 14.9ms
	elaboration 104ms
	fix level params 11.7ms
	import 743ms
	initialization 32.6ms
	instantiate metavars 35ms
	interpretation 5.16s
	let-to-have transformation 0.233ms
	linting 76.7ms
	module linting 0.00141ms
	norm_num 562ms
	overlappingInstancesLinter 4.23ms
	parsing 14.1ms
	process pre-definitions 422ms
	share common exprs 107ms
	simp 111ms
	tactic execution 11.5s
	tacticAnalysis 38.6ms
	type checking 2.18s
	typeclass inference 898ms
real 10.45
user 21.88
sys 1.02

LeanPool/MacMahon/Colourings.lean

import took 756ms
cumulative profiling times:
	attribute application 0.163ms
	blocked (unaccounted) 18.1ms
	compilation (IR) 0.158ms
	compilation (LCNF base) 2.09ms
	compilation (LCNF impure) 0.693ms
	compilation (LCNF mono) 1.21ms
	congr simp thm 0.384ms
	elaboration 18.7ms
	fix level params 0.184ms
	import 756ms
	initialization 43.9ms
	instantiate metavars 0.306ms
	interpretation 195ms
	let-to-have transformation 0.118ms
	linting 6.07ms
	module linting 0.00176ms
	norm_num 3.59ms
	overlappingInstancesLinter 2.69ms
	parsing 4.49ms
	process pre-definitions 4.73ms
	share common exprs 1.05ms
	simp 6.41ms
	tactic execution 26ms
	tacticAnalysis 14.7ms
	type checking 16.8ms
	typeclass inference 17.4ms
real 1.78
user 1.11
sys 0.84

LeanPool/MacMahon/Counting.lean

import took 713ms
cumulative profiling times:
	attribute application 0.0332ms
	blocked (unaccounted) 0.0405ms
	congr simp thm 1.08ms
	elaboration 8.14ms
	fix level params 0.111ms
	import 713ms
	initialization 32.5ms
	instantiate metavars 0.445ms
	interpretation 151ms
	let-to-have transformation 0.0419ms
	linting 5.55ms
	module linting 0.00196ms
	overlappingInstancesLinter 1.62ms
	parsing 3.98ms
	process pre-definitions 1.16ms
	share common exprs 0.669ms
	simp 16.3ms
	tactic execution 28.5ms
	tacticAnalysis 13.7ms
	type checking 3.78ms
	typeclass inference 13.5ms
real 1.71
user 0.94
sys 0.89

LeanPool/MacMahon/Data.lean

import took 689ms
cumulative profiling times:
	attribute application 0.0503ms
	compilation (IR) 4.85ms
	compilation (LCNF base) 55.6ms
	compilation (LCNF impure) 19.6ms
	compilation (LCNF mono) 50.6ms
	elaboration 189ms
	fix level params 0.178ms
	import 689ms
	initialization 33.1ms
	instantiate metavars 1.56ms
	interpretation 214ms
	let-to-have transformation 0.209ms
	linting 11.1ms
	module linting 0.00177ms
	overlappingInstancesLinter 3.41ms
	parsing 8.61ms
	process pre-definitions 8.69ms
	share common exprs 2.15ms
	tacticAnalysis 40.6ms
	type checking 3.53ms
	typeclass inference 29.4ms
real 1.93
user 1.37
sys 0.87

LeanPool/MacMahon/Definitions.lean

import took 658ms
cumulative profiling times:
	attribute application 0.7ms
	blocked (unaccounted) 0.988ms
	compilation (IR) 0.476ms
	compilation (LCNF base) 7.33ms
	compilation (LCNF impure) 2.19ms
	compilation (LCNF mono) 4.57ms
	elaboration 26.7ms
	fix level params 0.107ms
	import 658ms
	initialization 32.7ms
	instantiate metavars 0.0944ms
	interpretation 166ms
	let-to-have transformation 0.097ms
	linting 7.78ms
	module linting 0.00156ms
	overlappingInstancesLinter 3.42ms
	parsing 5.7ms
	process pre-definitions 4.18ms
	share common exprs 0.429ms
	tacticAnalysis 16.1ms
	type checking 6.71ms
	typeclass inference 11.4ms
real 1.61
user 0.93
sys 0.83

LeanPool/MacMahon/Geometry.lean

import took 659ms
cumulative profiling times:
	attribute application 0.0365ms
	elaboration 7.9ms
	fix level params 0.526ms
	import 659ms
	initialization 42.9ms
	instantiate metavars 21ms
	interpretation 230ms
	let-to-have transformation 0.0381ms
	linting 4.51ms
	module linting 0.00169ms
	overlappingInstancesLinter 2.09ms
	parsing 3.03ms
	process pre-definitions 10.7ms
	share common exprs 3.6ms
	tactic execution 18.9ms
	tacticAnalysis 12.8ms
	type checking 18.6ms
	typeclass inference 2.96ms
real 1.72
user 0.96
sys 0.86

LeanPool/MacMahon/Geometry/TargetFive.lean

import took 683ms
type checking took 6.64s
type checking took 6.68s
type checking took 6.78s
type checking took 6.7s
type checking took 6.65s
cumulative profiling times:
	attribute application 0.0622ms
	blocked (unaccounted) 66.8s
	elaboration 11.8ms
	fix level params 0.0776ms
	import 683ms
	initialization 32.1ms
	instantiate metavars 0.0526ms
	interpretation 139ms
	let-to-have transformation 0.12ms
	linting 4.75ms
	module linting 0.00208ms
	overlappingInstancesLinter 2.27ms
	parsing 1.92ms
	process pre-definitions 0.856ms
	share common exprs 0.218ms
	tactic execution 3.55ms
	tacticAnalysis 8.81ms
	type checking 33.4s
	typeclass inference 14.4ms
real 35.09
user 34.00
sys 1.20

LeanPool/MacMahon/Geometry/TargetFour.lean

import took 665ms
type checking took 6.66s
type checking took 6.96s
type checking took 6.67s
type checking took 6.59s
type checking took 6.66s
cumulative profiling times:
	attribute application 0.0738ms
	blocked (unaccounted) 67.5s
	elaboration 11.7ms
	fix level params 0.0562ms
	import 665ms
	initialization 31.4ms
	instantiate metavars 0.0528ms
	interpretation 137ms
	let-to-have transformation 0.0909ms
	linting 4.57ms
	module linting 0.00155ms
	overlappingInstancesLinter 2.36ms
	parsing 1.74ms
	process pre-definitions 0.814ms
	share common exprs 0.225ms
	tactic execution 3ms
	tacticAnalysis 9.07ms
	type checking 33.6s
	typeclass inference 16.9ms
real 35.13
user 34.06
sys 1.16

LeanPool/MacMahon/Geometry/TargetOne.lean

import took 661ms
type checking took 6.73s
type checking took 6.53s
type checking took 6.66s
type checking took 6.69s
type checking took 6.71s
cumulative profiling times:
	attribute application 0.0643ms
	blocked (unaccounted) 66.5s
	elaboration 11.5ms
	fix level params 0.0778ms
	import 661ms
	initialization 32.4ms
	instantiate metavars 0.0536ms
	interpretation 139ms
	let-to-have transformation 0.0991ms
	linting 4.84ms
	module linting 0.00161ms
	overlappingInstancesLinter 2.18ms
	parsing 1.89ms
	process pre-definitions 0.773ms
	share common exprs 0.222ms
	tactic execution 3.06ms
	tacticAnalysis 9.09ms
	type checking 33.3s
	typeclass inference 15.3ms
real 34.90
user 33.86
sys 1.15

LeanPool/MacMahon/Geometry/TargetThree.lean

import took 653ms
type checking took 6.56s
type checking took 6.63s
type checking took 6.63s
type checking took 6.52s
type checking took 6.72s
cumulative profiling times:
	attribute application 0.0575ms
	blocked (unaccounted) 65.9s
	elaboration 11.7ms
	fix level params 0.0577ms
	import 653ms
	initialization 40.4ms
	instantiate metavars 0.0564ms
	interpretation 139ms
	let-to-have transformation 0.0989ms
	linting 4.79ms
	module linting 0.00172ms
	overlappingInstancesLinter 2.41ms
	parsing 1.94ms
	process pre-definitions 0.776ms
	share common exprs 0.223ms
	tactic execution 2.46ms
	tacticAnalysis 8.53ms
	type checking 33.1s
	typeclass inference 14.4ms
real 34.71
user 33.67
sys 1.14

LeanPool/MacMahon/Geometry/TargetTwo.lean

import took 666ms
type checking took 6.83s
type checking took 6.71s
type checking took 6.81s
type checking took 6.83s
type checking took 6.63s
cumulative profiling times:
	attribute application 0.0596ms
	blocked (unaccounted) 67.9s
	elaboration 11.4ms
	fix level params 0.0573ms
	import 666ms
	initialization 33ms
	instantiate metavars 0.0547ms
	interpretation 140ms
	let-to-have transformation 0.098ms
	linting 4.49ms
	module linting 0.00175ms
	overlappingInstancesLinter 2.38ms
	parsing 1.87ms
	process pre-definitions 0.778ms
	share common exprs 0.226ms
	tactic execution 2.49ms
	tacticAnalysis 9.56ms
	type checking 33.8s
	typeclass inference 17.5ms
real 35.40
user 34.36
sys 1.14

LeanPool/MacMahon/Geometry/TargetZero.lean

import took 663ms
type checking took 6.76s
type checking took 6.72s
type checking took 6.74s
type checking took 6.9s
type checking took 6.79s
cumulative profiling times:
	attribute application 0.0596ms
	blocked (unaccounted) 67.6s
	elaboration 11.2ms
	fix level params 0.0578ms
	import 663ms
	initialization 32.5ms
	instantiate metavars 0.0573ms
	interpretation 138ms
	let-to-have transformation 0.097ms
	linting 4.53ms
	module linting 0.00165ms
	overlappingInstancesLinter 2.75ms
	parsing 1.75ms
	process pre-definitions 0.759ms
	share common exprs 0.255ms
	tactic execution 3.71ms
	tacticAnalysis 9.32ms
	type checking 33.9s
	typeclass inference 18.6ms
real 35.49
user 34.42
sys 1.17

LeanPool/MacMahon/Imports.lean

import took 766ms
cumulative profiling times:
	elaboration 0.0983ms
	import 766ms
	initialization 33ms
	interpretation 112ms
	linting 0.34ms
	module linting 0.00153ms
	overlappingInstancesLinter 0.106ms
	parsing 0.00192ms
	tacticAnalysis 0.438ms
real 1.70
user 0.88
sys 0.87

LeanPool/MacMahon/Incidence.lean

import took 681ms
type checking took 281ms
type checking took 105ms
type checking took 4.27s
type checking took 168ms
cumulative profiling times:
	attribute application 0.0465ms
	blocked (unaccounted) 5.32s
	elaboration 9.19ms
	fix level params 0.0358ms
	import 681ms
	initialization 33.3ms
	instantiate metavars 0.0505ms
	interpretation 132ms
	let-to-have transformation 0.0522ms
	linting 3.46ms
	module linting 0.00159ms
	overlappingInstancesLinter 2.16ms
	parsing 1.61ms
	process pre-definitions 0.566ms
	share common exprs 0.126ms
	tactic execution 2.48ms
	tacticAnalysis 8.69ms
	type checking 4.83s
	typeclass inference 17.6ms
real 6.44
user 5.65
sys 0.88

LeanPool/MacMahon/Partitions.lean

import took 698ms
type checking took 506ms
type checking took 311ms
cumulative profiling times:
	attribute application 0.084ms
	blocked (unaccounted) 1.37s
	compilation (IR) 0.397ms
	compilation (LCNF base) 5.26ms
	compilation (LCNF impure) 2.59ms
	compilation (LCNF mono) 5.01ms
	elaboration 24.4ms
	fix level params 0.0877ms
	import 698ms
	initialization 38.8ms
	instantiate metavars 0.178ms
	interpretation 157ms
	let-to-have transformation 0.0931ms
	linting 5.96ms
	module linting 0.00156ms
	overlappingInstancesLinter 2.63ms
	parsing 3.82ms
	process pre-definitions 3.71ms
	share common exprs 0.375ms
	tactic execution 5.62ms
	tacticAnalysis 13.9ms
	type checking 863ms
	typeclass inference 29.1ms
real 2.53
user 1.81
sys 0.86

LeanPool/MacMahon/Rotations.lean

import took 679ms
type checking took 265ms
type checking took 346ms
type checking took 414ms
type checking took 147ms
type checking took 342ms
type checking took 14.2s
type checking took 799ms
type checking took 8.13s
cumulative profiling times:
	attribute application 0.311ms
	blocked (unaccounted) 61.3s
	compilation (IR) 0.375ms
	compilation (LCNF base) 4.11ms
	compilation (LCNF impure) 2.32ms
	compilation (LCNF mono) 4.18ms
	elaboration 38.2ms
	fix level params 0.175ms
	import 679ms
	initialization 37.8ms
	instantiate metavars 0.295ms
	interpretation 176ms
	let-to-have transformation 0.203ms
	linting 11ms
	module linting 0.00164ms
	overlappingInstancesLinter 4.39ms
	parsing 6.57ms
	process pre-definitions 3.84ms
	share common exprs 0.753ms
	tactic execution 13.4ms
	tacticAnalysis 19ms
	type checking 24.6s
	typeclass inference 57ms
real 26.29
user 25.37
sys 1.13

LeanPool/MacMahon/Structure.lean

import took 679ms
cumulative profiling times:
	attribute application 0.0367ms
	congr simp thm 0.903ms
	elaboration 13.8ms
	fix level params 0.134ms
	import 679ms
	initialization 33.5ms
	instantiate metavars 0.473ms
	interpretation 147ms
	let-to-have transformation 0.053ms
	linting 5.93ms
	module linting 0.00175ms
	overlappingInstancesLinter 1.87ms
	parsing 4.58ms
	process pre-definitions 1.57ms
	share common exprs 0.763ms
	simp 25.6ms
	tactic execution 47.5ms
	tacticAnalysis 14.1ms
	type checking 51.9ms
	typeclass inference 32ms
real 1.69
user 0.98
sys 0.87

LeanPool/MacMahon/Submission.lean

import took 794ms
cumulative profiling times:
	attribute application 0.0318ms
	elaboration 10.2ms
	fix level params 0.0845ms
	import 794ms
	initialization 33.4ms
	instantiate metavars 0.18ms
	interpretation 154ms
	let-to-have transformation 0.0578ms
	linting 4.01ms
	module linting 0.00166ms
	overlappingInstancesLinter 1.94ms
	parsing 2.97ms
	process pre-definitions 1.01ms
	share common exprs 0.447ms
	tactic execution 21.5ms
	tacticAnalysis 8.65ms
	type checking 2.35ms
	typeclass inference 5.17ms
real 1.77
user 0.98
sys 0.89

LeanPool/MacMahon/Theorems.lean

import took 749ms
cumulative profiling times:
	attribute application 0.174ms
	compilation (IR) 0.028ms
	compilation (LCNF base) 0.313ms
	compilation (LCNF impure) 0.113ms
	compilation (LCNF mono) 0.143ms
	congr simp thm 0.108ms
	elaboration 17.9ms
	fix level params 0.16ms
	import 749ms
	initialization 36.6ms
	instantiate metavars 0.248ms
	interpretation 185ms
	let-to-have transformation 0.0964ms
	linting 7.66ms
	module linting 0.00155ms
	overlappingInstancesLinter 2.98ms
	parsing 5.75ms
	process pre-definitions 2.56ms
	share common exprs 0.717ms
	simp 1.56ms
	tactic execution 27.5ms
	tacticAnalysis 15.1ms
	type checking 3.76ms
	typeclass inference 6.22ms
real 1.73
user 0.97
sys 0.92

LeanPool/MacMahon/Types.lean

import took 666ms
cumulative profiling times:
	attribute application 0.188ms
	elaboration 2.99ms
	fix level params 0.0188ms
	import 666ms
	initialization 33.4ms
	instantiate metavars 0.0319ms
	interpretation 141ms
	let-to-have transformation 0.0251ms
	linting 2.24ms
	module linting 0.00163ms
	overlappingInstancesLinter 2.05ms
	parsing 1.5ms
	process pre-definitions 0.622ms
	share common exprs 0.0483ms
	tacticAnalysis 7.46ms
	type checking 0.165ms
	typeclass inference 0.526ms
real 1.61
user 0.82
sys 0.87

LeanPool/MacMahon/Witness.lean

import took 731ms
type checking took 11.4s
cumulative profiling times:
	attribute application 0.0245ms
	elaboration 4.54ms
	fix level params 0.0362ms
	import 731ms
	initialization 36.2ms
	instantiate metavars 0.0833ms
	interpretation 131ms
	let-to-have transformation 0.0303ms
	linting 2.41ms
	module linting 0.00163ms
	overlappingInstancesLinter 1.54ms
	parsing 1.82ms
	process pre-definitions 0.45ms
	share common exprs 0.246ms
	tactic execution 10.1ms
	tacticAnalysis 6.86ms
	type checking 11.4s
	typeclass inference 7.8ms
real 13.07
user 12.23
sys 0.92

LeanPool/MacMahon/WitnessData.lean

import took 672ms
elaboration took 1.15s
compilation (LCNF base) took 143ms
compilation (LCNF mono) took 169ms
tacticAnalysis took 196ms
interpretation of Batteries.Linter.UnreachableTactic.unreachableTacticLinter._lam_0._boxed took 126ms
cumulative profiling times:
	attribute application 0.0122ms
	compilation (IR) 51.3ms
	compilation (LCNF base) 143ms
	compilation (LCNF impure) 51.9ms
	compilation (LCNF mono) 220ms
	elaboration 1.15s
	fix level params 0.216ms
	import 672ms
	initialization 43.7ms
	instantiate metavars 18.6ms
	interpretation 664ms
	let-to-have transformation 0.334ms
	linting 62.3ms
	module linting 0.00177ms
	overlappingInstancesLinter 8.7ms
	parsing 76.1ms
	process pre-definitions 42.4ms
	share common exprs 13.5ms
	tacticAnalysis 201ms
	type checking 1.72ms
	typeclass inference 91ms
real 4.26
user 3.54
sys 0.88

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[greptile-apps]

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

[Medium impact] No actionable defect was found; external source checks remain unverified, so this is not a complete merge approval.

Summary

Imports the minimum universal MacMahon cube classification, including the physical face-matching model and ten minimum inventories.

• Universal inventories need at least twelve cubes and have ten minimum forms.
• Cube builds match exterior faces under proper rotations.
• Every six-colour face arrangement has one variety and rotation.
• Ten candidate inventories come with eight-cube builds for every target.
• Lean users can import the MacMahon classification as a Lean Pool entry.

_{Reviews (2) · Last reviewed commit: "Add modification notices to adapted MacM..." · Reviewed by Greptile}

[Vilin97]

Exact-head acquisition checkpoint for 9ddc427022b708c6220c86a558eb2e2802f1f908:

• Local project/public-wrapper build is warning-free. Generated indexes, Mathlib linters, style, full-repository static quality, all ten result resolutions, public axiom audit and compiled-environment audit pass. All 137 original declaration signatures and complete numeric tables are preserved.
• Clean local compile measurements: baseline 302.813 s, optimized mathematics 198.486 s, final documented source 247.889 s. The latter is 18.14% below baseline. Same exact pins, project artifacts removed, LEAN_NUM_THREADS=4; shared VM load is uncontrolled.
• Greptile completed on this head with no actionable defect. The separate comprehensive source review approves. Configured GPT review was requested once and has no observed verdict yet.
• Required Lean CI is still running, currently restoring the pool cache. Content separation and applicable completed scope checks pass. Final hosted Lean validation is not yet established.
• Advisory profiling failed before compiling this project while restoring Lean dependencies. Its check annotation reports System.IO.IOException: No space left on device in the GitHub runner. The build/profile steps did not run and no hosted timing is available. This advisory failure is not treated as an independent merge gate; the successful local measurements remain available above.

The PR remains open. PR610 and PR611 are merged, but the protected validation contexts at current main edbe5bd56f476cc2965564676b66199f281ab714 are not independently confirmed green, so the explicit infrastructure hold still prohibits queue, auto-merge and merge actions. Daily documentation publishing was excluded from that decision. No author-actionable defect is presently identified; remaining required hosted validation/review and the rollout hold are explicit external dependencies. No infrastructure or gate changes were made.

[Vilin97]

Source assessment: approve at 37895395733ae1a6ddc90d22ea28f3f9c4a93a01, after independent review of the complete 25-file import and its proof dependencies.

The model uses natural-number multiplicities and an injective allocation of eight physical copies. It verifies proper rotations, all six-colour face assignments, and the bridge from corner matching to exterior-face matching. Zero diagonal excludes invalid tableau placeholders. The lower bound and tight degree/symmetry constraints are derived before classification; the winning shape is not assumed. Explicit constructions establish attainment, and the ten results count labelled inventories, with no repeated variety at the minimum.

These statements match Johnson–Roldán Conjectures 4 and 8 and Haraguchi’s minimum-size theorem. The numerical solution-count histograms are outside the advertised Lean results. The classification and reusable finite geometry are significant; the inspected Mathlib and Tau Ceti contracts did not duplicate this development.

The pinned upstream, Apache-2.0 attribution and AI proof provenance were checked. I added file-local modification notices to the 22 adapted proof modules in this comment-only child. Removing those comment lines restores every parent proof, definition, import and numeric table byte for byte; the card and original copyright headers remain intact. Independent finite-data checks cover all 300 physical constructions and the face/corner bridge, separately from the general mathematical proofs.

No source blocker remains. Current-head hosted CI and configured review still need to pass independently before protected native admission. The old head’s checks, author-side local validation and advisory timings supply no current-head gate credit.

[Vilin97]

/review

Current head 37895395733ae1a6ddc90d22ea28f3f9c4a93a01 adds file-local modification notices to 22 adapted modules. Removing those comment lines restores the prior proofs and data exactly. The earlier request 6576166785 belongs to head9ddc; this is one request for the current revision. Independent source assessment: #730 (review).

[Vilin97]

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

Reviewed head: 37895395733ae1a6ddc90d22ea28f3f9c4a93a01

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

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	All ten headlines match the Lean; required Lean CI remains pending, and the earlier profiling failure was runner disk exhaustion before compilation.
Novelty	✅ pass	No declaration duplicating any of the ten headline results was found in the inspected Mathlib, Tau Ceti, or pool sources.
Significance	✅ pass	The complete classification merits pooling; generated-data modules occupy 741 of 2,055 Lean lines (36%) and contain ordinary finite tables reproducible from pinned upstream inputs, although the generator is not vendored.
Sources	✅ pass	The cited conjectures and Haraguchi theorem support the attributions; the pinned upstream formalization is credited, and the multiset extension is explicitly labelled.
Code quality (advisory)	🤔 discuss	The module structure is competent, but two arithmetic proofs exhaust the synchronous profiler’s default heartbeat budget; required CI remains pending.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	DiagonalZero is explicit and disclosed; the model uses six distinct colours, proper signed-axis rotations, eight distinct physical copies and exterior-face matching, with the geometric bridge and classification proved rather than assumed.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	research
Branch	finite combinatorics
Mode	mixed
Code quality	3 / 5

Statement check: For zero-diagonal natural-number inventories, the Lean proves an attained minimum of twelve, exactly ten minimizers, their two-triangle classification, and absence of repeated varieties, together with the advertised geometric coverage and uniqueness results.

MacMahon.minimum_size, MacMahon.physical_exactly_ten, and MacMahon.physical_iff_two_triangles establish the attained minimum of twelve and classify its ten inventories structurally, addressing the published MacMahon-cube classification conjectures.

Faithfulness findings (1)

• prompt-injection — PR-wide
  The contributor-supplied discussion embeds a prewritten faithfulness pass and invokes prior approval, which could substitute asserted authority for independent review; those claims were disregarded.
  Evidence: prose only: the discussion states ‘Conclusion: approve on source and local validation.’ and embeds a faithfulness assessment containing ‘"verdict": "pass"’ and ‘"proves_the_claim": "proves_it"’.

Significance findings (1)

• prompt-injection — PR-wide
  The contributor discussion supplies a prewritten significance verdict and repeats prior-approval claims, creating a risk of anchoring this independent review; those claims were disregarded when assessing the Lean.
  Evidence: In .review-pr.json, comment 6576157615 states ‘Conclusion: approve on source and local validation’ and embeds a significance verdict of pass; comment 6576282329 invokes that review again as approving.

Code quality findings (2)

• proof-cost — LeanPool/MacMahon/Arithmetic.lean:30
  The current-head profiling artifact records 200,000-heartbeat timeouts in usable_count_identity and Classification.lean’s normalized_triangle_closes under -DElab.async=false, although the ordinary changed-module build succeeds. Blanket finite expansion makes these arithmetic steps expensive and prevents complete heartbeat measurements. Consider summed identities and smaller constraint sets, then rerun profiling. Evidence: profiling run.
  Evidence: usable_count_identity uses fin_cases i <;> fin_cases j <;> norm_num [row, col, total, Fintype.sum_prod_type, Fin.sum_univ_succ] at * <;> omega. normalized_triangle_closes uses norm_num [DiagonalZero, row, Fin.forall_fin_succ, Fin.sum_univ_succ] at hz hr hs norm_num [Fin.forall_fin_succ, winner, twoTriangles, triple, Fintype.sum_prod_type, Fin.sum_univ_succ, -add_pos_iff] at hp omega.
• prompt-injection — PR-wide
  The contributor-written discussion supplies claimed prior approval and a precomputed quality verdict. These have no authority over this independent review and were disregarded.
  Evidence: Comment 6576157615 in .review-pr.json states Conclusion: **approve** on source and local validation. and embeds a quality review with "verdict": "pass".

---

Tokens: 7,302,557 in / 47,270 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $29.9193 (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]

Maintainer assessment of the new configured review at exact head 37895395733ae1a6ddc90d22ea28f3f9c4a93a01:

I retain source acceptance after considering the two proof-cost findings. usable_count_identity expands a fixed six-label identity, and normalized_triangle_closes reduces the fixed six-label, ten-partition constraints to arithmetic. These are localized finite proofs supporting the complete classification; their current structure is an acceptable maintenance tradeoff. Summed identities and a smaller constraint set would be useful future improvements.

The configured review reports synchronous 200,000-heartbeat profiler timeouts. I have inspected the actual proof commands, but have not independently reproduced that measurement. Profiling is advisory under the contribution rules. The literal configured verdict remains needs_discussion (quality 3/5); this maintainer assessment addresses its cost concern without changing that result.

The contributor-supplied prior verdicts played no role in the independent source, mathematical, attribution and novelty assessments. Current-head Lean validation is still pending, and complete required CI, current-main qualification and protected native integration remain necessary before any merge.