[Vilin97]

Split tubularProj_hasFDerivAt_starProjection into three private helper lemmas for the displacement bound, epsilon estimate, and chart derivative. Each helper is used once; existing public statements, hypotheses, and imports are preserved.

This addresses one of the eight Nesterov proofs in #723. The other seven proofs and the AndersonConjecture decomposition remain open.

Validation used Lean 4.35.0, the current Mathlib pin, and PR712’s unchanged semantic-linter plugin. The 200/201-line boundary control passed, the original full proof produced its 253-line warning, and the complete repaired module compiled without diagnostics with warnings treated as errors. Its Defs and IFT dependencies also passed. Normal PR CI remains pending.

[greptile-apps]

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

[Low impact] This proof-only refactor appears safe to merge.

Summary

Extracts three private helpers from tubularProj_hasFDerivAt_starProjection.

• The tubular projection proof now separates its three derivative steps.

_{Reviews (1) · Last reviewed commit: "refactor: split tubular projection deriv..." · Reviewed by Greptile}

[Vilin97]

Reviewed exact head a8c4100. Source review is favorable: the three private lemmas separate the existing displacement estimate, epsilon bound, and chart chain rule, and each has one caller. The byte-exact inverse check preserves all existing statements, hypotheses, imports, and surrounding code.

I independently validated the complete repaired module and its Defs/IFT dependencies with Lean 4.35.0, current project options, and warnings as errors. PR712’s unchanged semantic plugin was active: its 200/201-line control passed, the original full proof emitted the 253-line warning, and the corrected full module compiled with no diagnostics.

This addresses one Nesterov proof in #723. The other seven proofs and the AndersonConjecture decomposition remain requested. Protected PR CI and the current-head configured review remain separate integration requirements.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

Superseded by #757, whose independent favorable source review covers all eight Nesterov proof splits, including this same derivative file. Closing this overlapping alternative lets #757 integrate the repair together. The branch, exact-head review and completed targeted semantic-linter validation are retained. #757 still needs its own semantic-linter execution and protected CI; #723 remains open.