WIP: Import Davis–Kahan rotation of eigenvectors

[Vilin97]

Imports aiq-kitware/aiq-davis-kahan-1970-rotation-eigenvectgors-perturbation-formalization at 38e37da6e147cd0016da1eb05987c3edf7d95b39 into LeanPool.DavisKahan.

Formalizes the sin-Theta, tan-Theta, sin-two-Theta, and tan-two-Theta theorem families from Section 2 of Davis and Kahan (1970), for real or complex separable Hilbert spaces, including common-domain unbounded operators and symmetric-norm estimates.

All 954 production and required source modules remain included, with 1,079 destination files. Supporting spectral, path-continuity, reflection and invariant-plane proofs are factored without weakening their statements. The public summary retains the Ritz-residual orthogonality premise.

Work remains in progress; the existing PR lifecycle is preserved. No checks, gates, compiler budgets or repository settings have been weakened.

• Before module migration, full build28 passed all 4,965 jobs and declaration linter14 passed.
• Current scoped header, forbidden-text, file-size and proof-size checks pass across all 1,079 files.
• Module migration and four public-interface compatibility repairs are checkpointed. The interrupted full31 run does not validate the current head; a fresh bounded build, remaining style cleanup, lint and compiled audit remain.

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 56b3f8645aa369964b3a00eded0585e9e116e77f. The exact-head Build pool gate fails its zero-warning scan. The Davis–Kahan import emits hundreds of line-length, deprecated-API, formatting, and style warnings across the changed closure, including CanonicalRealView.lean, AbstractSpectrum.lean, TanTwoThetaReflectionAmbient.lean, and source Section 2/8 modules. Repair the warnings rather than suppressing them, then rerun complete protected CI at the new head.

[Vilin97]

{
"reviewed_head": "77343db09bc8f4f201cc0be54fcfbe5a3901e121",
"review_scope": "Tan-Theta headline faithfulness only.",
"assessment": "The registry summary, tanTheta informal statement, and theorem docstring now explicitly require Rayleigh–Ritz trial data whose residual is orthogonal to the trial subspace. The statement also identifies the positive directed gap between the trial compression and unwanted reducing block, and the finite residual symmetric-norm premise. This matches tanTheta and the residual_orthogonal field of RitzData; no theorem type or proof changed.",
"remaining_work": "The importer has a separate active module-system/proof-port checkpoint. Full current-head build, linters, quality/axiom/environment audits, remaining maintenance findings, and final integration review remain pending. This repairs the identified hidden-hypothesis description; it is not full merge approval.",
"validation": "Executable Lean text is unchanged; scoped registry/card checks passed. Lossless current-main integration preserves all 218 cards from 99afd29 and adds only this project. Importer worktrees were not modified.",
"merge_approval": false
}

[Vilin97]

Regenerated LeanPool.lean at 832020448b2284dd8ad03e1331302949d8846e4e to resolve the documentation-preflight and build index failures. The index adds all 1078 omitted DavisKahan module imports; every prior import is preserved and mathematical sources are unchanged. The actual generator now passes mk_all --module --check in this checkout. My earlier index-pass claim was incorrect; this check exposed the omission. The separate source-scope review remains valid, but this is not a full build or final acceptance; the ongoing module port and fresh CI still need to pass.

[greptile-apps]

Internal Helpers Become Public

Removing private from positiveEigenspaceBasis and positiveEigenspaceVector exposes choice-based helpers that are used only in this file. The same change exposes zeroExtensionProd. These implementation details now form part of the API available through the project entry point, so downstream code may come to depend on them and make future refactoring harder. Keep them internal if the module conversion permits it.

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]

Reviewed the incoming source changes from 832020448b2284dd8ad03e1331302949d8846e4e through 2ed17a06577919adab33a684ebb7e575efd0f486. The branch advanced to 2a400c2a07ce7e546b98353017d660d9df644a91 during final verification; this review does not cover that subsequent delta.

The module migration and bounded proof repairs preserve the inspected mathematical contracts. The textual audit retains all 11,939 existing named declaration headers and all 1,079 project files. The two new private helpers isolate cyclic-subspace invariance and restriction of a bounded inverse to the spectral range; their specializations retain the original hypotheses, domain transports, projection identity, and inverse sign. The other substantive changes expose existing interfaces, supply completeness from finite dimensionality and a zero rank-bounded approximation witness, or make existing proof arguments explicit. No weakened endpoint or changed operator construction was found.

At the audited head, the corrected Rayleigh–Ritz residual-orthogonality card is unchanged in value and literal text, and all 1,079 DavisKahan imports in the root index are retained. The repository's unchanged header, forbidden-text, file-size, and proof-size routines pass on these project files; the scoped whitespace check also passes. No local compiler, declaration linter, or compiled trust audit was run for this review.

Leave this PR unmerged. Fresh validation of the module port remains pending. The earlier maintenance findings also remain in the inspected source: the exported exploration probes, duplicated complex/scalar beam development, repeated tangent inverse/projection helpers, and unused helper premises. This review accepts the inspected incoming source delta, not the whole import or its final build status.

