Skip to content

Import order-closure and weak Fatou formalization - #536

Open
Vilin97 wants to merge 8 commits into
mainfrom
codex/daily-order-closures-20260926
Open

Import order-closure and weak Fatou formalization#536
Vilin97 wants to merge 8 commits into
mainfrom
codex/daily-order-closures-20260926

Conversation

@Vilin97

@Vilin97 Vilin97 commented Sep 26, 2026 •
edited
Loading

Copy link
Copy Markdown
Owner

This imports the completed formalization accompanying Order closure, order adherence and Fatou norms by Antonio Avilés, Mitchell A. Taylor, and Pedro Tradacete. It preserves a complete weakly Fatou lattice norm (constant 2) that admits no equivalent Fatou lattice norm, arbitrarily long solid order-adherence towers, and the Gao–Leung characterization for sigma-order-complete Banach lattices.

The source is pedrotradacete/OrderClosures at 6189ba7134f6975e7d8e4c8c093a9869d03a769c, licensed Apache-2.0. The completion commit is dated 2026-08-26 18:19:54 UTC; the public paper was submitted 2026-09-06 15:59:03 UTC. Both are in this acquisition's eligible interval [2026-07-26 03:14:40, 2026-09-19 03:14:40) UTC. The later repository metadata update is not used as completion evidence. Registry, directory, history, issues, and open/merged PR checks found no duplicate.

The 37-module scope retains all 17 paper modules and 20 prerequisite modules extracted from David Muñoz-Lahoz's Apache-2.0 BanLat at b00e59836016aa1099b8011add6b07385e66428e. This supplies reusable vector lattices, order-convergent nets, ideals/bands, positive operators, lattice homomorphisms, seminorms, completions, and the proof-producing llarith tactic. The research construction supplies Boolean/Stone and transfinite-iteration infrastructure. Unused operator, projection-band, locally-solid representation, and finite PiLp developments are omitted; the seminorm interface and pointwise-product instance remain.

Provenance is recorded as AI, with the evidence and inference disclosed in the entry module: BanLat says that language models wrote much of the implementation under human direction; OrderClosures records phase-specific agent instructions and a phase-II proof pass. No particular model or precise fraction is asserted. Credits to Jaume de Dios Pont for earlier Section 3 formalization, and Michael Elliott/Anthony Wickstead for the previously announced weak Fatou result, are retained. Codex performed this port and cleanup.

The metadata follows the Lean statements exactly. In particular, gao_counterexample is the order-complete C(K) construction with large density and a closed separable sublattice whose only order-closed extension is the whole space; it does not itself assert the negation of GaoLeungProperty. The iteration theorem requires an infinite cardinal, bounds the ordinal by its successor cardinal's initial ordinal, and lifts the witness one universe. The Fatou endpoint uses explicit lattice norms and sequential metric completeness.

Ported to Lean 4.34.0 and Mathlib 5ed2965256430c3649e86755f9576b54eca72435. Changes include module/public exports, current coercion and conditional APIs, TFAE indexing, typeclass coherence for sublattices, explicit proofs where stronger transparency exposed old simplification assumptions, removal of unused hypotheses, and documentation repairs. Four recursive tactic helpers are total: quotation uses the expression's structural size as its recursion bound. Three long proofs were split into CNF, projection, positive-budget, and thinned-majorant helpers. No theorem was weakened and no check, option override, suppression, or waiver was added.

Measured optimization used /usr/bin/time -v lake build LeanPool.OrderClosures, deleting only this project's .lake/build/{lib/lean,ir}/LeanPool/OrderClosures* artifacts before each run. Same Azure VM, toolchain, pinned dependencies, default Lake concurrency, warm Mathlib oleans/configuration/file cache; no simultaneous task-specific compilation in the reported controlled pairs. Shared-host timing variation remains possible.

Baseline (48 modules) Optimized (37 modules)
Clean wall-clock runs 69.98 / 71.73 s 38.04 / 39.10 s
Mean wall clock 70.86 s 38.57 s (45.6% lower)
User CPU 201.71 / 207.89 s 139.53 / 140.96 s

Profiling identified ambiguous expected-type inference in completion, ideal intersections, and convergence proofs. Explicit type/function arguments removed that repeated elaboration. Blanket tactic imports were replaced with direct dependencies; the dependency graph shrank from 3231 to 2587 Lake jobs. The initial baseline source and per-file/Lean profiler logs are retained. The first optimized run was 38.60 s but is excluded from the controlled pair because the audit was finishing concurrently. No heartbeat override was retained. These timings were measured at 1708a9a31 and include the Greptile-requested 11 kernel-checked tactic examples; the preceding optimized commit measured 37.51 / 34.81 s. They precede the later goal-focus repair and two additional examples at 0e45643c. No comparable project-clean timing of that later head is claimed; its focused module validation and CI passed.

Local validation: warning-free project build; generated indexes; Mathlib's 15 linters; style; all standard quality checks in a source-identical 37-module audit checkout, with its own compiled root and empty challenge/solution libraries; axiom audit over 798 parsed declarations; compiled-environment option/axiom/backdoor audit including private/generated declarations. Only Classical.choice, propext, and Quot.sound are permitted. No Python source changed. Whole-pool CI and configured Greptile/GPT reviews remain the final integration/review authority.

Greptile's initial two findings were repaired in 1708a9a: ambient-norm reductions now reuse the general paper-norm proofs; 11 tactic examples cover equality, inequalities, scalar multiplication, all four sign forms, mixed signs, positive/negative parts, and reflexivity. The mixed-sign test exposed and drove a fix to proof transfer, including state restoration before fallback. Both review threads are resolved.

The separate thorough agentic review covers every imported file in bounded packets, all four endpoint definitions and quantifiers, the full semantic port/refactor diff, dependency closure, representative implementations, and all five repository review axes. It finds the mathematics and repaired implementation suitable, but requests changes before automatic merge: the main upstream's AI versus mix proof-authorship classification needs conclusive first-party evidence. The entry module already discloses the current classification as an inference; factual confirmation remains external.

At repaired head 0e45643ca8923ea5249d4de936e8219983c082b1, Lean Action CI passed the build, index, challenge/solution, linter, style and quality checks. The logs show fresh lint, declaration, axiom and backdoor validation for OrderClosures; unchanged projects can use the configured validation cache. All three required checks are green. The branch is currently behind main, so strict base freshness would also need restoration before merge.

The configured GPT review requested changes on earlier head f0d23ffff. Its findings were repaired in 0e45643c: the card, entry exposition and counterexample docstring now describe the exact order-closed-extension property and cite Proposition 2.1; evalLlarith focuses its main goal and two additional regressions check preservation of sibling goals. The thirteen tactic examples pass. Greptile reviewed the repaired head with no outstanding finding. No GPT verdict for the repaired head is published yet.

The resumed thorough review preserves the completed full-source review, covers the entire later source/card delta and current CI evidence, and retains request_changes solely for the unresolved upstream proof-provenance classification. The public upstream commit history, README, formalization guide, paper and current issue/release metadata do not conclusively establish AI versus mix. Required credit and inference disclosure are already present. The PR remains open with auto-merge disabled; no duplicate import or review request was created.

@greptile-apps

greptile-apps Bot commented Sep 26, 2026 •
edited
Loading

Copy link
Copy Markdown

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

Retrigger

[Low risk] Adds formalized mathematics library for order closures and Fatou norms.

No new issue or outstanding Greptile finding was identified, but the externally unresolved proof-provenance classification should be settled before describing the contribution as fully verified.

Summary

Imports the OrderClosures formalization and its BanLat prerequisites, registers its four headline results, and exposes the modules through the aggregate library.

  • The changes since the previous review merge main; they do not modify the OrderClosures source or catalog entry.
  • The current code retains the repairs to both earlier Greptile findings.
  • The upstream AI-versus-mix proof-authorship classification remains an externally unverified aspect of the contribution, not a new finding from this review.

Reviews (7) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..."

greptile-apps[bot]
greptile-apps Bot reviewed Sep 26, 2026
View reviewed changes
Comment thread LeanPool/OrderClosures/WeaklyFatou/Reductions.lean
Comment thread LeanPool/OrderClosures/BanLat/Tactic/LLexpr.lean
@github-actions

github-actions Bot commented Sep 26, 2026

Copy link
Copy Markdown
Contributor

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 99.85 s (= 1.66 min) — user 265.72 s, sys 24.83 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: 66,104 maxHeartbeats units across 37 files (18,723 added LOC).

