WIP: Import Riemannian curvature and geometric analysis toward Ricci flow

[Vilin97]

Imports arthur742ramos/lean-poincare-formalization-plan at 065c4335e2a23838cebed51417bb2fb0429007bc into LeanPool.PoincareGeometry.

The import retains 778 production and required source modules in 806 destination files, including the independent curvature developments and contracted-Bianchi bridge. It covers curvature and Levi–Civita connections, Bianchi identities, Hamilton–Ivey reaction estimates, Bonnet–Myers, Schur rigidity, almost-Schur, Lichnerowicz–Obata, scalar comparison, and symmetric tensor heat infrastructure. The upstream roadmap remains incomplete; this PR does not claim a proof of the Poincaré conjecture.

This PR is in progress. Published head f02d706a4cf43c986bab0c62dda5e204cee93b93 uses Lean v4.35.0-rc3 and the project-root index migration: LeanPool.lean is a compact 258-line aggregate root, and LeanPool/PoincareGeometry/Imports.lean lists the project modules. The former 10,800-line flat-root size blocker is resolved at this head. Project proof sources at this head match the locally tested a603644585116e29976fff6513338b87502672aa; subsequent proof repairs remain local and unpushed.

The current-head sharded CI run has failing shards, so no complete build or lint pass is claimed. In a bounded local full project build after the RiemannianSection and MetricSegmentBoundary repairs, there were 85 Lean source-error records across six modules and 9,258 warning records (9,092 unique sites). A guarded exact build of HamiltonIveyIntrinsicVariation then passed with zero Lean errors. Guarded SmoothRealization trials cleared its two earliest type mismatches, a dependent metavariable error, and four repeated instance and subtype-distance failures; 23 source errors remain in that scoped file, with no increase over its 2,291 baseline warning records. The next local trial targets four separate Picard Lipschitz fields. These proof repairs remain unpushed. The largest remaining source frontier includes Diffeomorph3FlowExistence, SmoothRealization, ConnectionLaplacianTraceFreezing, TensorHeatCoordinatePerturbation, and JointSpatialMVFDeriv. The raw-to-strong Diffeomorph3 conversion also has a genuine missing variational-data hypothesis, which needs a statement-preserving mathematical repair.

A prior scoped static audit found 88 remaining findings across 806 files, including broad imports and oversized files or proofs. No checks, gates, compiler budgets, waivers, or repository settings have been weakened. Please leave this PR unmerged.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

Changes requested by automated review

Reviewed exact head b1d964faa566393afca88f53347c72181497f091. This draft cannot advance to merge until the concrete CI blocker below is repaired and complete protected CI is green.

The exact-head Build pool run fails in the imported PoincareGeometry closure: deterministic heartbeat timeouts, unsolved goals, rewrite/type mismatches, and kernel unknown constants are reported in ConnectionLaplacianTraceFreezing.lean, StandardDeTurckDerivativeExpansion.lean, Diffeomorph3FlowExistence.lean, and AnalyticPDE/SmoothRealization.lean. Documentation also fails because the project does not build.

Acceptance: repair the proof-bearing closure, rerun generated-index, full pool build, warning scan, linters, quality/trust audit, and documentation at the new head. Do not change repository policy or add waivers.

[Vilin97]

/review

[greptile-apps]

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

[Low risk] Adds mathematical proofs in Lean for differential geometry.

Keep this PR unmerged while the earlier broad-import requirement and radial-proof finding remain outstanding.

Findings

1.  Referenced change record is missing ▶
2.  Parallel curvature interfaces ▶
3.  Broad Mathlib import ▶
4.  Radial rewrites block compilation ▶
5.  Unused premise limits reuse ▶

Summary

Imports Riemannian geometry and analysis toward Ricci flow, with Hamilton–Ivey reaction estimates as the catalog’s main results.