[Vilin97]

Changes requested by automated review

Reviewed 7fbcdb57ba5e219095103d711af0aa5252c860d8. The spectral-subspace perturbation and beam applications are significant; green kernel/trust evidence is still required for the claimed imported endpoints.

Blocking finding: ForTauCeti/Analysis/InnerProductSpace/DoubleAngle/SpectralCutoff.lean:126 cannot resolve abs_le_of_mem_Icc_neg; DavisKahan/SpectralTheory/BoundedTruncation.lean:64 cannot resolve abs_le_max_zero_of_mem_Icc and then has type mismatches/timeouts; Specialized/FreeBeam/BeamFormSpace.lean:424 lacks Polynomial.hasDerivAt. Restore precise imports/namespace references and update the truncation callers, then rebuild the entire affected dependency closure without raising limits.

Evidence: exact-head build log. Acceptance condition: the complete project, repository quality/axiom gates and required protected checks pass on the repaired head, and the remaining substantive/maintainability findings are resolved. The prior bot verdict does not override these reproduced source/build failures.

[Vilin97]

Changes requested by automated review

Reconciled to exact current head 4e9299d1c8c37291cd9219cb7e157393897db72d. 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 spectral-cutoff absolute-value helpers and polynomial derivative dependency remain unavailable at the reported uses.

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]

{
"reviewed_head": "d50ab87c87215ea4c8a02cd4781f415962e33992",
"verdict": "request_changes",
"scope": "Focused compiler-maintenance follow-up. This does not replace the prior mathematical/source reviews or remove the existing request to leave this PR unmerged.",
"changes": [
"Keep the spectralCutoff and spectraBoundedTruncation interval-bound helpers private by supplying the same proofs through explicit by exact boundaries; fix the latter bound explicitly as max 0 τ.",
"Make only the existing crossT computational operator public because it appears in two public theorem types; its formula and those theorem statements are unchanged.",
"Import Mathlib.Analysis.Calculus.Deriv.Polynomial in both beam form-space modules that use Polynomial.hasDerivAt.",
"Specify b := mv in mbasis to fix the intended basis family while preserving its original proof boundary and data."
],
"source_evidence": {
"baseline": "c1dcd2689f92c2d2b572f9bc183a1e8fc089b317",
"diff": "Six files, 7 insertions and 5 deletions; all 219 existing explicit declaration headers remain unchanged. Only crossT changes visibility. No declaration, module, card, index, setting, or gate is removed.",
"peer": "The complete patch and failing contexts were independently source-reviewed against the pinned Lean proof-export implementation and Mathlib basis/derivative interfaces."
},
"validation": {
"passed": "Scoped header, forbidden-text, file-size and proof-size checks have zero findings; git diff --check passes. Exact patch and unchanged card/index/configuration guards passed before the normal fast-forward push.",
"not_run": "No local compiler, module linter, native index check, or axiom audit was run for this patch.",
"cache_feasibility": "The six-target dependency closure has 165 project modules. Of its 159 prerequisites, 35 have legacy/incomplete artifact sets, including 6 of the 11 direct prerequisites. The read-only census did not certify native source/output hashes, so it does not establish a reusable compiled closure."
},
"limits": "The failed Build pool run 36226510279/job 108361597438 belongs to baseline c1dcd26, not this new head. This patch targets its concrete root diagnostics; secondary rewrite, missing-derived-declaration and timeout errors may be cascades, but their resolution remains untested. Fresh current-head CI and the existing remaining import work are still required; this is not full acceptance.",
"findings": [
{
"status": "pending_validation",
"evidence": "The recorded baseline contains 30 diagnostic headers across the six repaired modules. Source inspection supports these narrow repairs, but no fresh compiler result establishes that all diagnostics are resolved."
}
]
}

[Vilin97]