Sum of lean --profile: 197176.2 ms (= 197.18 s). Import-excluded time: 156865.2 ms (= 156.87 s).

Count-heartbeats wall-clock total: 231.72 s. Repeated import cost inside lean --profile: 40311.0 ms (= 40.31 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units. 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) Decls Errors
LeanPool/OrderClosures/GaoLeungProblem/Iterations.lean 760 15,433 13.44 9.96 8.82 1.14 36 0
LeanPool/OrderClosures/BanLat/Substructures/Ideal.lean 1,127 13,522 11.09 10.34 9.27 1.07 78 0
LeanPool/OrderClosures/BanLat/Operators/Positive.lean 343 7,784 7.34 5.67 4.66 1.01 19 0
LeanPool/OrderClosures/BanLat/Operators/Hom.lean 606 6,947 8.97 6.69 5.60 1.09 45 0
LeanPool/OrderClosures/BanLat/Substructures/Sublattice.lean 935 5,869 8.63 7.02 5.96 1.06 51 0
LeanPool/OrderClosures/BanLat/Normed.lean 404 2,214 5.05 3.53 2.51 1.02 35 0
LeanPool/OrderClosures/BanLat/Disjoint.lean 632 2,074 5.10 5.85 4.85 1.00 36 0
LeanPool/OrderClosures/OrderAdherence.lean 454 1,989 8.03 9.45 8.37 1.08 29 0
LeanPool/OrderClosures/BanLat/Basic.lean 589 1,477 5.46 6.47 5.58 0.89 30 0
LeanPool/OrderClosures/BanLat/OrderContinuous/MeyerNieberg.lean 909 1,069 7.83 12.04 11.02 1.02 11 0
LeanPool/OrderClosures/BanLat/Substructures/Band/Basic.lean 218 1,040 3.35 1.97 0.91 1.06 12 0
LeanPool/OrderClosures/GaoLeungCharacterization.lean 1,039 1,010 16.25 17.44 16.38 1.06 22 0
LeanPool/OrderClosures/BanLat/Convergences/Order.lean 367 828 3.53 3.57 2.69 0.88 18 0
LeanPool/OrderClosures/BanLat/LLexpr.lean 511 777 5.46 5.29 4.24 1.05 53 0
LeanPool/OrderClosures/WeaklyFatou/Reductions.lean 466 682 4.84 4.16 3.08 1.08 11 0
LeanPool/OrderClosures/Solovay.lean 1,660 628 8.07 11.17 10.03 1.14 98 0
LeanPool/OrderClosures/BanLat/OrderContinuous/Basic.lean 354 573 5.40 3.36 2.32 1.04 9 0
LeanPool/OrderClosures/BanLat/OrderContinuous/Nakano.lean 226 398 6.14 2.76 1.75 1.01 6 0
LeanPool/OrderClosures/BanLat/OrderUnit.lean 68 246 3.75 1.61 0.60 1.01 4 0
LeanPool/OrderClosures/BanLat/Substructures/Band/DisjointComplement.lean 150 246 3.16 1.95 0.88 1.07 3 0
LeanPool/OrderClosures/BanLat/LatticeSeminorm.lean 57 187 3.34 1.42 0.43 0.99 4 0
LeanPool/OrderClosures/WeaklyFatou/TreeNorm.lean 690 184 3.86 7.20 6.12 1.08 46 0
LeanPool/OrderClosures/GaoLeungProblem/CNFOrder.lean 736 130 4.98 3.86 2.69 1.17 28 0
LeanPool/OrderClosures/WeaklyFatou/Bands.lean 681 128 6.08 4.73 3.64 1.09 32 0
LeanPool/OrderClosures/BanLat/Tactic/LLexpr.lean 504 116 8.40 4.68 3.64 1.04 26 0
LeanPool/OrderClosures/WeaklyFatou/FiniteTree.lean 453 108 4.79 3.22 2.15 1.07 27 0
LeanPool/OrderClosures/WeaklyFatou/FinalSpace.lean 599 96 12.09 10.55 9.47 1.08 24 0
LeanPool/OrderClosures/GaoLeungProblem/OrdinalSpace.lean 905 79 5.52 4.29 3.14 1.15 19 0
LeanPool/OrderClosures/GaoLeungProblem/StageFormula.lean 715 68 6.13 5.27 4.13 1.14 17 0
LeanPool/OrderClosures/BanLat/Pi.lean 34 67 2.81 1.30 0.29 1.01 1 0
LeanPool/OrderClosures/BanLat/OrderComplete.lean 379 51 4.59 2.39 1.50 0.89 12 0
LeanPool/OrderClosures/GaoLeungProblem/Counterexample.lean 526 36 6.78 5.30 4.15 1.15 9 0
LeanPool/OrderClosures/BanLat/Examples/CofK/Basic.lean 65 24 3.58 1.50 0.48 1.02 4 0
LeanPool/OrderClosures/WeaklyFatou/Moderated.lean 459 24 7.73 5.92 4.85 1.07 6 0
LeanPool/OrderClosures.lean 57 0 4.08 2.56 0.21 2.35 0 0
LeanPool/OrderClosures/GaoLeungProblem.lean 22 0 2.96 1.38 0.22 1.16 0 0
LeanPool/OrderClosures/WeaklyFatou.lean 23 0 3.11 1.29 0.21 1.08 0 0
Total 18,723 66,104 231.72 197.18 156.87 40.31 861 0

Aggregate phase totals

Phase Time
typeclass inference 57418.2 ms (= 57.42 s)
import 40311.0 ms (= 40.31 s)
tactic execution 28596.5 ms (= 28.60 s)
interpretation 20648.0 ms (= 20.65 s)
simp 17635.0 ms (= 17.64 s)
type checking 7729.9 ms (= 7.73 s)
elaboration 5688.4 ms (= 5.69 s)
blocked (unaccounted) 4634.7 ms (= 4.63 s)
tacticAnalysis 3324.5 ms (= 3.32 s)
linting 1844.9 ms (= 1.84 s)
parsing 1294.7 ms (= 1.29 s)
initialization 1256.8 ms (= 1.26 s)

Slowest changed modules (from lake build)

Changed module Lake time
LeanPool.OrderClosures.GaoLeungCharacterization 13.00 s
LeanPool.OrderClosures.BanLat.Operators.Hom 12.00 s
LeanPool.OrderClosures.BanLat.Substructures.Sublattice 10.00 s
LeanPool.OrderClosures.BanLat.OrderContinuous.MeyerNieberg 10.00 s
LeanPool.OrderClosures.Solovay 8.90 s
LeanPool.OrderClosures.WeaklyFatou.FinalSpace 8.50 s
LeanPool.OrderClosures.BanLat.Substructures.Ideal 8.40 s
LeanPool.OrderClosures.BanLat.Tactic.LLexpr 8.10 s
LeanPool.OrderClosures.BanLat.Operators.Positive 8.00 s
LeanPool.OrderClosures.GaoLeungProblem.Iterations 7.10 s
LeanPool.OrderClosures.BanLat.OrderContinuous.Basic 6.80 s
LeanPool.OrderClosures.BanLat.Disjoint 6.80 s
Per-file `lean --profile` output

LeanPool/OrderClosures.lean

import took 2.35s
cumulative profiling times:
	elaboration 0.264ms
	import 2.35s
	initialization 29.6ms
	interpretation 181ms
	linting 0.448ms
	module linting 0.00132ms
	overlappingInstancesLinter 0.645ms
	parsing 0.0659ms
	tacticAnalysis 2.09ms
real 3.13
user 1.17
sys 1.00

LeanPool/OrderClosures/BanLat/Basic.lean

import took 888ms
cumulative profiling times:
	attribute application 0.51ms
	blocked (unaccounted) 403ms
	congr simp thm 6.05ms
	elaboration 205ms
	fix level params 6.28ms
	import 888ms
	initialization 34.5ms
	instantiate metavars 6.23ms
	interpretation 697ms
	let-to-have transformation 0.49ms
	linting 70.9ms
	module linting 0.00157ms
	norm_num 10.7ms
	overlappingInstancesLinter 22.9ms
	parsing 45.3ms
	process pre-definitions 26.6ms
	ring 7.45ms
	share common exprs 15.3ms
	simp 409ms
	tactic execution 821ms
	tacticAnalysis 134ms
	type checking 121ms
	typeclass inference 2.54s
real 3.14
user 5.80
sys 0.80

LeanPool/OrderClosures/BanLat/Convergences/Order.lean

