Repository navigation

perf: adopt modules and reduce Lean Pool build cost - #415

Merged

Vilin97 merged 229 commits into

mainfrom

codex/module-import-optimization

Sep 18, 2026

Merged

perf: adopt modules and reduce Lean Pool build cost#415
Vilin97 merged 229 commits into
mainfrom
codex/module-import-optimization

Commits on Sep 11, 2026
Commits on Sep 12, 2026
- style: remove trailing blank line
  Vilin97
  committed
  d0a8bb4
- Optimize Bollobas-Nikiforov module imports
  Vilin97
  committed
  2d9fc3e
- Reduce Lie solver interface and preserve standalone tactics
  Vilin97
  committed
  c6d31ae
- Preserve module exports in regenerated pool index
  Vilin97
  committed
  58c8237
- Optimize Gardam certificates by combining formal-sum coefficients
  Vilin97
  committed
  a0821a7
- Reduce symplectic certificate checks to independent row pairings
  Vilin97
  committed
  ba17369
- Evaluate octagon coverage certificates once in the kernel
  Vilin97
  committed
  d30b789
- Simplify hypergraph certificate proofs and evaluate them in the kernel
  Vilin97
  committed
  92230c8
- Speed up kernel-checked GKP finite-range certificates
  Vilin97
  committed
  77efad8
- Reuse finite-support and algebra-equivalence constructions in Brauer proof
  Vilin97
  committed
  51636a5
- Evaluate compressed basis entries over nonzero coordinates
  Vilin97
  committed
  f50676d
- Reuse block nonexistence and tensor basis proofs in Monlib
  Vilin97
  committed
  ea8374b
- Avoid expanding subdivision homeomorphisms in fan center equality
  Vilin97
  committed
  d2ae90d
- Check Hadwiger symmetry tables directly in the kernel
  Vilin97
  committed
  8e17e69
- Keep weighted circle coordinate homeomorphisms folded
  Vilin97
  committed
  9c07ca9
- Reuse finite-sum bounds in Monlib uniqueness proof
  Vilin97
  committed
  5dd1db3
- Share Nesterov curvature estimates across state families
  Vilin97
  committed
  d865a72
- Simplify finite interpolation tree path proofs
  Vilin97
  committed
  3b23eff
- Reuse chart compatibility certificates and focus affine evaluation
  Vilin97
  committed
  be931aa
- Simplify cycle embeddings and Hamming distance bounds
  Vilin97
  committed
  091312b
- Check Erdos97 finite row tables directly in the kernel
  Vilin97
  committed
  e7237b9
- Share local mesh case analysis in subdivision proofs
  Vilin97
  committed
  9b3d553
- Apply existing analytic input lemmas without broad simplification
  Vilin97
  committed
  4a42ef7
- Reuse analytic bounds in invariance of domain proofs
  Vilin97
  committed
  27e803d
- Reuse boundary factorization and cutoff bounds in modular forms
  Vilin97
  committed
  4ab6c65
- Reuse affine independence and focus plane geometry proofs
  Vilin97
  committed
  f53caab
- Reuse coefficient and limit identities in Hermite basis proofs
  Vilin97
  committed
  c19d599
- Reuse IdentDistrib.add in the PFR sum-distance proof
  Vilin97
  committed
  3fd06f7
- Reuse minterm identities and simplify Shannon circuit proof bounds
  Vilin97
  committed
  283bc6a
- Share affine parameter bounds in graph polygonalization
  Vilin97
  committed
  82cc72b
- Use direct order bounds in Burkholder monotonicity proofs
  Vilin97
  committed
  775cc1b
- Prepend fixed word prefixes directly
  Vilin97
  committed
  8c14a0a
- Simplify Schur product proofs using existing linear-map identities
  Vilin97
  committed
  80a83b0
- Simplify LatticeTriangle arithmetic and sum proofs
  Vilin97
  committed
  f4f578a
- Use direct ideal and cardinality bounds in Krull domain proofs
  Vilin97
  committed
  ed8bf42
- Apply tensor restriction identities directly
  Vilin97
  committed
  efc4909
- Reuse the small norm bound for radial projection
  Vilin97
  committed
  29af292