• The current Hamilton–Ivey descriptions match their formal statements.
• The imported curvature files refer to an extraction record that was not retained.
• Vilin97 acknowledges failing builds, the unfinished roadmap, and missing variational data, and requests that the PR remain unmerged.
• A complete source-by-source audit, external license and source verification, repository-wide novelty comparison, and current-head compile-cost assessment remain unverified. The full diff contains 495,012 added lines; only selected modules received detailed inspection.

_{Reviews (3) · Last reviewed commit: "Merge current main and migrate PR #512 t..." · Reviewed by Greptile}

[greptile-apps]

Parallel curvature interfaces

This pipeline defines its own curvature, Ricci, scalar-curvature, and metric-compatibility concepts even though the central CovariantDerivative API already provides them. The conversion lemmas at lines 100–120 are private and require custom extension hypotheses. The Ricci-scalar comparison and tensor-heat pipelines repeat this pattern, so downstream code cannot directly share central curvature and Levi–Civita results, and future API or convention changes must be repaired across several interfaces. This is non-blocking, but these pipelines should use the central abstractions or expose one reusable set of equivalence lemmas.

Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!

[Vilin97]

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

Reviewed head: 26a1121e5267d35d8cf9fbde0607c82e9ba1f191

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

Rubric	Verdict	Bottom line
Faithfulness	🛑 block	The Hamilton–Ivey headlines need to disclose the scalar-barrier assumption and the restriction to intervals with strictly negative least eigenvalue.
Novelty	✅ pass	Searches of the pinned Mathlib revision and existing pool sources found no duplicate of either Hamilton–Ivey headline.
Significance	✅ pass	The named comparison, rigidity, and pinching results provide substantial mathematical endpoints and meet the pool’s significance bar.
Sources	✅ pass	Both headline statements match the pinned upstream source, the ODE scope is explicitly labelled, and prior formalizations are credited.
Code quality (advisory)	🤔 discuss	A maintainer should weigh the duplicated curvature implementations and unnecessary helper hypotheses before merging.

Aspect	Value
Proves the claim	🟡 weaker_than_claimed
Assumed, not proved	The reaction theorem assumes K > 0, t ≥ 0, ordered eigenvalues, ν < 0, and R ≥ −3K/(1+Kt). The ODE theorem assumes the reaction equations and eigenvalue ordering and strict negativity throughout [0,T], together with ν(0) ≥ −K; it derives the scalar barrier internally. The card does not disclose the scalar-barrier or whole-interval negativity restrictions.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	research
Branch	Riemannian geometry and geometric analysis
Mode	theory_building
Code quality	3 / 5

Statement check: The Lean proves pointwise coercivity under a scalar lower barrier and ODE pinching for ordered solutions whose least eigenvalue remains strictly negative throughout the interval.

The development establishes Bonnet–Myers, Lichnerowicz–Obata, almost-Schur with equality rigidity, and Hamilton–Ivey reaction-ODE pinching, supported by substantial curvature and analytic theory.

Faithfulness findings (1)

• undisclosed-hypothesis — LeanPool/projects.yml:9980
  Both headlines omit restrictions present in their declarations. In particular, ‘under the stated initial bounds’ does not disclose that the ODE theorem requires ν(t) < 0 throughout [0,T]; its signature cannot be applied across a zero crossing merely from the initial lower bound. The pointwise coercivity theorem also takes the scalar lower barrier as an input. State that the reaction estimate assumes R ≥ −3K/(1+Kt), and that ODE preservation is proved for ordered solutions on intervals where the least eigenvalue stays strictly negative.
  Evidence: LeanPool/PoincareGeometry/HamiltonIveyReaction/Reaction.lean:299–307: theorem hamiltonIvey_reaction_coercive {K t lambda mu nu : ℝ} (hK : 0 < K) (ht : 0 ≤ t) (hlm : mu ≤ lambda) (hmn : nu ≤ mu) (hnu : nu < 0) (hscalar : -3 * (K / (1 + K * t)) ≤ scalar lambda mu nu) (hdefect : defect K t lambda mu nu < 0) : K / (1 + K * t) < -nu ∧ -nu / 9 ≤ reaction K t lambda mu nu ∧ 0 < reaction K t lambda mu nu. In hamiltonIvey_ode_pinching, lines 573–578 require (hlm : ∀ t ∈ Set.Icc 0 T, mu t ≤ lambda t) (hmn : ∀ t ∈ Set.Icc 0 T, nu t ≤ mu t) (hnuNeg : ∀ t ∈ Set.Icc 0 T, nu t < 0) (hT : 0 ≤ T) (hnuLower : -K ≤ nu 0) : ∀ t ∈ Set.Icc 0 T, 0 ≤ defect K t (lambda t) (mu t) (nu t).