import took 882ms
cumulative profiling times:
	attribute application 0.291ms
	congr simp thm 3.05ms
	dsimp 0.816ms
	elaboration 95.9ms
	fix level params 6.24ms
	import 882ms
	initialization 29.5ms
	instantiate metavars 4.79ms
	interpretation 437ms
	let-to-have transformation 0.317ms
	linting 40.2ms
	module linting 0.0011ms
	norm_num 4.06ms
	overlappingInstancesLinter 14.1ms
	parsing 31ms
	process pre-definitions 18.3ms
	share common exprs 11.4ms
	simp 163ms
	tactic execution 447ms
	tacticAnalysis 72.6ms
	type checking 69.2ms
	typeclass inference 1.24s
real 2.31
user 3.35
sys 0.78

LeanPool/OrderClosures/BanLat/Disjoint.lean

import took 996ms
cumulative profiling times:
	attribute application 0.436ms
	congr simp thm 2.1ms
	dsimp 2.37ms
	elaboration 171ms
	fix level params 5.6ms
	import 996ms
	initialization 30.2ms
	instantiate metavars 5.14ms
	interpretation 770ms
	let-to-have transformation 0.525ms
	linting 79ms
	module linting 0.00123ms
	norm_num 0.602ms
	overlappingInstancesLinter 22.1ms
	parsing 48.6ms
	process pre-definitions 25.7ms
	share common exprs 13.7ms
	simp 56.6ms
	tactic execution 819ms
	tacticAnalysis 143ms
	type checking 96.1ms
	typeclass inference 2.56s
real 3.05
user 5.56
sys 0.86

LeanPool/OrderClosures/BanLat/Examples/CofK/Basic.lean

import took 1.02s
cumulative profiling times:
	attribute application 0.73ms
	congr simp thm 0.366ms
	elaboration 57.5ms
	fix level params 0.168ms
	import 1.02s
	initialization 41.6ms
	instantiate metavars 0.141ms
	interpretation 196ms
	let-to-have transformation 0.0331ms
	linting 3.06ms
	module linting 0.000871ms
	overlappingInstancesLinter 2.89ms
	parsing 2.08ms
	process pre-definitions 4.06ms
	share common exprs 0.444ms
	simp 6.39ms
	tactic execution 17.8ms
	tacticAnalysis 7.71ms
	type checking 23.3ms
	typeclass inference 111ms
real 1.99
user 1.26
sys 0.81

LeanPool/OrderClosures/BanLat/LLexpr.lean

import took 1.05s
simp took 202ms
cumulative profiling times:
	attribute application 11.3ms
	blocked (unaccounted) 339ms
	compilation (IR) 0.678ms
	compilation (LCNF base) 7.98ms
	compilation (LCNF impure) 4.63ms
	compilation (LCNF mono) 6.06ms
	congr simp thm 9.96ms
	elaboration 234ms
	fix level params 2.87ms
	import 1.05s
	initialization 30.5ms
	instantiate metavars 2.16ms
	interpretation 523ms
	let-to-have transformation 0.598ms
	linting 38.3ms
	module linting 0.00136ms
	norm_num 3.78ms
	overlappingInstancesLinter 20.1ms
	parsing 36ms
	process pre-definitions 29.2ms
	ring 4.8ms
	share common exprs 10.1ms
	simp 719ms
	tactic execution 316ms
	tacticAnalysis 80.4ms
	type checking 113ms
	typeclass inference 1.7s
real 3.15
user 4.73
sys 0.82

LeanPool/OrderClosures/BanLat/LatticeSeminorm.lean

import took 990ms
cumulative profiling times:
	attribute application 0.0623ms
	blocked (unaccounted) 2.56ms
	compilation (IR) 0.0451ms
	compilation (LCNF base) 0.32ms
	compilation (LCNF impure) 0.195ms
	compilation (LCNF mono) 0.227ms
	congr simp thm 1.91ms
	elaboration 34.2ms
	fix level params 0.246ms
	import 990ms
	initialization 30.5ms
	instantiate metavars 0.219ms
	interpretation 192ms
	let-to-have transformation 0.0445ms
	linting 4.33ms
	module linting 0.00126ms
	overlappingInstancesLinter 3.87ms
	parsing 2.65ms
	process pre-definitions 1.12ms
	share common exprs 0.62ms
	simp 0.53ms
	tactic execution 20ms
	tacticAnalysis 7.84ms
	type checking 25ms
	typeclass inference 98.3ms
real 1.89
user 1.21
sys 0.79

LeanPool/OrderClosures/BanLat/Normed.lean

import took 1.02s
cumulative profiling times:
	attribute application 5.19ms
	blocked (unaccounted) 58.9ms
	compilation (IR) 0.0433ms
	compilation (LCNF base) 0.505ms
	compilation (LCNF impure) 0.178ms
	compilation (LCNF mono) 0.197ms
	congr simp thm 1.15ms
	elaboration 183ms
	fix level params 2.66ms
	import 1.02s
	initialization 34.8ms
	instantiate metavars 2.42ms
	interpretation 370ms
	let-to-have transformation 0.308ms
	linting 25.9ms
	module linting 0.00129ms
	norm_num 0.382ms
	overlappingInstancesLinter 28.2ms
	parsing 26.7ms
	process pre-definitions 18.7ms
	ring 3.81ms
	share common exprs 6.91ms
	simp 10.4ms
	tactic execution 363ms
	tacticAnalysis 60.9ms
	type checking 85.2ms
	typeclass inference 1.22s
real 3.13
user 3.26
sys 0.82

LeanPool/OrderClosures/BanLat/Operators/Hom.lean

import took 1.09s
cumulative profiling times:
	attribute application 5.23ms
	blocked (unaccounted) 114ms
	compilation (IR) 0.981ms
	compilation (LCNF base) 16ms
	compilation (LCNF impure) 4.35ms
	compilation (LCNF mono) 10.4ms
	congr simp thm 15.8ms
	dsimp 2.76ms
	elaboration 428ms
	fix level params 4.1ms
	import 1.09s
	initialization 41.7ms
	instantiate metavars 2.64ms
	interpretation 466ms
	let-to-have transformation 78.2ms
	linting 43.1ms
	module linting 0.00132ms
	overlappingInstancesLinter 31.9ms
	parsing 34ms
	process pre-definitions 55.6ms
	share common exprs 9.52ms
	simp 120ms
	tactic execution 668ms
	tacticAnalysis 94.3ms
	type checking 395ms
	typeclass inference 2.96s
real 5.49
user 6.41
sys 0.87

LeanPool/OrderClosures/BanLat/Operators/Positive.lean

import took 1.01s
cumulative profiling times:
	attribute application 2.89ms
	blocked (unaccounted) 98.6ms
	compilation (IR) 0.0855ms
	compilation (LCNF base) 2.44ms
	compilation (LCNF impure) 0.416ms
	compilation (LCNF mono) 0.512ms
	congr simp thm 5.31ms
	elaboration 215ms
	fix level params 4.04ms
	import 1.01s
	initialization 30.9ms
	instantiate metavars 3.46ms
	interpretation 476ms
	let-to-have transformation 0.532ms
	linting 49.7ms
	module linting 0.00113ms
	norm_num 8.58ms
	overlappingInstancesLinter 20.9ms
	parsing 26.2ms
	process pre-definitions 18.7ms
	ring 4.97ms
	share common exprs 11.8ms
	simp 66.7ms
	tactic execution 594ms
	tacticAnalysis 113ms
	type checking 101ms
	typeclass inference 2.8s
real 3.93
user 5.34
sys 0.81

LeanPool/OrderClosures/BanLat/OrderComplete.lean

import took 885ms
cumulative profiling times:
	attribute application 0.342ms
	blocked (unaccounted) 44.7ms
	compilation (IR) 0.0453ms
	compilation (LCNF base) 0.426ms
	compilation (LCNF impure) 0.242ms
	compilation (LCNF mono) 0.893ms
	congr simp thm 1.8ms
	elaboration 75.5ms
	fix level params 1.2ms
	import 885ms
	initialization 35.9ms
	instantiate metavars 1.19ms
	interpretation 390ms
	let-to-have transformation 4.56ms
	linting 27.9ms
	module linting 0.0011ms
	norm_num 1.21ms
	overlappingInstancesLinter 9.31ms
	parsing 19ms
	process pre-definitions 11.1ms
	share common exprs 2.88ms
	simp 28.8ms
	tactic execution 252ms
	tacticAnalysis 71.3ms
	type checking 48.4ms
	typeclass inference 472ms