{
"reviewed_commit": "1ecc96e5dc4cf6f7eddee91f2b6a202b308040c3",
"conclusion": "Focused source/static repair accepted; current compilation and full acceptance remain pending. Keep the existing leave-unmerged hold.",
"scope": {
"baseline": "d50ab87c87215ea4c8a02cd4781f415962e33992",
"files": 3,
"change": "Six changed lines addressing the primary causes of 17 current CI diagnostics across three failed modules. No new five-rubric/full-project approval is claimed."
},
"repairs": [
{
"declarations": [
"TauCeti.liftProj",
"TauCeti.DavisKahan.TanTheta.UnboundedCompressionTrialData.subspaceOut",
"TauCeti.DavisKahan.TanTheta.UnboundedCompressionTrialData.compressionDomainOut"
],
"change": "Export the exact existing data helpers required by exposed cutoff/transport definitions and the public scalarTransport_action type. Their types, arguments, operator/coordinate formulas and bodies are unchanged; these are three additions to the public API."
},
{
"declaration": "TauCeti.spectralBandCutoff",
"change": "Wrap only the existing mem_domain proof in an explicit by/exact boundary. The private interval-bound lemma and the spectral projection are unchanged."
},
{
"declaration": "TauCeti.instCompleteSpaceFiniteSource",
"change": "Give the existing local CompleteSpace E instance an explicit name, retaining its exact FiniteDimensional.complete construction, type and local scope. This removes the generated TauCeti.instCompleteSpace_leanPool collision with Polar.CFCBridge. No textual consumer of the old generated name occurs in the project."
}
],
"validation": {
"source": "Complete patch and relevant definition/proof contexts independently reviewed by two additional reviewers. Exact transformation replay establishes that all other bytes in the three files are unchanged.",
"static": "The existing header, forbidden-text, file-size and proof-size gates pass on all three changed modules. All 1,079 project paths remain; the other 1,076 project files, registry/card, root index/umbrella, imports and configurations are byte-identical to the reviewed baseline. Own generated card matches the registry.",
"compiled": "No local compilation, native style/linter, generator or compiled-trust run was performed. Prior cache feasibility contains uncertified legacy dependencies, so no broad rebuild was started. The expected disappearance of secondary diagnostics remains unverified until fresh CI.",
"current_failure_evidence": "https://github.com/Vilin97/lean-pool/actions/runs/36228984481/job/108368398538",
"remaining": "Fresh compilation must confirm these primary repairs and their cascades; existing project warnings, full lint/compiled-trust checks and exact-head required CI remain pending."
},
"lifecycle": "The PR body continues to say Please leave this PR unmerged. No merge, main refresh, CI retry/cancellation or gate change was performed."
}

[Vilin97]

{
"reviewed_commit": "42d70a26c1e6cb7208d7b0658f8fc0720aca61be",
"conclusion": "Focused source/static repair accepted; fresh compilation and full acceptance remain pending. Preserve the existing leave-unmerged hold.",
"scope": {
"baseline": "1ecc96e5dc4cf6f7eddee91f2b6a202b308040c3",
"files": [
"LeanPool/DavisKahan/DavisKahan/Explorations/SourceUnitaryInvariantNormFanDominance.lean"
],
"change": "Two primary source repairs for the 26 current CI errors in this exploration module: 24 missing completeness instances, one later failed-declaration cascade, and one private proof exposure. No new five-rubric or full-project approval is claimed."
},
"repairs": [
{
"declaration": "instCompleteSpaceFiniteFanDominance",
"change": "Add one explicitly named local CompleteSpace instance derived from FiniteDimensional.complete ℂ E. All 24 failing sites already have normed complex inner-product and FiniteDimensional ℂ assumptions; the same polymorphic instance covers E and F. No caller premise or globally registered instance is added. The existing gauge, membership, seminorm and finite-dimensional Fan-dominance statements and proofs are textually unchanged.",
"primary_api": "https://github.com/leanprover-community/mathlib4/blob/5ed2965256430c3649e86755f9576b54eca72435/Mathlib/Topology/Algebra/Module/FiniteDimension.lean#L500-L513"
},
{
"declaration": "fanCounterexampleA",
"change": "Put the existing private fanCounterexampleCoeff_le_one argument inside an explicit by/exact proof boundary. The private theorem, geometric coefficients, bound K=1 and diagonal operator data remain unchanged. The later unknown finiteDimensional_fanDominance name is a cascade from the failed declaration earlier in this same file; no import or theorem rename was made.",
"primary_api": "https://github.com/leanprover/lean4/blob/v4.34.0/src/Lean/Elab/SyntheticMVars.lean#L474-L489"
}
],
"validation": {
"source": "Complete patch, all seven affected declaration interfaces, existing coefficient/diagonal definitions and pinned APIs independently source-reviewed by two additional reviewers. Exact inverse transformation restores every original byte, including all existing public headers.",
"static": "The existing header, forbidden-text, file-size and proof-size gates pass on the complete changed module. All 1,079 own paths remain; the other 1,078 project files, complete registry/card, root index/umbrella, imports and configurations are byte-identical. The generated own card matches the registry.",
"compiled": "No local compiler, native style/linter, generator or compiled-trust run was performed. Existing uncertified legacy-cache constraints were retained; no broad rebuild was started. Fresh CI must confirm both primary fixes and the expected disappearance of cascades.",
"baseline_ci": "https://github.com/Vilin97/lean-pool/actions/runs/36232846010/job/108379181289",
"remaining": "Please complete the remaining actual warning cleanup after the compiler repair and rerun all required exact-head checks. The baseline log has 334 emitted warning headers (288 distinct location/message tuples across 150 modules), including two elaboration-recovery sorry notices after failed declarations. Those notices do not establish source proof holes: the unchanged forbidden-text gate passes on this complete module, and this patch introduces no sorry/admit. Full compilation, warning-free build, linter and compiled-trust acceptance remain pending."
},
"lifecycle": "The body still says Please leave this PR unmerged. No merge, main refresh, CI queue operation, label, gate or reviewed-manifest change was made."
}