- Infer rewrite words from their established hypotheses
  Vilin97
  committed
  dad36e7
- Reuse prime transport and direct height bounds in transfinite construction
  Vilin97
  committed
  881d7c6
- Share ambient mesh injectivity in chart weld proofs
  Vilin97
  committed
  6ee407a
- Reuse finite-set and collision arguments in Scarf proofs
  Vilin97
  committed
  ec6fddb
- Share the N-subring union construction and its cardinality bounds
  Vilin97
  committed
  3d396ce
- Reuse scaled basis facts in the Brauer quotient proof
  Vilin97
  committed
  0e22609
- Use dimension and union identities in polygon separation proofs
  Vilin97
  committed
  87fd891
- Use annihilator and polynomial identities in prime-adjoining proofs
  Vilin97
  committed
  84e90f4
- Check template coordinate uniqueness through finite lists
  Vilin97
  committed
  5dbd6e6
- Reuse adaptive fan coordinate formulas in affine proofs
  Vilin97
  committed
  9a96428
- Reuse equivalences in double centralizer proofs
  Vilin97
  committed
  650f561
- Use direct normalization and scaling identities in word closures
  Vilin97
  committed
  e3c4236
- Separate opposite diamond triangles directly
  Vilin97
  committed
  449f095
- Reuse the tensor factor centralizer theorem
  Vilin97
  committed
  7b0e933
- Reuse adic completeness and simplify Noetherian filtration proofs
  Vilin97
  committed
  d44fc24
- Use direct monotonicity and factorization proofs for ABC exceptions
  Vilin97
  committed
  955257c
- Use explicit block coefficient identities in matrix proofs
  Vilin97
  committed
  0d237fe
- Reuse the adic completion evaluation kernel theorem
  Vilin97
  committed
  109df9b
Commits on Sep 13, 2026
- Select geometry bounds directly in ABC estimates
  Vilin97
  committed
  c0be201
- Use polynomial translation identities in critical value positivity
  Vilin97
  committed
  c68c92d
- Reuse algebra map facts in Frobenius proofs
  Vilin97
  committed
  9b644c6
- Simplify two-generator close-up and prime ideal proofs
  Vilin97
  committed
  3a7296e
- Reuse height and cardinality facts in no-common-factor proofs
  Vilin97
  committed
  52aec04
- Clear singular-point denominators with field_simp
  Vilin97
  committed
  f88a5d7
- Use direct evaluation and sign bounds in the Obreschkoff proof
  Vilin97
  committed
  f898cf7
- Use explicit coefficient identities in Obreschkoff transport
  Vilin97
  committed
  833a072
- Share subring closure proofs in the height construction
  Vilin97
  committed
  985fc53
- Use recurrence and sign identities in Biswal proofs
  Vilin97
  committed
  2c3a891
- Use direct cardinality and height facts in adjoining surjectivity
  Vilin97
  committed
  b4d9697
- Reuse continuity and finite-infimum bounds in root perturbation
  Vilin97
  committed
  73874a5
- Merge main while preserving module import interfaces
  Vilin97
  committed
  21d4442
- Share coefficient recurrence proofs in the hypergeometric equations
  Vilin97
  committed
  93ac224
- Use direct identities and bounds in Chudnovsky coefficient estimates
  Vilin97
  committed
  2b34f00
- Share denominator clearing and remove unused UFD construction proofs
  Vilin97
  committed
  0207184
- Prune the private discriminant search before enumerating multipliers
  Vilin97
  committed
  bc4d7c3
- Reuse coefficient and cocycle identities in cross product algebra
  Vilin97
  committed
  f2562d5
- Reuse the shared union construction in combined extension steps
  Vilin97
  committed
  d098780
- Use focused bounds in the Chudnovsky truncation estimates
  Vilin97
  committed
  e6124ad
- Reuse direct summand identities in Azumaya tensor proofs
  Vilin97
  committed
  6d06681
- Use direct positivity in the winding-factor proof
  Vilin97
  committed
  8c575ff
- Reuse interval bounds and a common Cauchy product limit
  Vilin97
  committed
  22e7c4f
- Use explicit positivity in the Kummer Wronskian proof
  Vilin97
  committed
  7415f11