real 2.29
user 2.17
sys 0.75

LeanPool/OrderClosures/BanLat/OrderContinuous/Basic.lean

import took 1.04s
cumulative profiling times:
	attribute application 0.41ms
	blocked (unaccounted) 2.06ms
	congr simp thm 1.84ms
	elaboration 56.9ms
	fix level params 2.69ms
	import 1.04s
	initialization 30.6ms
	instantiate metavars 4.21ms
	interpretation 437ms
	let-to-have transformation 0.107ms
	linting 25.5ms
	module linting 0.00144ms
	norm_num 21.2ms
	overlappingInstancesLinter 11.3ms
	parsing 21.7ms
	process pre-definitions 14.5ms
	ring 8.23ms
	share common exprs 7.56ms
	simp 54.1ms
	tactic execution 321ms
	tacticAnalysis 50ms
	type checking 72.9ms
	typeclass inference 1.18s
real 2.80
user 3.10
sys 0.83

LeanPool/OrderClosures/BanLat/OrderContinuous/MeyerNieberg.lean

import took 1.02s
simp took 101ms
simp took 132ms
simp took 114ms
simp took 140ms
simp took 139ms
simp took 123ms
cumulative profiling times:
	attribute application 0.19ms
	congr simp thm 27ms
	dsimp 7ms
	elaboration 148ms
	fix level params 8.92ms
	import 1.02s
	initialization 29.8ms
	instantiate metavars 13ms
	interpretation 1.68s
	let-to-have transformation 0.416ms
	linting 99.8ms
	module linting 0.00113ms
	norm_num 157ms
	overlappingInstancesLinter 18.4ms
	parsing 74.5ms
	process pre-definitions 38.6ms
	ring 57.6ms
	share common exprs 38.9ms
	simp 1.63s
	tactic execution 1.35s
	tacticAnalysis 183ms
	type checking 241ms
	typeclass inference 5.22s
real 4.87
user 11.70
sys 0.87

LeanPool/OrderClosures/BanLat/OrderContinuous/Nakano.lean

import took 1.01s
cumulative profiling times:
	attribute application 0.0859ms
	congr simp thm 4.55ms
	elaboration 31.3ms
	fix level params 1.46ms
	import 1.01s
	initialization 29.9ms
	instantiate metavars 2.17ms
	interpretation 377ms
	let-to-have transformation 0.0983ms
	linting 15.7ms
	module linting 0.00126ms
	norm_num 30ms
	overlappingInstancesLinter 9.39ms
	parsing 12.4ms
	process pre-definitions 7.19ms
	ring 13.3ms
	share common exprs 7.48ms
	simp 86.7ms
	tactic execution 269ms
	tacticAnalysis 32.7ms
	type checking 164ms
	typeclass inference 655ms
real 2.78
user 2.52
sys 0.84

LeanPool/OrderClosures/BanLat/OrderUnit.lean

import took 1.01s
cumulative profiling times:
	attribute application 0.0337ms
	congr simp thm 0.793ms
	elaboration 15.1ms
	fix level params 0.422ms
	import 1.01s
	initialization 29.4ms
	instantiate metavars 0.311ms
	interpretation 193ms
	let-to-have transformation 0.0518ms
	linting 4.09ms
	module linting 0.00118ms
	overlappingInstancesLinter 3.72ms
	parsing 2.95ms
	process pre-definitions 8.65ms
	share common exprs 0.973ms
	simp 15.3ms
	tactic execution 38.3ms
	tacticAnalysis 7.87ms
	type checking 9.2ms
	typeclass inference 266ms
real 2.07
user 1.40
sys 0.80

LeanPool/OrderClosures/BanLat/Pi.lean

import took 1.01s
cumulative profiling times:
	attribute application 0.263ms
	compilation (IR) 0.0568ms
	compilation (LCNF base) 1.36ms
	compilation (LCNF impure) 0.273ms
	compilation (LCNF mono) 0.442ms
	elaboration 5.3ms
	fix level params 0.0386ms
	import 1.01s
	initialization 30.4ms
	instantiate metavars 0.00606ms
	interpretation 181ms
	let-to-have transformation 0.0145ms
	linting 1.35ms
	module linting 0.00107ms
	overlappingInstancesLinter 3.14ms
	parsing 0.962ms
	process pre-definitions 1.48ms
	share common exprs 0.0838ms
	tacticAnalysis 4.59ms
	type checking 4.43ms
	typeclass inference 56.9ms
real 1.83
user 1.07
sys 0.81

LeanPool/OrderClosures/BanLat/Substructures/Band/Basic.lean

import took 1.06s
cumulative profiling times:
	attribute application 0.939ms
	blocked (unaccounted) 2.89ms
	compilation (IR) 0.104ms
	compilation (LCNF base) 1.25ms
	compilation (LCNF impure) 0.504ms
	compilation (LCNF mono) 0.549ms
	congr simp thm 2.51ms
	elaboration 78.6ms
	fix level params 0.646ms
	import 1.06s
	initialization 29.8ms
	instantiate metavars 0.424ms
	interpretation 279ms
	let-to-have transformation 0.125ms
	linting 16.5ms
	module linting 0.00153ms
	overlappingInstancesLinter 9.49ms
	parsing 10.9ms
	process pre-definitions 6.17ms
	share common exprs 1.16ms
	simp 17.3ms
	tactic execution 142ms
	tacticAnalysis 30.5ms
	type checking 41.9ms
	typeclass inference 237ms
real 2.34
user 1.75
sys 0.82

LeanPool/OrderClosures/BanLat/Substructures/Band/DisjointComplement.lean

import took 1.07s
cumulative profiling times:
	attribute application 0.45ms
	blocked (unaccounted) 21.6ms
	compilation (IR) 0.297ms
	compilation (LCNF base) 14.4ms
	compilation (LCNF impure) 1.23ms
	compilation (LCNF mono) 2.02ms
	congr simp thm 1.29ms
	elaboration 65.1ms
	fix level params 0.409ms
	import 1.07s
	initialization 36.1ms
	instantiate metavars 0.296ms
	interpretation 251ms
	let-to-have transformation 0.0892ms
	linting 12.9ms
	module linting 0.00126ms
	overlappingInstancesLinter 7.34ms
	parsing 8.19ms
	process pre-definitions 4.99ms
	share common exprs 1.15ms
	simp 67.7ms
	tactic execution 51.4ms
	tacticAnalysis 24.9ms
	type checking 16.5ms
	typeclass inference 293ms
real 2.34
user 1.71
sys 0.84

LeanPool/OrderClosures/BanLat/Substructures/Ideal.lean

import took 1.07s
cumulative profiling times:
	attribute application 15.4ms
	blocked (unaccounted) 172ms
	compilation (IR) 0.886ms
	compilation (LCNF base) 18.6ms
	compilation (LCNF impure) 3.62ms
	compilation (LCNF mono) 6.03ms
	congr simp thm 5.71ms
	elaboration 719ms
	fix level params 12.8ms
	import 1.07s
	initialization 33.4ms
	instantiate metavars 11.7ms
	interpretation 1.18s
	let-to-have transformation 24.6ms
	linting 144ms
	module linting 0.00112ms
	norm_num 22.9ms
	overlappingInstancesLinter 46.7ms
	parsing 82.6ms
	process pre-definitions 109ms
	ring 17.4ms
	share common exprs 31.1ms
	simp 108ms
	tactic execution 1.42s
	tacticAnalysis 242ms
	type checking 430ms
	typeclass inference 4.41s
real 5.78
user 9.96
sys 0.88

LeanPool/OrderClosures/BanLat/Substructures/Sublattice.lean

import took 1.06s
cumulative profiling times:
	attribute application 7.92ms
	blocked (unaccounted) 1.34ms
	compilation (IR) 0.53ms
	compilation (LCNF base) 11.4ms
	compilation (LCNF impure) 2.18ms
	compilation (LCNF mono) 3.55ms
	congr simp thm 5.87ms
	elaboration 481ms
	fix level params 9.91ms
	import 1.06s
	initialization 31.2ms
	instantiate metavars 9.65ms
	interpretation 835ms
	let-to-have transformation 15.9ms
	linting 127ms
	module linting 0.00112ms
	norm_num 11.8ms
	overlappingInstancesLinter 33.2ms
	parsing 58.4ms
	process pre-definitions 65.9ms
	ring 9.47ms
	share common exprs 22.9ms
	simp 100ms
	tactic execution 1.14s
	tacticAnalysis 177ms
	type checking 263ms
	typeclass inference 2.54s
