docs: record eigen2 verification and unresolved numerical contracts

This commit is contained in:
KOKO\Mimi
2026-09-09 03:16:08 +09:00
parent 22c9d4435c
commit 76192508fd
9 changed files with 467 additions and 3 deletions
@@ -0,0 +1,99 @@
# 수정 전 구현 수치 검토 기록
아래는 최초 검토 당시 관찰이다. 현재 판정·수정 상태는 [현재 보고서](implementation-numerical-review.md)를 따른다.
# 구현 독립 수치 검토
- Feature: `mitc4-shell-feast-eigen2`; Owner: `numerical-review-agent`.
- 검토일: `2026-09-09`; 대상: 질량·선형 stabilization·constraint-first reduction의 현재 작업본.
- 판정: **correction-required / verification-incomplete**. 최초 질량/축소 검토에 이어 메인의 추가 할당으로 FEAST backend를 검토했다. Procedure는 메인이 수정 중이므로 검토하지 않았다.
- 기준: [formulation](formulation.md), [mass/stabilization](formulation-mass-stabilization.md), [eigen](formulation-eigen.md), [controls](numerical-review-controls.md), [cases](numerical-review-cases.md), [requirements](requirements.md), [공통 tolerance](../TOLERANCE.md).
## 수정 사항
### NR-IMP-01 — P2: 질량 양성 검사가 불필요한 곱의 범위에 의존한다
[mitc4_shell.cpp](../../src/fesa/elements/mitc4_shell.cpp) 819–824행은
`m*j-h*h`의 finite/positive 여부를 검사한다. 채택 C2-09의 검사는
`j-h²/m>0`이며, 전자는 유한하고 잘 조건화된 질량도 density 배율만으로 거부한다.
평판 `A=4,t=2,h=0`에서 `m=2*rho,j=(2/3)*rho`다.
| rho | m*j의 binary64 결과 | j-(h/m)*h | 현재 guard |
| ---: | ---: | ---: | --- |
| 1 | 1.3333333333333333 | 0.6666666666666666 | true |
| 1e-180 | 0 | 6.666666666666667e-181 | false |
| 1e180 | inf | 6.666666666666666e179 | false |
이는 Python 표준 `float`/`math.isfinite`로 실제 계산한 scalar 반례이며 C++ solver 재현은 미실행이다.
모든 사례의 `m,j`와 nodal block 성분은 finite positive이고 density 배율은 condition number를 바꾸지 않는다.
**수정:** 승인된 Schur variance를 불필요한 `m*j`, `h*h` 중간 곱 없이 평가하고 strict finite/positive 판정은 유지한다.
두 배율의 element mass 회귀로 실패를 재현하고, 정상 mass의 density 비례 및 잘못된 variance의 거부를 확인한다.
근거: M4/M5, C1 및 C2-09, 요구 003/014/026. 허용오차·rank·density 계약 변경은 필요하지 않다.
### NR-IMP-02 — P2: 새 oracle/covariance 검사가 승인된 metric을 사용하지 않는다
[mitc4_shell_test.cpp](../../tests/unit/elements/mitc4_shell_test.cpp) 837–845, 901, 922–937행은
차원이 다른 `C0/C1/C2` 및 translation/rotation matrix entries에 동일한 absolute `1e-12`를 적용한다.
특히 `ExpectGlobalZCovariance`는 `D^T M D`, `D^T K D`와 상대 Frobenius 지표를 계산하지 않는다.
이 검사는 현재 fixture의 entry 오차를 확인하지만 C1/C2-02/03의 통과 evidence를 대신할 수 없다.
**수정:** scalar Ck 오차는 `m_e(t/2)^k`, matrix congruence는 같은 `ell`의 D congruence 후
`norm(R-S)/(norm(R)+norm(S))`로 검사한다. Finite-first와 승인된 zero branch를 유지한다.
단위변환 E2-C20을 함께 연결하여 고정 절대 단위에 의존하지 않음을 확인한다.
## FEAST 추가 검토: 수정 사항
대상은 [mkl_feast_eigen_solver.cpp](../../src/fesa/solvers/eigen/mkl_feast_eigen_solver.cpp)의
2026-09-09 추가 할당 시점 작업본이다. 아래 행 번호는 후속 수정 전이며 기준은 C1/C3/C5/C6다.
| Finding | 위치·영향 | 필요한 수정·검증 |
| --- | --- | --- |
| NR-IMP-03 **P1** | 420–425행은 optional count의 **모든** 오류를 fallback으로 처리한다. Invalid/SPD/inner-solver 오류도 이후 solve 성공으로 우회될 수 있다. | `info=1,2,3,-5`만 optional search 종료로 분류하고 나머지는 즉시 실패. E2-C21 status 주입으로 각각 확인 |
| NR-IMP-04 **P1** | 429–433행은 세 guard의 서로 다른 successful count를 모두 fatal로 처리한다. Spectrum이 guard 사이에 있으면 정상적인 nondecreasing count 차이이며 endpoint collision이다. 반대로 서로 다른 interval들의 global monotonicity는 검사하지 않는다. | C5의 후보 `0,+1,-1,+2,-2,+4,-4` times delta 최대7개와 certified fallback을 구현. Successful count가 interval 포함관계에 모순될 때만 count-inconsistent. 정상 collision과 실제 역전 mock을 구분 |
| NR-IMP-05 **P1** | 451–457행의 final interior endpoint 검사는 central count 한 번뿐이다. 500–505행의 retry는 같은 b에서 capacity만 늘리며 재count하지 않는다. 542–546행의 endpoint separation 실패는 retry 경로에 들어가지 않는다. | Final interior b의 세 guard 재확인, 저장된 더 큰 certified b 선택→재count→capacity 갱신을 solve retry와 endpoint 실패에 연결. 최종 b0 및 변경 없는 입력 재호출 금지·3회/budget 한계 확인 |
| NR-IMP-06 **P2** | 360–365행은 초기 retry 때 Gershgorin padding 대신 전체 bracket 폭을 2^j배 한다. 불필요하게 넓어진 contour는 승인된 controls와 다른 수렴 동작을 만든다. | 원 gL/gU를 보존하고 **16delta padding만** 2^j배로 outward 재계산. Zero B의 ±2^j branch는 현재 정의와 일치 |
| NR-IMP-07 **P2** | 175–219행의 QR은 reflector norm의 absolute 1e-12만 검사하고 relative pivot, positive R diagonal, post-QR Gram 검사를 수행하지 않는다. | C6의 원 column scale 대비 pivot·positive R sign·Gram<=1e-12를 실제 계산. Fixed seed/n,m0별 재현성과 부적합 QR 실패 검증 |
| NR-IMP-08 **P1** | 236–238/312/459–473행은 일부 size_t product만 검사한다. n²/nm0의 byte·PTRDIFF_MAX·container max_size와 count padding arithmetic 사전검사가 없고 allocation exception 변환도 이 함수에 없다. | 모든 integer/byte operation 전에 C6 범위 검사, allocation/length 오류의 structured failure 경로를 연결. 불가능한 count m0도 cast 전 `0<=m0<=n` 검증(338–344행). E2-C22의 boundary/실패 주입 |
| NR-IMP-09 **P2** | 513–535행은 finite 검사 전에 eigenvalues를 sort한다. 565행은 physical lambda 환산의 finite/비영 underflow 검사를 하지 않는다. 492–495행은 epsout을 무조건 available로 기록하고 finite 검사하지 않는다. 571–579행은 Gram 최대 entry만 계산한다. | Raw eigenpairs finite-first 후 sort, `mu*s` overflow/비영→0 실패, epsout finite 검증, 전체 c의 `norm(G-I)F/sqrt(c)`와 pairwise 기준을 별도 적용. Public 결과의 gram_error 의미를 승인된 schema에 맞춤 |
추가 관찰: `ValidateSymmetry` 118–143행의 max-entry 기준도 C2-01의 Frobenius 지표와 다르다.
Failure 반환은 local `calls`를 버리므로 실패/fallback 이력을 상위 diagnostic/log에 남기는 연결을 확인해야 한다.
현재 [backend tests](../../tests/unit/solvers/eigen/mkl_feast_eigen_solver_test.cpp)는 actual n1/zero/repeated/prefix/negative/thread/request를 다루지만,
위 C5 status·collision·monotonicity·final guard·retry·512 call budget·overflow failure injection은 확인되지 않았다.
Backend를 이 검토에서 실행하지 않았으며 actual FEAST의 성공 또는 실패를 새로 주장하지 않는다.
## 정적 대조에서 일치한 구현
| 경로·행 | 확인 내용 |
| --- | --- |
| [mitc4_shell.cpp](../../src/fesa/elements/mitc4_shell.cpp) 292–299, 725–805 | `S=-[d]cross`, 27점 xi→eta→zeta 적분, 각 점 geometry/J 검사, 대칭 Ck와 MC의 네 block 부호·DOF 순서가 M1/M3와 일치 |
| 같은 파일 808–850 | 보존된 Ck의 실제 row sum에서 m/h/j를 만들고 nodal tensor를 재구성한다. Full24 row sum 또는 인공 drilling mass를 사용하지 않음 |
| 같은 파일 649–716 | 초기 physical rotary 8개 전부의 trace mean, zero 포함 분모8, negative/nonfinite/allzero 거부 및 complete K 재조립이 S1과 일치 |
| [eigen_reduction.cpp](../../src/fesa/analysis/eigen_reduction.cpp) 65–112 | 실제 component BC를 먼저 적용하고 constrained director의 **정확한 비영** 성분으로 analytic null을 판정. Partial URZ의 양의 mass를 보존 |
| 같은 파일 116–200, 311–332, 359–370 | `Mp/scale`의 block Cholesky, small triangular inverse action으로 rcond_inf, `P L^-T` lift, nodal stiffness congruence 및 constrained-zero scaled mode 복원 방향이 E1–E4와 일치. Global dense inverse 없음 |
| 같은 파일 238–280, 289–349 | 원 scaled constrained MZ/KZ/PZ를 검사하고 null stiffness kappa의 strict positivity를 유지. `nz=0`의 storage0는 상위 I/O에서 N/A flag와 연결해야 함 |
## 아직 연결해야 하는 검증
다음은 할당된 [element tests](../../tests/unit/elements/mitc4_shell_test.cpp)와
[reduction tests](../../tests/unit/analysis/eigen_reduction_test.cpp)의 정적 coverage 확인이다.
다른 파일의 미확인 coverage를 전체 저장소의 부재로 단정하지 않는다.
- E2-C02/03/04/11: warped oracle는 현재 Ck(0,0) 및 전체 scalar sums만 확인한다.
모든 Ck/row, `sum(m_i X_i+h_i d_i)`의 독립 first spatial moment, MC/ML 각각의 직접 kinetic energy,
Jensen pairwise integral·mesh 차이, consistent rank20·nodal rank5·drill null·여섯 physical rigid mass Gram이 필요하다.
- E2-C08/09/10: 원 S3 exact scalar target은 구현되어 있다. **회전한 같은 S3 fixture**의 실제 partial BC spectrum과
admissible tangent moment `(5/3)b`의 정적 응답·full residual covariance는 아직 이 두 파일에서 확인되지 않았다.
Zero 포함 rotary inventory와 독립 tangent basis, invalid inventory 경계도 별도 evidence가 필요하다.
- E2-C13/14/15/16: 현 reduction 3개 테스트는 URZ positive, full-free aligned null/Kpz 실패, p=1e-8 conditioning 실패를 다룬다.
p=1/2000 positive 성공과 p=0 exact null, 2개 free rotations, drill-only free/all-fixed node/global n0,
nonpositive kappa·MZ 위반, **비대각 Mp** `[[2,1],[1,2]]`의 lambda `2,10/3` 및 original-mass 복원 검증이 필요하다.
- E2-C06/12/20/26: 공유 node의 section별 stable assembly·재현성, frozen nonlinear scale/미분/rollback,
density와 단위변환, retained static·pressure synthetic evidence는 이번 할당 파일 범위 밖의 후속 연결 사항이다.
## 실행 경계와 잔여 위험
이번에는 문서·source·test를 읽고 scalar binary64 반례만 실행했다. Build/CTest·FEAST·external reference·physics 검증은 실행하지 않았다.
메인의 focused build/test 성공 전달은 별도 실행 evidence이며 본 검토가 전체 기능 완료를 승인하지 않는다.
Reference artifact와 제외 예제는 읽거나 수정하지 않았다. 상위 계약·source·test·Git도 수정하지 않았다.
남는 위험은 거의 정렬된 partial BC의 forward accuracy, geometry 평가점 밖 injectivity,
원 free residual·전체 c개 Gram을 포함한 procedure 복원 검증과 actual FEAST의 count/cluster/runtime다.