- Reuse matrix and tensor equivalences in Brauer group proofs
  Vilin97
  committed
  ed3d359
- Use direct order bounds in the modular j valence proofs
  Vilin97
  committed
  cf57f60
- Reuse completion kernel and tensor range proofs in Anderson Main
  Vilin97
  committed
  1069d2d
- Share the coefficient decomposition in local power series proofs
  Vilin97
  committed
  ea82149
- Reuse integer periodicity in the sigma product formula
  Vilin97
  committed
  19c22e6
- perf: reuse separability and commuting-adjoin proofs
  Vilin97
  committed
  2eb5e38
- Use direct integer bounds in the CM representative proofs
  Vilin97
  committed
  88d627d
- Focus the maximum-modulus radius estimate
  Vilin97
  committed
  d1da4ef
- Reuse Jensen theorems and lift generators through finite preimages
  Vilin97
  committed
  bcb73ed
- perf: simplify matching and weighted sum proof elaboration
  Vilin97
  committed
  eeec700
- Simplify the finite matrix checks for the S coset permutation
  Vilin97
  committed
  61a2410
- Share the quotient recurrence in the Anderson domain proof
  Vilin97
  committed
  a8b5119
- perf: share matrix identities in Cartan existence proofs
  Vilin97
  committed
  f3881a0
- Share the factorial recurrence in the Chudnovsky main theorem
  Vilin97
  committed
  623da04
- Bound and check the Masser norm-form solutions directly
  Vilin97
  committed
  6b502c1
- Induct on cocycles and use direct linear-map laws in Cech multiplication
  Vilin97
  committed
  2fd55c0
- Simplify finite generators and annihilator arguments in Heitmann proposition
  Vilin97
  committed
  fbf4de3
- perf: derive global Vlasov flow bounds from local theorems
  Vilin97
  committed
  28657c2
- Reuse the lattice equivalence zero formula
  Vilin97
  committed
  b3544c7
- Share the sigma-factor derivative and focus the norm bounds
  Vilin97
  committed
  7aa9f5b
- Reuse the completion equivalence in Jensen construction
  Vilin97
  committed
  7714e21
- Use direct power-series cancellation for the j expansion
  Vilin97
  committed
  2aa3219
- Use direct period and degree bounds for the modular polynomial
  Vilin97
  committed
  780cc90
- perf: derive generalized convergence bounds directly
  Vilin97
  committed
  caa76ff
- Use direct matrix and prime arguments for CM rationality
  Vilin97
  committed
  369ff98
- Share cocycle induction across Cech inclusions and multiplication
  Vilin97
  committed
  646f1da
- Simplify quadratic-form root and matrix cancellation proofs
  Vilin97
  committed
  4049b87
- perf: share entropy expansion in rho continuity proof
  Vilin97
  committed
  a1c3b4e
- Share the factorial bound across the Chudnovsky normalization proofs
  Vilin97
  committed
  8b5d379
- Reuse section restrictions and finite-support sums in Laurent-tail proofs
  Vilin97
  committed
  45c03ed
- Reuse prime ideal and local ring facts in transcendental adjoining
  Vilin97
  committed
  1312a6c
- perf: reuse weight monotonicity in H1 exchange proof
  Vilin97
  committed
  7828ed9
- Use direct cancellation in the two-circle uniqueness proof
  Vilin97
  committed
  36f6f52
- Focus the metric dichotomy arithmetic and cancel positive factors
  Vilin97
  committed
  c60d965
- perf: share generic fibre polynomial evaluation proof
  Vilin97
  committed
  1d3989a
- Share the three-rank chain argument between cover proofs
  Vilin97
  committed
  11e8834
- Use direct prepared facts and square-order bridges in terminal closure
  Vilin97
  committed
  4ec2f23
- perf: reuse ZF function graph and product proofs
  Vilin97
  committed
  12fd914
- Normalize unordered-pair membership before finite distance checks
  Vilin97
  committed
  4a0315a
- Use direct radial and positive-sum bounds in the diameter lens
  Vilin97
  committed
  19eafc7
- Reuse cocycle induction and direct equalities in the six-term sequence
  Vilin97
  committed
  1bd4f2b
- Use direct turn and positivity arguments in majorant arc nesting
  Vilin97
  committed
  d8ae217