real 4.54
user 6.81
sys 0.84

LeanPool/OrderClosures/BanLat/Tactic/LLexpr.lean

import took 1.04s
do element elaborator of Lean.Parser.Term.doExpr took 102ms
compilation (LCNF base) took 178ms
cumulative profiling times:
	attribute application 0.923ms
	blocked (unaccounted) 309ms
	compilation (IR) 10.2ms
	compilation (LCNF base) 499ms
	compilation (LCNF impure) 57.5ms
	compilation (LCNF mono) 107ms
	congr simp thm 0.665ms
	do element elaborator 582ms
	dsimp 4.8ms
	elaboration 126ms
	fix level params 0.528ms
	import 1.04s
	initialization 36ms
	instantiate metavars 1ms
	interpretation 436ms
	let-to-have transformation 11.2ms
	linting 41.9ms
	module linting 0.000812ms
	overlappingInstancesLinter 8.16ms
	parsing 43.3ms
	process pre-definitions 46.8ms
	share common exprs 7.11ms
	simp 4.5ms
	tactic execution 621ms
	tacticAnalysis 124ms
	type checking 67.2ms
	typeclass inference 496ms
real 4.12
user 4.43
sys 0.85

LeanPool/OrderClosures/GaoLeungCharacterization.lean

import took 1.06s
tactic execution of Lean.Parser.Tactic.exact took 6.52s
tactic execution of Mathlib.Tactic.nlinarith took 118ms
cumulative profiling times:
	attribute application 0.69ms
	compilation (IR) 0.0713ms
	compilation (LCNF base) 4.26ms
	compilation (LCNF impure) 0.301ms
	compilation (LCNF mono) 0.533ms
	congr simp thm 29.3ms
	dsimp 8.71ms
	elaboration 338ms
	fix level params 12.4ms
	import 1.06s
	initialization 39.5ms
	instantiate metavars 12ms
	interpretation 1.03s
	let-to-have transformation 15.9ms
	linting 111ms
	module linting 0.00125ms
	norm_num 37.6ms
	overlappingInstancesLinter 26.3ms
	parsing 74ms
	process pre-definitions 62.7ms
	ring 17.8ms
	share common exprs 34.2ms
	simp 1.16s
	tactic execution 8.12s
	tacticAnalysis 163ms
	type checking 374ms
	typeclass inference 4.71s
real 9.30
user 16.90
sys 0.92

LeanPool/OrderClosures/GaoLeungProblem.lean

import took 1.16s
cumulative profiling times:
	elaboration 0.308ms
	import 1.16s
	initialization 28.9ms
	interpretation 183ms
	linting 0.421ms
	module linting 0.0012ms
	overlappingInstancesLinter 0.751ms
	parsing 0.264ms
	tacticAnalysis 4.59ms
real 1.94
user 1.10
sys 0.86

LeanPool/OrderClosures/GaoLeungProblem/CNFOrder.lean

import took 1.17s
cumulative profiling times:
	attribute application 0.299ms
	blocked (unaccounted) 74.3ms
	compilation (IR) 0.0799ms
	compilation (LCNF base) 0.71ms
	compilation (LCNF impure) 0.474ms
	compilation (LCNF mono) 0.796ms
	congr simp thm 6.61ms
	elaboration 141ms
	fix level params 10.3ms
	import 1.17s
	initialization 34.2ms
	instantiate metavars 10.6ms
	interpretation 583ms
	let-to-have transformation 0.854ms
	linting 84.3ms
	module linting 0.00175ms
	overlappingInstancesLinter 7.98ms
	parsing 52.8ms
	process pre-definitions 31.8ms
	share common exprs 14.8ms
	simp 395ms
	tactic execution 713ms
	tacticAnalysis 124ms
	type checking 107ms
	typeclass inference 295ms
real 2.59
user 3.29
sys 0.92

LeanPool/OrderClosures/GaoLeungProblem/Counterexample.lean

import took 1.15s
typeclass inference of IsStrictOrderedRing took 273ms
typeclass inference of IsStrictOrderedRing took 173ms
cumulative profiling times:
	attribute application 0.0918ms
	congr simp thm 9.11ms
	dsimp 67.9ms
	elaboration 40.7ms
	fix level params 4.24ms
	import 1.15s
	initialization 42.5ms
	instantiate metavars 5.7ms
	interpretation 630ms
	let-to-have transformation 0.126ms
	linting 46.6ms
	module linting 0.00128ms
	norm_num 18.6ms
	overlappingInstancesLinter 11.5ms
	parsing 35.8ms
	process pre-definitions 18.9ms
	ring 9.28ms
	share common exprs 11.4ms
	simp 446ms
	tactic execution 636ms
	tacticAnalysis 93.6ms
	type checking 94.8ms
	typeclass inference 1.93s
real 3.56
user 5.00
sys 0.87

LeanPool/OrderClosures/GaoLeungProblem/Iterations.lean

import took 1.14s
simp took 140ms
simp took 265ms
simp took 245ms
simp took 213ms
grind took 173ms
simp took 328ms
simp took 146ms
simp took 227ms
type checking took 412ms
cumulative profiling times:
	attribute application 5.35ms
	compilation (IR) 0.0573ms
	compilation (LCNF base) 0.754ms
	compilation (LCNF impure) 0.323ms
	compilation (LCNF mono) 0.514ms
	congr simp thm 28.3ms
	dsimp 4.88ms
	elaboration 203ms
	fix level params 13.2ms
	grind 230ms
	grind ac 8.87ms
	grind cutsat 0.318ms
	grind ematch 50.8ms
	grind linarith 13.5ms
	grind mark subsingleton 85.6ms
	grind ring 26.7ms
	grind simp 18.4ms
	import 1.14s
	initialization 42.1ms
	instantiate metavars 15.6ms
	interpretation 709ms
	let-to-have transformation 0.749ms
	linting 75.4ms
	module linting 0.00119ms
	norm_num 5.85ms
	overlappingInstancesLinter 14.5ms
	parsing 49.1ms
	process pre-definitions 47.6ms
	share common exprs 30.8ms
	simp 2.65s
	sym canon 18.5ms
	sym typeclass inference 251ms
	tactic execution 994ms
	tacticAnalysis 112ms
	type checking 745ms
	typeclass inference 2.37s
real 7.40
user 9.67
sys 0.88

LeanPool/OrderClosures/GaoLeungProblem/OrdinalSpace.lean

import took 1.15s
cumulative profiling times:
	attribute application 0.228ms
	congr simp thm 7.62ms
	dsimp 75.1ms
	elaboration 89.8ms
	fix level params 6.46ms
	import 1.15s
	initialization 40.2ms
	instantiate metavars 9.95ms
	interpretation 740ms
	let-to-have transformation 0.284ms
	linting 100ms
	module linting 0.00111ms
	norm_num 5.48ms
	overlappingInstancesLinter 8.53ms
	parsing 56.2ms
	process pre-definitions 32.8ms
	share common exprs 18.1ms
	simp 133ms
	tactic execution 956ms
	tacticAnalysis 154ms
	type checking 109ms
	typeclass inference 600ms
real 2.75
user 4.02
sys 0.86

LeanPool/OrderClosures/GaoLeungProblem/StageFormula.lean

import took 1.14s
simp took 109ms
simp took 114ms
cumulative profiling times:
	attribute application 0.18ms
	congr simp thm 14.2ms
	dsimp 19.9ms
	elaboration 83.6ms
	fix level params 6.62ms
	import 1.14s
	initialization 38ms
	instantiate metavars 8.79ms
	interpretation 634ms
	let-to-have transformation 0.328ms
	linting 83.3ms
	module linting 0.00125ms
	norm_num 4.17ms
	overlappingInstancesLinter 7.64ms
	parsing 49.2ms
	process pre-definitions 25.7ms
	share common exprs 16.4ms
	simp 736ms
	tactic execution 920ms
	tacticAnalysis 129ms
	type checking 104ms
	typeclass inference 1.25s
real 3.79
user 4.99
sys 0.88

LeanPool/OrderClosures/OrderAdherence.lean