Code quality findings (2)

• duplicate-definition — LeanPool/PoincareGeometry/AlmostSchur/CurvatureVendor/Tensor.lean:89
  The CurvatureVendor subtree maintains a second implementation of the central curvature library: Along, Raw, Tensor, Bianchi, Contractions, ContractedBianchi and ContractedBianchiBridge repeat definitions and proofs, often with only an AlmostSchur suffix. ContractedBianchiSections.lean also repeats the central bridge's regularity and symmetry proofs under additional names. These copies multiply the work needed for Mathlib upgrades and allow the interfaces to diverge. Extract shared foundations and retain compatibility names through aliases or forwarding lemmas instead of independent proof bodies.
  Evidence: AlmostSchur/CurvatureVendor/Tensor.lean:89 declares lemma contMDiffOn_extend_baseSet_twoAlmostSchur {x : M} (v : V x) :; PoincareCurvature/Geometry/Manifold/VectorBundle/CovariantDerivative/Curvature/Tensor.lean:82 declares lemma contMDiffOn_extend_baseSet_two {x : M} (v : V x) :. Both continue identically:
  ContMDiffOn I (I.prod 𝓘(ℝ, F)) 2 (T% (extend F v)) (trivializationAt F V x).baseSet := by
  let t := trivializationAt F V x
  suffices ContMDiffOn I 𝓘(ℝ, F) 2 (fun y ↦ (t ⟨y, extend F v y⟩).2) t.baseSet by
  intro y hy
  rw [t.contMDiffWithinAt_section _ hy]
  exact this y hy
  let w : F := (t ⟨x, v⟩).2
  have hw : ContMDiffOn I 𝓘(ℝ, F) 2 (fun _y ↦ w) t.baseSet := contMDiffOn_const
  exact hw.congr (fun y hy ↦ by simp [extend, t, w, hy])

ContractedBianchiSections.lean:105 declares theorem curvatureCovariantDerivativeInner_firstPairSkew_sectionBridge; the central Curvature/ContractedBianchiBridge.lean:156 declares theorem curvatureCovariantDerivativeInner_firstPairSkew. Both repeat this statement and proof:
(x : M) (p a b c d : TangentSpace I x) :
curvatureCovariantDerivativeInner cov x p a b c d =
-curvatureCovariantDerivativeInner cov x p b a c d := by
have h := secondBianchiAux_swap_curvature_slots cov x
(X := smoothExtend (I := I) (F := E) (V := TangentSpace I) x p)
(smoothExtend_contMDiff_two (I := I) (F := E) (V := TangentSpace I) x a)
(smoothExtend_contMDiff_two (I := I) (F := E) (V := TangentSpace I) x b)
(smoothExtend_contMDiff_three (I := I) (E := E) (M := M) x c)
simpa only [curvatureCovariantDerivativeInner, curvatureCovariantDerivative,
inner_neg_left] using congrArg (fun z : TangentSpace I x ↦ inner ℝ z d) h

