docs(hex8): record failed-entry equivalence evidence

This commit is contained in:
KOKO\Mimi
2026-10-09 06:05:09 +09:00
parent dcbf7bf8c0
commit 75e5cc3297
3 changed files with 38 additions and 15 deletions
+3 -2
View File
@@ -441,8 +441,9 @@ Local kernel과 입력·3N mapping은 독립 검토 및 연결 후 관련180개
native CTest exit0이며 독립 수치 검토를 통과했다. 두 정적 원본과442절점 고유치 원본은 native CTest exit0이며 독립 수치 검토를 통과했다. 두 정적 원본과442절점 고유치 원본은
직접 API로 실행했지만 원본 결과값 비교를 수행한 것은 아니다. 연결 source `28be39f`의 직접 API로 실행했지만 원본 결과값 비교를 수행한 것은 아니다. 연결 source `28be39f`의
전체 MSVC Debug build는 exit0이며 이 build 자체를 전체 CTest 통과로 해석하지 않는다. 전체 MSVC Debug build는 exit0이며 이 build 자체를 전체 CTest 통과로 해석하지 않는다.
HHT 내부 사례는 진행 중이다. 별도 구현 `b394ae7`의 관련75개 검사는 통과했으나, HHT 내부 사례는 진행 중이다. 별도 구현 `f661864`의 관련76개 검사와 독립 수치 검토는
두 동적 원본은 세 번째 증분의100회 제한에서 엄격 잔차 기준을 만족하지 못했다. 통과했고, 두 동적 원본의 새 실행은 진행 중이다. 이전 구현 `b394ae7`은 두 원본의
세 번째 증분100회 제한에서 엄격 잔차 기준을 만족하지 못했다.
동적 검증은 미완료이며 원인과 추가 검증은 [lessons](lessons.md)에 기록한다. 동적 검증은 미완료이며 원인과 추가 검증은 [lessons](lessons.md)에 기록한다.
공식 결과·외부 비교·최신 전체 회귀도 남아 있다. 공식 결과·외부 비교·최신 전체 회귀도 남아 있다.
원본 frequency 결과 부재는 구현 진행을 막지 않지만 기능 검증 완료를 막는다. 원본 frequency 결과 부재는 구현 진행을 막지 않지만 기능 검증 완료를 막는다.
+21 -4
View File
@@ -91,10 +91,27 @@ native build0/CTest8로 실패를 검출했다. 기존 수렴 기준·100회 제
상태로 복귀했다는 증거는 아니다. 비선형의 잔차 점수 왕복도 전체 상태 반복의 증거가 아니다. 상태로 복귀했다는 증거는 아니다. 비선형의 잔차 점수 왕복도 전체 상태 반복의 증거가 아니다.
Incoming correction4개의 실제 수치는 정상 Newton의 rates·tangent·rhs에 사용하지 않으며, Incoming correction4개의 실제 수치는 정상 Newton의 rates·tangent·rhs에 사용하지 않으며,
유한 값과 PASS 여부가 수용에 쓰인다. 숫자까지 같은 조건은 더 보수적이지만 이것이 유한 값과 PASS 여부가 수용에 쓰인다. 추가 계측에서 선형 진입20→다음23, 비선형72→80은
이번 원본 실패의 원인이라고 확정하지 않는다. 동일 순수 Newton 구간의 실제 전체 변위· 각각 같은 순수 Newton 구간의 전체1326개 변위·1275개 mask가 정확히 같았으나 correction
mask 일치와 correction 숫자 차이, 또는 ULP를 포함한 전체 상태의 재현을 별도 계측으로 숫자4개는 달랐다. 모두 finite/PASS이고 prospective physical FAIL이었으며 기존 판별은
확인해야 한다. 새로운 점수 heuristic이나 허용치 변경으로 이 증거를 대신하지 않는다. false였다. 선형 진입23→다음30은 실제 ULP 이동을 사이에 두고 변위·mask·correction
숫자까지 같았지만 history 초기화로 판별하지 못해 정상 Newton이 적용되는 경로였다.
독립 검토와 원시 배열 Python 검산 exit0으로 두 조건의 영향을 확인했다. 비선형에서
ULP를 사이에 둔 복귀는 입증하지 않았으며 전체 혼합 알고리즘의 주기 반복도 주장하지 않는다.
수정 `f661864`는 고정 증분 전체의 적격 실패 진입을 유지하고, 실제 변위·mask와 각각의
finite correction PASS로 동등성을 판별한다. Correction 숫자의 차이는 진단으로 유지한다.
관련76개 검사는 native build/CTest0이며 독립 검토를 통과했다. 실제 Hex8 사례의
history 초기화 재삽입은 두 번째 증분100회 실패를 만들었다. 숫자 일치 재삽입은
두 helper 검사의 assertion 실패를 만들었다. 올바른 원본을 복원하고 실제 object를
재컴파일한 뒤 최종 회귀를 수행했다.
이 재현은 질량이 지배적인 작은 문제의 제어흐름 검사이며 원본 conditioning 해결의 증거가
아니다. 원본101개 endpoint의 새 실행은 별도 진행 중이다. 원래 gates·100회 제한은 유지한다.
추가 원시 proof와 검산은 로컬 `.harness/hex8-evidence/t6-independent-semantic/`에,
수정·mutation·최종 회귀 로그는 별도 구현의
`.harness/build-ninja-msvc-debug/hex8-evidence/t6/`에 보존한다. 선형 진단은 닫힌 proof 검토
후 명시적으로 중단했고 비선형 진단은 native exit1로 자연 종료했다. 둘 다 solver PASS가 아니다.
재현 가능한 원시 tuple 검산과 SHA256은 로컬 evidence 재현 가능한 원시 tuple 검산과 SHA256은 로컬 evidence
`.harness/hex8-evidence/t6-independent-tuple/check-v3.py` 및 `v3-check-result.json`에 `.harness/hex8-evidence/t6-independent-tuple/check-v3.py` 및 `v3-check-result.json`에
@@ -42,9 +42,9 @@ exact-zero다. 빈 free vector는 vacuous convergence이며 required prescribed/
### 표현 가능한 변위에서의 내부 정제 ### 표현 가능한 변위에서의 내부 정제
검토된 별도 동적 구현 `b394ae7`은 위 판정을 유지하며 다음 정제를 사용한다. 검토된 별도 동적 구현 `f661864`는 위 판정을 유지하며 다음 정제를 사용한다.
관련75개 검사와 독립 코드 검토는 통과했으나 두 동적 원본은 세 번째 증분에서 실패했다. 관련76개 검사와 독립 코드 검토는 통과했고 두 동적 원본의 새 실행은 진행 중이다.
실제 실패와 정체 증거는 [lessons](lessons.md)에 기록한다. 이전 구현 `b394ae7`의 원본 실패와 변경 근거는 [lessons](lessons.md)에 기록한다.
물리 잔차가 통과한 좌표에서 sub-ULP 갱신 소실이 발생하면, 물리 잔차와 각 좌표의 물리 잔차가 통과한 좌표에서 sub-ULP 갱신 소실이 발생하면, 물리 잔차와 각 좌표의
fresh correction4개가 모두 통과한 좌표를 hold한다. 다음 반복부터 원래 effective tangent의 fresh correction4개가 모두 통과한 좌표를 hold한다. 다음 반복부터 원래 effective tangent의
@@ -52,13 +52,18 @@ fresh correction4개가 모두 통과한 좌표를 hold한다. 다음 반복부
Holding은 새 BC나 equation 제거가 아니다. 다음 반복에서 해당 성분이 원래 물리 기준을 Holding은 새 BC나 equation 제거가 아니다. 다음 반복에서 해당 성분이 원래 물리 기준을
실패하면 즉시 다시 solve에 포함한다. 최종 판정은 항상 모든 원래 free 성분을 사용한다. 실패하면 즉시 다시 solve에 포함한다. 최종 판정은 항상 모든 원래 free 성분을 사용한다.
정체는 잔차 최대 점수의 증가가 아니라 전체 반복 상태의 정확한 재현으로 판별한다. 정체 판별은 잔차 최대 점수의 증가 대신 이미 실패한 Newton 진입 상태로의 복귀를 사용한다.
진입 tuple은 전체3N 변위·reactivation 전 holding mask·incoming correction4개다. 진입 tuple은 전체3N 변위·reactivation 전 holding mask·incoming correction4개다.
Physical FAIL 및 유한 correction PASS 진입만 저장하고, 실제 다음 Newton의 전체 변위· Physical FAIL 및 finite correction4개가 각각 PASS인 진입만 저장한다. 실제 다음 Newton의
freeze 후 mask·fresh correction4개와 모두 정확히 비교한다. 고정 증분의 M·하중·이전 전체 변위·freeze 후 mask가 정확히 같고 fresh correction4개도 각각 finite/PASS이면
accepted state·predictor 및 결정적인 fresh solve/탄성 local recovery가 전제다. 동등한 실패 상태로 판별한다. Correction 숫자의 차이는 진단으로 남기지만 동일성을 요구하지
History는 증분 시작과 실제 ULP 이동 후 초기화한다. Rejected trial에서는 초기화하지 않는다. 않는다. 숫자 자체는 정상 Newton의 rates·tangent·rhs에 사용되지 않는다는 검토에 근거한다.
Prospective physical PASS이면 정상 Newton을 유지하며 별도 history cap이나 threshold는 없다. 고정 증분의 M·하중·이전 accepted state·predictor 및 결정적인 fresh solve/탄성 local
recovery가 전제다. History는 증분 시작에만 초기화하고 실제 ULP 이동 후에도 유지한다.
Prospective physical PASS, correction FAIL 또는 새로운 전체 변위/mask는 정상 Newton을
유지한다. 별도 history cap이나 threshold는 없으며 기존100회 제한으로 기록 수가 제한된다.
이는 알려진 실패 상태의 재방문을 감지해 내부 정제를 시도하는 선택이며 전체 알고리즘의
수렴 보장은 아니다. 실제로 개선하는 이웃이 없으면 기존 Newton 경로를 유지한다.
재현이 확인된 경우에만 각 free 좌표의 양·음 방향 한 ULP 이웃을 예측한다. 재현이 확인된 경우에만 각 free 좌표의 양·음 방향 한 ULP 이웃을 예측한다.
물리 관성력 변화는 `M*delta_u/((1+alpha)*beta*h^2)`, 내력 변화는 `Kt*delta_u`로 물리 관성력 변화는 `M*delta_u/((1+alpha)*beta*h^2)`, 내력 변화는 `Kt*delta_u`로