import took 1.08s
simp took 112ms
simp took 190ms
grind took 305ms
simp took 289ms
simp took 434ms
type checking took 563ms
cumulative profiling times:
	attribute application 0.613ms
	blocked (unaccounted) 1.98s
	compilation (IR) 0.0477ms
	compilation (LCNF base) 0.407ms
	compilation (LCNF impure) 0.223ms
	compilation (LCNF mono) 0.264ms
	congr simp thm 22.9ms
	dsimp 1.93ms
	elaboration 164ms
	fix level params 3.78ms
	grind 305ms
	grind ac 8.31ms
	grind cutsat 0.225ms
	grind ematch 104ms
	grind linarith 21.5ms
	grind mark subsingleton 136ms
	grind ring 30.2ms
	grind simp 12.5ms
	import 1.08s
	initialization 31.1ms
	instantiate metavars 5.29ms
	interpretation 526ms
	let-to-have transformation 0.287ms
	linting 47.8ms
	module linting 0.00137ms
	norm_num 1.76ms
	overlappingInstancesLinter 19ms
	parsing 33.2ms
	process pre-definitions 23.2ms
	share common exprs 8.76ms
	simp 1.65s
	sym canon 17.5ms
	sym typeclass inference 168ms
	tactic execution 424ms
	tacticAnalysis 88.3ms
	type checking 653ms
	typeclass inference 1.88s
real 4.63
user 7.15
sys 0.89

LeanPool/OrderClosures/Solovay.lean

import took 1.14s
simp took 125ms
simp took 158ms
cumulative profiling times:
	attribute application 7.25ms
	blocked (unaccounted) 1.01s
	compilation (IR) 0.481ms
	compilation (LCNF base) 6.1ms
	compilation (LCNF impure) 2.09ms
	compilation (LCNF mono) 3.76ms
	congr simp thm 45.7ms
	dsimp 5.43ms
	elaboration 425ms
	fix level params 13.1ms
	import 1.14s
	initialization 30.1ms
	instantiate metavars 13.7ms
	interpretation 1.26s
	let-to-have transformation 16.6ms
	linting 146ms
	module linting 0.00125ms
	norm_num 9.08ms
	overlappingInstancesLinter 45ms
	parsing 114ms
	process pre-definitions 79.1ms
	share common exprs 33.4ms
	simp 2.21s
	tactic execution 1.37s
	tacticAnalysis 264ms
	type checking 349ms
	typeclass inference 2.57s
real 4.43
user 9.73
sys 0.97

LeanPool/OrderClosures/WeaklyFatou.lean

import took 1.08s
cumulative profiling times:
	elaboration 0.288ms
	import 1.08s
	initialization 29.7ms
	interpretation 177ms
	linting 0.427ms
	module linting 0.000931ms
	overlappingInstancesLinter 0.752ms
	parsing 0.224ms
	tacticAnalysis 2.21ms
real 1.85
user 1.05
sys 0.82

LeanPool/OrderClosures/WeaklyFatou/Bands.lean

import took 1.09s
cumulative profiling times:
	attribute application 0.354ms
	blocked (unaccounted) 0.783ms
	compilation (IR) 0.0893ms
	compilation (LCNF base) 0.728ms
	compilation (LCNF impure) 0.458ms
	compilation (LCNF mono) 0.637ms
	congr simp thm 10.6ms
	dsimp 0.962ms
	elaboration 86.6ms
	fix level params 2.56ms
	import 1.09s
	initialization 36.6ms
	instantiate metavars 5.63ms
	interpretation 719ms
	let-to-have transformation 0.846ms
	linting 60.9ms
	module linting 0.00121ms
	norm_num 31.8ms
	overlappingInstancesLinter 9.81ms
	parsing 54.4ms
	process pre-definitions 25.3ms
	ring 26.1ms
	share common exprs 20.5ms
	simp 509ms
	tactic execution 714ms
	tacticAnalysis 113ms
	type checking 159ms
	typeclass inference 1.05s
real 3.36
user 4.40
sys 0.89

LeanPool/OrderClosures/WeaklyFatou/FinalSpace.lean

import took 1.08s
type checking took 160ms
cumulative profiling times:
	attribute application 1.41ms
	congr simp thm 8.05ms
	dsimp 13.3ms
	elaboration 216ms
	fix level params 2.21ms
	import 1.08s
	initialization 33.9ms
	instantiate metavars 4.63ms
	interpretation 657ms
	let-to-have transformation 0.76ms
	linting 41.2ms
	module linting 0.00114ms
	norm_num 40.7ms
	overlappingInstancesLinter 6.65ms
	parsing 39.2ms
	process pre-definitions 43ms
	ring 13.9ms
	share common exprs 19.4ms
	simp 579ms
	tactic execution 1.41s
	tacticAnalysis 78.2ms
	type checking 1.74s
	typeclass inference 4.52s
real 6.40
user 10.31
sys 0.86

LeanPool/OrderClosures/WeaklyFatou/FiniteTree.lean

import took 1.07s
simp took 232ms
cumulative profiling times:
	attribute application 0.588ms
	compilation (IR) 0.324ms
	compilation (LCNF base) 2.97ms
	compilation (LCNF impure) 1.59ms
	compilation (LCNF mono) 2.43ms
	congr simp thm 11.4ms
	dsimp 10.8ms
	elaboration 110ms
	fix level params 0.932ms
	import 1.07s
	initialization 35.4ms
	instantiate metavars 2.7ms
	interpretation 451ms
	let-to-have transformation 0.944ms
	linting 32.8ms
	module linting 0.00123ms
	norm_num 1.93ms
	overlappingInstancesLinter 6.34ms
	parsing 30.9ms
	process pre-definitions 14.9ms
	share common exprs 5.75ms
	simp 506ms
	tactic execution 299ms
	tacticAnalysis 71.4ms
	type checking 85ms
	typeclass inference 468ms
real 2.70
user 2.96
sys 0.85

LeanPool/OrderClosures/WeaklyFatou/Moderated.lean

import took 1.07s
simp took 591ms
simp took 409ms
simp took 731ms
typeclass inference of NormedAddCommGroup took 126ms
cumulative profiling times:
	attribute application 0.0715ms
	congr simp thm 9.74ms
	dsimp 3.68ms
	elaboration 47.9ms
	fix level params 1.94ms
	import 1.07s
	initialization 35.1ms
	instantiate metavars 5.91ms
	interpretation 511ms
	let-to-have transformation 2.15ms
	linting 43.1ms
	module linting 0.00131ms
	norm_num 28.2ms
	overlappingInstancesLinter 4.01ms
	parsing 38ms
	process pre-definitions 17.2ms
	ring 17.2ms
	share common exprs 14.2ms
	simp 1.89s
	tactic execution 735ms
	tacticAnalysis 73.1ms
	type checking 190ms
	typeclass inference 1.18s
real 4.23
user 5.64
sys 0.85

LeanPool/OrderClosures/WeaklyFatou/Reductions.lean

import took 1.08s
cumulative profiling times:
	attribute application 0.114ms
	compilation (IR) 0.115ms
	compilation (LCNF base) 0.626ms
	compilation (LCNF impure) 0.544ms
	compilation (LCNF mono) 0.853ms
	congr simp thm 3.92ms
	elaboration 63.5ms
	fix level params 5.06ms
	import 1.08s
	initialization 36.4ms
	instantiate metavars 6.16ms
	interpretation 533ms
	let-to-have transformation 0.161ms
	linting 42.2ms
	module linting 0.00119ms
	norm_num 4.66ms
	overlappingInstancesLinter 12.4ms
	parsing 29.9ms
	process pre-definitions 18.5ms
	ring 11.1ms
	share common exprs 13.9ms
	simp 165ms
	tactic execution 585ms
	tacticAnalysis 73.4ms
	type checking 87.8ms
	typeclass inference 1.39s
real 2.75
user 3.86
sys 0.86

LeanPool/OrderClosures/WeaklyFatou/TreeNorm.lean

import took 1.08s
cumulative profiling times:
	attribute application 2.09ms
	congr simp thm 14.2ms
	elaboration 253ms
	fix level params 3.14ms
	import 1.08s
	initialization 36.8ms
	instantiate metavars 4.67ms
	interpretation 758ms
	let-to-have transformation 0.722ms
	linting 57.9ms
	module linting 0.0011ms
	norm_num 31.8ms
	overlappingInstancesLinter 11.1ms
	parsing 50ms
	process pre-definitions 44.7ms
	ring 31.6ms
	share common exprs 20.6ms
	simp 942ms
	tactic execution 1.05s
	tacticAnalysis 117ms
	type checking 545ms
	typeclass inference 2.15s
real 3.69
user 6.88
sys 0.88

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

@Vilin97