• unused-hypothesis — LeanPool/PoincareGeometry/PoincareCurvature/Geometry/Manifold/RicciFlow/AnalyticPDE/HeatKernel1D.lean:4434
  Several public helpers require hypotheses their proofs do not use. second_order_fixedPoint_bound needs neither the sign/time bounds nor contractivity of S0; contraction_iterate_bound (3655) does not use hθ1, hd0 or hd; cauchySeq_of_geometric_real (3675) does not use hC or hr0. These requirements restrict reuse and make callers thread irrelevant proof arguments, as the calls to contraction_iterate_bound already do. Remove the unused parameters from the helpers and their callers.
  Evidence: lemma second_order_fixedPoint_bound (β : BoundedContinuousFunction ℝ ℝ) {M t : ℝ}
  (hM : 0 ≤ M) (ht : 0 < t) (hsmall : M < t)
  (S0 : BoundedContinuousFunction ℝ ℝ → BoundedContinuousFunction ℝ ℝ)
  (hS0 : ∀ w w' : BoundedContinuousFunction ℝ ℝ, ∀ x, |S0 w x - S0 w' x| ≤ (M / t) * dist w w')
  (z : BoundedContinuousFunction ℝ ℝ) (hz : β + S0 z = z) (x : ℝ) :
  |z x| ≤ |β x| + |S0 z x| := by
  have hx : z x = (β + S0 z) x := by rw [hz]
  rw [hx, BoundedContinuousFunction.add_apply]
  exact abs_add_le _ _

lemma contraction_iterate_bound {θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ < 1) (d0 : ℝ) (hd0 : 0 ≤ d0)
(n : ℕ) (d : ℕ → ℝ) (hd : ∀ k, 0 ≤ d k) (h0 : d 0 ≤ d0)
(hstep : ∀ k, d (k + 1) ≤ θ * d k) :
d n ≤ θ ^ n * d0 := by
induction n with
| zero => simpa using h0
| succ m ih =>
calc d (m + 1) ≤ θ * d m := hstep m
_ ≤ θ * (θ ^ m * d0) := mul_le_mul_of_nonneg_left ih hθ0
_ = θ ^ (m + 1) * d0 := by rw [pow_succ]; ring

lemma cauchySeq_of_geometric_real (f : ℕ → ℝ) (C r : ℝ) (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r < 1)
(hstep : ∀ n, |f n - f (n + 1)| ≤ C * r ^ n) : CauchySeq f := by
apply cauchySeq_of_le_geometric r C hr1
intro n
rw [Real.dist_eq]
exact hstep n

---

Tokens: 4,116,611 in / 42,776 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $85.5404 (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.

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

[greptile-apps]

Broad Mathlib import

This content module uses public import Mathlib, but the repository quality rule forbids broad import Mathlib in content files. The quality checker explicitly matches both ordinary and public imports, so this requirement must be satisfied before merging. Replace it with the specific Mathlib modules needed here. The same violation appears in LeanPool/PoincareGeometry/LichnerowiczObata/GeometryStatements.lean:15 and LeanPool/PoincareGeometry/LichnerowiczObata/ClosedStatement.lean:15.

File Used: .github/CODE_QUALITY.md (source)

[Vilin97]

Changes requested by automated review

Reviewed exact current head f94fac6abc4905d630c2ae5be197248994ee18d8. The PoincareGeometry closure still has deterministic heartbeat timeouts, unsolved goals, rewrite/type mismatches, and unknown constants. Repair the proof-bearing closure and keep the card’s scalar-barrier and interval-wide strict-negativity hypotheses explicit, then rerun all protected gates.

[greptile-apps]

Unused premise limits reuse

exists_short_symmetric_tensorHeat_wellPosed requires _hLevi : cov.IsLeviCivita, but its proof never uses that premise. The underlying existence theorem and the symmetry argument work without it. Callers must therefore prove a stronger condition than the result needs. Remove the premise, or expose the general theorem and keep this version as a specialized wrapper.

[greptile-apps]

Referenced change record is missing

The copied curvature files direct readers to PROVENANCE.json for their exact extraction and local changes, but that record was not retained. The pinned source paths and blob IDs identify the originals, but maintainers cannot follow the promised explanation of how these copies differ. The same reference appears in Raw.lean and Contractions.lean.

This is non-blocking documentation feedback. Preserve the explanation in permitted source comments, or replace the reference with an available, pinned location.

Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!