- perf: reuse PFR endgame permutation bounds
  Vilin97
  committed
  92955cd
- Share the three-rank chain theorem with the cover reduction
  Vilin97
  committed
  0dcfb8c
- Reuse coboundary linearity and global section gluing in skyscraper proofs
  Vilin97
  committed
  7521e1e
- Share Mittag-Leffler refinement compatibility with both callers
  Vilin97
  committed
  bf9733e
- Use explicit circle identities in the penultimate-point geometry
  Vilin97
  committed
  8983fbf
- Reduce the exact rational regression certificates in the kernel
  Vilin97
  committed
  8cf5a0d
- perf: simplify torsion PFR independence proofs
  Vilin97
  committed
  776692e
- Use square-order lemmas in the maximal-gap tail geometry
  Vilin97
  committed
  443a578
- Use local offset facts directly in the global degree assembly
  Vilin97
  committed
  fb0b72c
- Share gluing restrictions and use direct H0 cochain equalities
  Vilin97
  committed
  94149f5
- Reuse rank chains and square-order facts for coordinated majorants
  Vilin97
  committed
  539d078
- Use square-order facts for the equal-third-rank diagonal argument
  Vilin97
  committed
  104b1b8
- perf: kernel-check closed Runge-Kutta certificates
  Vilin97
  committed
  9ccd591
- Cancel the zero sum of squares in squared-distance positivity
  Vilin97
  committed
  4a81267
- Reduce finite enumeration completeness proofs in the kernel
  Vilin97
  committed
  0b9c446
- Reuse matrix-unit identities in multiplication adjoint proof
  Vilin97
  committed
  bcb4945
- Reuse cochain linearity and section bounds in the bounded trade
  Vilin97
  committed
  1008e3a
- Use explicit winnability cases in the lifted strategy dichotomy
  Vilin97
  committed
  d2410e6
- perf: reuse general Ext and zero-object proofs
  Vilin97
  committed
  3a295bb
- Restrict the lifted winning-condition projection simplification
  Vilin97
  committed
  b786acf
- perf: apply the PFR chain rule without index transports
  Vilin97
  committed
  587aaab
- Expand matrix representation sums with the product identity
  Vilin97
  committed
  7d3139b
- Use definitional equality in the short lifted-tree projection
  Vilin97
  committed
  1b0dfe5
- Restrict the short strategy projection simplification
  Vilin97
  committed
  2ebea77
- Reuse quotient and refinement identities in Dolbeault comparison
  Vilin97
  committed
  a2f464a
- perf: share independent-copy distribution comparisons
  Vilin97
  committed
  1fb1f9b
- Apply zero criteria directly in the Abel Dolbeault bridge
  Vilin97
  committed
  63bca65
- Use diagonal injectivity for scalar matrices
  Vilin97
  committed
  f781c32
- Merge remote-tracking branch 'origin/main' into pr-415
  github-actions[bot]
  committed
  196cd52
- Use list projection laws in the losing lift construction
  Vilin97
  committed
  0f49c22
- Reuse chart and product identities in the Abel upgrade
  Vilin97
  committed
  7997b6b
- perf: simplify Ramanujan arithmetic proof bounds
  Vilin97
  committed
  01a8f1a
- Use direct quotient and dimension identities for the Serre functional
  Vilin97
  committed
  08b3eb7
- Use explicit logical facts in the zero-player strategy proof
  Vilin97
  committed
  052f2b7
- Simplify the preimage calculations in Borel determinacy
  Vilin97
  committed
  0f9dc52
- Reuse length preservation in the tree restriction functor
  Vilin97
  committed
  26c1f1b
- Use prefix lemmas in the short-lift projection
  Vilin97
  committed
  19851ee
- Merge upstream PR update and preserve module imports for matching project
  Vilin97
  committed
  aadad16
- Merge commit 'aadad161fe4e93127377e6a4efc52c52136e4d30' into codex/module-import-optimization
  Vilin97
  committed
  c07200b
- perf: share conjoined automaton edge witnesses
  Vilin97
  committed
  18b161b
- Use player residual cancellation in the winning-prefix proof
  Vilin97
  committed
  771f25a