Vilin97 commented Sep 26, 2026 •
edited
Loading

Copy link
Copy Markdown
Owner Author 
{
  "review_kind": "Separate thorough agentic acquisition review; distinct from the configured Greptile and GPT worker reviews",
  "reviewed_commit": "0e45643ca8923ea5249d4de936e8219983c082b1",
  "conclusion": "request_changes",
  "bottom_line": "The code and wording findings are repaired and required CI passes at this head. The acquisition remains request_changes solely because public evidence does not unambiguously distinguish AI from mixed authorship of the main upstream proofs. The configured GPT verdict still targets the previous head; no current-head approval is claimed.",
  "coverage": {
    "files": "37 imported Lean modules plus the generated index and project card; the original full-source review is preserved and the later complete source/card delta is reviewed.",
    "semantic_changes": "The complete upstream-to-port diff was read in bounded chunks; the final explicit-function optimization, shared norm reductions, tactic transfer fix and all 11 regression examples were reviewed separately. The exact upstream sources and paper/formalization guide were inspected.",
    "upstreams": [
      "pedrotradacete/OrderClosures@6189ba7134f6975e7d8e4c8c093a9869d03a769c",
      "davidmunozlahoz/banlat@b00e59836016aa1099b8011add6b07385e66428e"
    ],
    "recovery": "Preserved the completed bounded full-source/upstream review at 1708a9a315dd323bc6aec9493b2f5695a1e4a38a. Compared all 37 imported module blobs: 34 are unchanged. Inspected the complete delta in the three changed modules and the project card, surrounding tactic implementation, exact endpoint statements, source Proposition 2.1, scoped repair validation and current CI logs. This is a resumed review, not a claim that the full 18k-line source review was repeated."
  },
  "rubrics": {
    "faithfulness": {
      "verdict": "pass",
      "evidence": [
        "gaoLeung_orderContinuous_characterization explicitly assumes sigma order completeness and relates sublattice adherence to order continuity of the norm.",
        "gao_counterexample constructs an order-complete C(K) with density at least the requested cardinal and a norm-closed separable sublattice whose only order-closed extension is the whole space. The card describes this endpoint and does not overclaim a literal Lean negation of GaoLeungProperty.",
        "solid_sets_require_arbitrarily_many_iterations retains the infinite-cardinal hypothesis, successor-cardinal initial-ordinal bound, every strict stage, and the universe lift.",
        "exists_weaklyFatou_not_equivalent_fatou constructs a genuine positive-definite lattice norm, proves sequential metric completeness and constant-2 weak Fatou, and excludes every equivalent Fatou norm via positive comparison constants.",
        "Order-convergence witnesses require nonempty directed index types; the hard construction steps are proved rather than assumed in structures. The selected dependency closure supplies those proofs.",
        "The earlier review missed order-density wording in the summary/entry exposition. At 0e45643c that wording is corrected to the exact only-order-closed-vector-sublattice-extension property, matching gao_counterexample. Mathematical statements and proofs were not weakened."
      ]
    },
    "novelty": {
      "verdict": "pass",
      "evidence": "Registry, directories, PRs, issues and relevant history contain no duplicate acquisition; targeted Mathlib/pool searches did not locate these endpoint results. Elementary supporting facts overlap the ordinary mathematical vocabulary, while the preserved lattice/net/Boolean and transfinite infrastructure forms a coherent prerequisite library."
    },
    "significance": {
      "verdict": "pass",
      "fit": "lean_pool",
      "evidence": "Completed functional-analysis research combining the Gao–Leung characterization, large-density Stone-space construction, arbitrary transfinite adherence lengths and a complete non-renormable weak Fatou example. The natural reusable infrastructure and substantial linked constructions justify preservation beyond a single isolated exercise. This is completed content rather than a challenge statement."
    },
    "sources": {
      "verdict": "pass",
      "source_match": "matches",
      "evidence": "The paper supports the four precisely qualified card statements. The source commits and full Apache-2.0 licenses were verified for both repositories. BanLat attribution, Jaume de Dios Pont's earlier Section 3 formalization, and the Elliott/Wickstead mathematical credit are retained. Completion on 2026-08-26T18:19:54Z and the public paper on 2026-09-06T15:59:03Z fall in the exact eligible interval. The later correction identifies Proposition 2.1 accurately and removes the unsupported order-density claim from both source descriptions; the primary paper confirms the extension property."
    },
    "quality": {
      "verdict": "pass",
      "code_quality": 4,
      "evidence": "The 17 paper modules retain 20 useful dependency modules. Eleven unused modules and broad tactic imports were removed; typeclass/elaboration hot spots were repaired using profiling. Four recursive tactic helpers are total, three long construction proofs have meaningful helper boundaries, and duplicated norm reductions now specialize the general lemmas. Eleven tactic examples found and now cover a mixed-sign transfer defect. The explicit lattice-norm interface preserves generality instead of forcing an ambient topology change. The later evalLlarith implementation uses focus internally. Two additional regression examples enter the evaluator with three explicit metavariable goals and check preservation of the exact sibling goal IDs and order, with unsigned transfer and signed fallback paths; all thirteen examples compile in current CI."
    }
  },
  "validation": {
    "local": "Retained original warning-free project-clean builds, generated-index check, 15 Mathlib linters, style and full standard quality/trust checks from the source-identical project audit checkout. The subsequent focused repair has warning-free compilation, style/card checks and direct transfer-theorem axiom checks recorded in the published repair review. No new local build was necessary in this resume; current-head integration validation is supplied by CI.",
    "ci": "Head 0e45643ca8923ea5249d4de936e8219983c082b1: Lean Action CI run 36234298867 passed. Its logs explicitly rebuild all 37 OrderClosures modules and freshly validate lint, declarations, axioms and backdoors for this project. Index, challenge/solution, text-style and repository-quality steps passed. Required Build project, Content / non-content separation and Documentation preflight checks are green. Unchanged projects may use the configured validation cache; this is not a claim every pooled module was freshly linted. Strict base freshness is not satisfied (BEHIND).",
    "greptile": "Current-head Greptile review completed successfully at 2026-09-26T09:59:43Z with no outstanding finding. Both original threads remain resolved.",
    "gpt": "The published request_changes verdict reviews f0d23ffff21ae6dcb6c01b899bee5e1585ca31fe. Its order-density/source wording and sibling-goal findings are repaired in 0e45643ca8923ea5249d4de936e8219983c082b1. No configured GPT verdict for that repaired head was published at this observation. The original /review request is retained; no duplicate request was posted."
  },
  "compile_measurements": {
    "command": "/usr/bin/time -v lake build LeanPool.OrderClosures after removing only this project's build artifacts",
    "conditions": "Same Azure VM, Lean 4.34.0, Mathlib 5ed2965256430c3649e86755f9576b54eca72435, default Lake concurrency, warm dependency oleans/configuration/file cache, no other task-specific compilation during each controlled pair; shared-host timing variation is possible.",
    "baseline_wall_seconds": [
      69.98,
      71.73
    ],
    "final_wall_seconds": [
      38.04,
      39.1
    ],
    "mean_reduction_percent": 45.6,
    "evidence": "Preserved original per-file profiling, clean-build logs and baseline source archive. The 45.6% comparison measures the completed optimization pass. No additional substantive optimization was made in this resume; neither old remote profiling nor the later focused validation is substituted for a controlled final-head measurement.",
    "optimized_measured_commit": "1708a9a315dd323bc6aec9493b2f5695a1e4a38a",
    "measurement_limit": "The controlled optimized pair is for the 11-example source at 1708a9a31, before the later focus change and two additional examples. The 4.14-second focused-module local check and current CI module timings are different experiments, not a comparable new project-clean pair."
  },
  "remaining_findings": [
    {
      "file": "LeanPool/OrderClosures.lean",
      "line": 45,
      "rule": "acquisition-provenance-confirmation",
      "comment": "Public evidence still establishes AI participation without settling predominantly AI versus substantial human-plus-AI proof authorship. Current public upstream HEAD remains 6189ba7134; its 12-commit history, README, formalization guide, paper and empty issue/release lists provide no new conclusive classification. The exact-window X/Zulip records are unchanged. Retain the disclosed inference and hold automatic merge until first-party confirmation or conclusive public authorship evidence permits confirming or correcting the enum. This is an external factual gap, not an editable attribution repair left undone.",
      "evidence": "The entry module says: \"The AI provenance classification is an evidence-based inference\". Main history records phase-specific agent instructions and a phase-II proof pass; BanLat discloses LLM-assisted implementation. Those establish AI participation, but do not settle AI versus mix for the main formalization."
    }
  ],
  "updated_at": "2026-09-26T11:04:55.238089+00:00"
}

