spectral: spectral theorem for real symmetric matrices#1611
Open
gbdrt wants to merge 7 commits into
Open
Conversation
`conjFieldType` is a `numFieldType` with an involutive conjugation `conj` (`|x| ^+ 2 = x * conj x`) and a square root of nonnegatives; `numClosedFieldType` and `rcfType` inherit it via HB factories. Adds `archimedean.v` join structures. Developed with the assistance of Claude Opus 4.8 (1M context) and Rocq-MCP (https://github.com/LLM4Rocq/rocq-mcp). Co-authored-by: Cyril Cohen <cyril.cohen@inria.fr>
Generalize the `conjC` `involutive_rmorphism` instance, `map_mxCK`, the dot-norm theory and `hermitian1mx` from `numClosedFieldType` to `conjFieldType`. Developed with the assistance of Claude Opus 4.8 (1M context) and Rocq-MCP (https://github.com/LLM4Rocq/rocq-mcp). Co-authored-by: Cyril Cohen <cyril.cohen@inria.fr>
Move `dotmx`, `unitarymx`, the orthogonal complement and `schmidt` to a new `Section ConjSpectral` over `conjFieldType`; the eigenvalue/spectral results stay over `numClosedFieldType` and reuse `schmidt` by subtyping. Statements unchanged. Developed with the assistance of Claude Opus 4.8 (1M context) and Rocq-MCP (https://github.com/LLM4Rocq/rocq-mcp). Co-authored-by: Cyril Cohen <cyril.cohen@inria.fr>
Define `realsubfield C`, the reals of a `numClosedFieldType` `C`, and equip it via subType factories with an `rcfType` structure; `realsubval` is the inclusion into `C`. Generalizes Abel's `algR`. Developed with the assistance of Claude Opus 4.8 (1M context) and Rocq-MCP (https://github.com/LLM4Rocq/rocq-mcp). Co-authored-by: Cyril Cohen <cyril.cohen@inria.fr>
`real_spectral_theorem` (over any `numClosedFieldType`, axiom-free): a real symmetric `A` is `invmx P *m diag_mx (spectral_diag A) *m P` for some real unitary `P`, via diagonalization over the real subfield (`schmidt_diag_real`). Developed with the assistance of Claude Opus 4.8 (1M context) and Rocq-MCP (https://github.com/LLM4Rocq/rocq-mcp). Co-authored-by: Cyril Cohen <cyril.cohen@inria.fr>
Developed with the assistance of Claude Opus 4.8 (1M context) and Rocq-MCP (https://github.com/LLM4Rocq/rocq-mcp). Co-authored-by: Cyril Cohen <cyril.cohen@inria.fr>
f6719f1 to
6c48901
Compare
- silence `HB.no-new-instance` on the intermediate `NumField_hasImaginary` and `RealField_hasPolyIvt` instances built by the `NumField_isImaginary` and `RealField_isClosed` factories - use `&` rather than `of` in the `HB.factory Record` and `HB.builders Context` headers (Rocq 9.2 syntax) - parenthesize `(x \is Num.real)` in `realsubpfactor` (Rocq 9.2 level-tolerance) - drop contributor names from the changelog entries Developed with the assistance of Claude Opus 4.8 (1M context) and Rocq-MCP (https://github.com/LLM4Rocq/rocq-mcp). Co-authored-by: Cyril Cohen <cyril.cohen@inria.fr>
6c48901 to
9b7ea63
Compare
Author
|
The remaining errors (building mathcomp-analysis) should be fixed with MCA PR#1987. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Motivation for this change
This PR proves the spectral theorem for real symmetric matrices over a numClosedFieldType (real_spectral_theorem): such a matrix is diagonalized by a real orthogonal matrix, with the same spectral diagonal as the existing (complex) spectral theorem.
To reuse Gram–Schmidt for this, it is generalized from numClosedFieldType to a new common ancestor conjFieldType of rcfType and numClosedFieldType — a numFieldType with an involutive conjugation conj such that
|x| ^+ 2 = x * conj xand a square root of nonnegatives. Existing interfaces are unchanged. As a building block, the PR also shows that the real subfield of a numClosedFieldType is an rcfType.Minimal TODO list
doc/changelog/make-entry.shSee this Checklist for details.
Automatic note to reviewers
Read this Checklist.