- Reuse the limit-body projection theorem
  Vilin97
  committed
  f2b5f66
- Use direct membership facts in the closed-game proofs
  Vilin97
  committed
  c1ac397
- Privatize matching implementation imports
  Vilin97
  committed
  a1aa4f4
- perf: use direct bounds along automaton paths
  Vilin97
  committed
  aba13b9
- Simplify bounded cocycle kernel and restriction proofs
  Vilin97
  committed
  10f4aa1
- Use direct bounds in the matching potential estimate
  Vilin97
  committed
  1eac46d
- Remove an unused simp argument in the losing-prefix proof
  Vilin97
  committed
  e55f6bf
- Use naturality directly in the system-lift correspondence proof
  Vilin97
  committed
  ca7ceda
- Compose the matching threshold bounds directly
  Vilin97
  committed
  1df48b0
- perf: use direct orbit and quotient cardinality proofs
  Vilin97
  committed
  63d1d7d
- Use direct quotient equivalences in the adele filtration proofs
  Vilin97
  committed
  54e9431
- Share restriction calculations in Leray gluing proofs
  Vilin97
  committed
  ede6e24
- Merge remote-tracking branch 'origin/main' into pr-415
  github-actions[bot]
  committed
  e7b024e
- Simplify finiteness and zero-quotient proofs for Riemann-Roch spaces
  Vilin97
  committed
  b331104
- Use direct restriction and quotient identities for Cech refinement
  Vilin97
  committed
  0a72656
- perf: simplify Pebbling parameter budget estimates
  Vilin97
  committed
  0a96125
- Reuse modular lattice identities in the adele sandwich proofs
  Vilin97
  committed
  b238c9c
- perf: share Rellich chartwise transport proofs
  Vilin97
  committed
  b6b3649
- Share inclusion bounds in Cech differential proofs
  Vilin97
  committed
  a339f5c
- Reconcile upstream projects with module headers; visibility repairs pending
  Vilin97
  committed
  28f6afc
- Integrate upstream module conversion checkpoint
  Vilin97
  committed
  3566aa3
- Share patch restriction identities in Cech injectivity
  Vilin97
  committed
  7708057
- Use quotient membership in window dimension proofs
  Vilin97
  committed
  de6a313
- Restore the generated module index header
  Vilin97
  committed
  e7ea4d0
- Share order bounds and compose Laurent-tail identities
  Vilin97
  committed
  ee3f81d
- fix(QuantumParallelRepetition): complete module visibility
  Vilin97
  committed
  e25b681
- Reuse order bounds and interval sums in LatticeTriangle proofs
  Vilin97
  committed
  9b52a00
- perf(RellichKondrachov): simplify the chart range coercion proof
  Vilin97
  committed
  5b8fd52
- fix: complete MetricCodes module compatibility
  Vilin97
  committed
  2411ec2
- perf: guide residue-field torsion-free synthesis
  Vilin97
  committed
  6be8e3a
- Compose existing bounds in LatticeTriangle estimates
  Vilin97
  committed
  119cefb
- Simplify LatticeTriangle sum reindexing and telescoping proofs
  Vilin97
  committed
  c87169d
- Merge remote-tracking branch 'origin/main' into pr-415
  github-actions[bot]
  committed
  0dc7314
- perf: simplify Weil differential finiteness proofs
  Vilin97
  committed
  71f616c
- Merge commit '0dc7314fec74a70a57dd63853d42d01c11c6e2e6' into codex/module-import-optimization
  Vilin97
  committed
  b11edbc
- Merge commit '76d2444305cb934243f18108fe173b8a0fa0d718' into codex/module-import-optimization
  Vilin97
  committed
  cca2b10
- Preserve module exports after the upstream index update
  Vilin97
  committed
  3e8d4cd
Commits on Sep 14, 2026
- Merge remote-tracking branch 'origin/main' into pr-415
  github-actions[bot]
  committed
  3854dd7
Commits on Sep 16, 2026
- Merge remote-tracking branch 'origin/main' into pr-415
  github-actions[bot]
  committed
  a6909d2
Commits on Sep 17, 2026
Commits on Sep 18, 2026

Commits

Commits on Sep 11, 2026

Commits on Sep 12, 2026

Commits on Sep 13, 2026