@Vilin97

Vilin97 commented Sep 26, 2026

Copy link
Copy Markdown
Owner Author

/review

@Vilin97

Vilin97 commented Sep 26, 2026

Copy link
Copy Markdown
Owner Author

Changes requested by automated review

Reconciled to exact current head 21075bfc5bcc9227006f062bfbece509e574d7e2. The main-branch integration leaves this project’s Lean sources byte-identical to the reviewed source; the existing substantive findings and acceptance conditions remain unresolved. The mathematics and implementation remain suitable, but the AI-versus-mix proof-provenance classification is explicitly an inference. First-party confirmation or other conclusive public evidence is still required; AI participation alone does not establish predominantly AI authorship.

Preserve the valid completed repairs. Merge requires the cited author-actionable defects to be resolved and all protected checks to pass at the resulting head; this is not a needs-maintainer handoff.

@Vilin97

Vilin97 commented Sep 26, 2026

Copy link
Copy Markdown
Owner Author

🤖 LLM review (gpt-6-astra, 5 rubrics)

Reviewed head: f0d23ffff21ae6dcb6c01b899bee5e1585ca31fe

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

Rubric Verdict Bottom line
Faithfulness 🛑 block The four main_results match their Lean statements, but the summary and entry module overclaim order density.
Novelty ✅ pass Full-diff review and direct searches of pinned Mathlib and the reviewed pool projects found no duplicate of any of the four headline results.
Significance ✅ pass This is a substantial, completed research project in Banach-lattice theory with clear construction and characterization theorems.
Sources 🛑 block Correct the two order-density claims: the cited Proposition 2.1 establishes generation under order closure, a different property.
Code quality (advisory) 🤔 discuss The code is generally maintainable, but a maintainer should address llarith's loss of sibling goals.
Aspect Value
Proves the claim 🟡 weaker_than_claimed
Assumed, not proved The characterization assumes a sigma-order-complete Banach lattice; the iteration theorem assumes an infinite cardinal and the stated successor-initial-ordinal bound, with a universe lift. These restrictions are disclosed. No undisclosed headline assumption was found.
Matches cited source 🛑 mismatch
Fit ✅ good_fit
Level research
Branch functional analysis
Mode theory_building
Code quality 3 / 5

Statement check: gao_counterexample constructs a closed separable sublattice whose only order-closed vector-sublattice extension is the whole space; it does not establish order density.

The formalization develops the paper's separation of weak Fatou and Fatou renormability, arbitrarily long solid order-adherence towers, and the Gao–Leung characterization of order-continuous norms.

Faithfulness findings (1)

  • overclaimed-headline — LeanPool/projects.yml:9
    Replace ‘separable order-dense sublattices’ with the extension property already stated accurately in main_results, and correct the same wording in LeanPool/OrderClosures.lean:53. Order density requires every positive nonzero ambient element to dominate a positive nonzero element of Y. Having no proper order-closed sublattice extension is a different, weaker property: generation through iterated order limits does not establish that domination condition. The current wording advertises an additional mathematical property the endpoint does not prove.
    Evidence: LeanPool/OrderClosures/GaoLeungProblem/Counterexample.lean:44–51: theorem gao_counterexample (κ : Cardinal.{u}) : ∃ (K : Type u) (_ : TopologicalSpace K) (_ : CompactSpace K) (_ : T2Space K), IsOrderComplete C(K, ℝ) ∧ κ ≤ densityCharacter C(K, ℝ) ∧ ∃ Y : VectorSublattice C(K, ℝ), IsClosed (Y : Set C(K, ℝ)) ∧ TopologicalSpace.IsSeparable (Y : Set C(K, ℝ)) ∧ ∀ Z : VectorSublattice C(K, ℝ), Y ≤ Z → IsOrderClosed (Z : Set C(K, ℝ)) → Z = ⊤

Sources findings (1)

  • source-mismatch — LeanPool/projects.yml:9
    The cited Proposition 2.1 supplies a separable norm-closed sublattice whose only order-closed sublattice extension is C(K). It does not assert order density, which requires a positive element of Y below every positive nonzero ambient element (Definition 2.4). Calling this construction order-dense attributes a stronger result to the source. Replace that wording here and in LeanPool/OrderClosures.lean:53 with the order-closed-extension property already used in the main_results description.
    Evidence: The summary claims ‘construction of order-complete C(K) spaces with arbitrarily large density and separable order-dense sublattices’, citing ‘Paper Theorem 2.1, via the Solovay Boolean algebra.’ The entry module repeats ‘norm-closed separable order-dense sublattice’. The corresponding declaration, gao_counterexample (Counterexample.lean:44–51), instead concludes: ‘∀ Z : VectorSublattice C(K, ℝ), Y ≤ Z → IsOrderClosed (Z : Set C(K, ℝ)) → Z = ⊤’.

Code quality findings (1)

  • tactic-goal-management — LeanPool/OrderClosures/BanLat/Tactic/LLexpr.lean:403
    Both assertAtomSignFacts (line 310) and closeByTransfer (line 403) replace the entire goal list while modifying only the main goal. evalLlarith uses withMainContext without focusing, so invoking its transfer path with multiple active goals discards untouched sibling goals without assigning them. A standalone Lean test of this exact bookkeeping sequence confirms the loss. Focus the implementation, or preserve the goal tail and isolate the fallback tactics. Add multi-goal regression examples covering transfer with and without sign hypotheses; the existing examples all start with one goal.
    Evidence: assertAtomSignFacts: let (_, goal) ← (← (← getMainGoal).assert signName proofType proof).intro1P setGoals [goal]. closeByTransfer: let (_, goal) ← (← (← getMainGoal).assert transferName proofType proof).intro1P setGoals [goal]. Entry points: def evalLlarith : TacticM Unit := withMainContext do and elab "llarith" : tactic => evalLlarith.

Tokens: 16,260,773 in / 39,384 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $328.1693 (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.
request_changes is an ask, not a close: of the reviewer's past request_changes verdicts, 39% were merged after a human looked. Read the findings before acting on the verdict.

Vilin97
Vilin97 commented Sep 26, 2026
View reviewed changes

@Vilin97 Vilin97 left a comment

Copy link
Copy Markdown
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

{
"review_scope": "Focused four-file repair at 0e45643. This does not replace the earlier substantive project review.",
"verdict": "The scoped repair passes source review and bounded validation; overall project acceptance remains on hold.",
"changes": [
"The card, entry exposition and counterexample docstring now describe the actual only-order-closed-vector-sublattice-extension property. The source reference is Proposition 2.1; no order-density claim remains in these descriptions. Mathematical statements and proofs are unchanged.",
"evalLlarith now focuses its main goal internally, so helper calls that replace the goal list preserve the caller's sibling goals.",
"Two new regressions exercise unsigned transfer and signed fallback with three actual MVarIds at evaluator entry. They assert main-goal closure and the exact remaining sibling IDs/order before closing those siblings. The original eleven examples remain."
],
"validation": {
"toolchain": "Lean v4.34.0; exact pinned Mathlib 5ed2965256430c3649e86755f9576b54eca72435; 8 GiB aggregate process cap and -j2.",
"compilation": "Basic and LLexpr compiled warning-free; their twelve artifact parts were retained under SHA guards. The final Tactic.LLexpr module recompiled warning-free in 4.14 seconds, including all thirteen examples.",
"axioms": "Exactly LLexpr.vanishes_of_vanishes_real and LLexpr.eval_eq_of_vanishes_real were checked; both use only propext, Classical.choice and Quot.sound.",
"checks": "Native style checked the three changed Lean files. All four existing scoped quality checks and card/metadata checks passed. All thirty-seven project files, existing imports, unrelated card bytes and configuration/root-index bytes were preserved. Final hashes verified the frozen inputs, direct pinned dependency inputs and eighteen own module artifact parts."
},
"limits": [
"No whole-project compilation or linter run is claimed. The native global index check remains for CI because this checkout is sparse; no module paths or imports changed.",
"Fresh required CI at this published head remains necessary.",
"First-party evidence distinguishing AI from mixed authorship is still missing. The existing AI metadata, qualified inference and provenance hold are unchanged. This review is not a whole-project approval or merge authorization."
]
}

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@greptile-apps greptile-apps[bot] greptile-apps[bot] left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@Vilin97