NS Robustness & Reachability Lab v0.7

建立在 Proof-to-Computation v1.7 與 Robustness v0.1 之上的第二階段。v0.2 掃描 radial cutoff × Lambda × eta-grid robustness phase diagram，並直接擾動 admissible SchedulePressure 參數 P、m、lambda、wait；同時把 repo 中的 formal small-perturbation lemmas 整理成 Formal Robustness Ladder。

v1.4 是第一個真正的 precision-state experiment。DD fixed-point iteration 自 referencePair 起就在 double-double 中更新；但 fixed coefficient / SchedulePressure source data 仍由 Float64 建立，所以這是 solver arithmetic precision convergence，不是完整 source-data 106-bit pipeline。

模擬參數

預設

N×N

精度

起始 t

停止 t

Domain 半寬 L

CFL

Poisson Jacobi 次數

每 frame solver steps

熱圖

Forcing Intervention

forcing 模式

forcing scale λ

t_off

smooth ramp width

OpenAI exact-layer probe

h (Lean: 0<h≤0.001)

j (Lean: 0<j≤0.001)

z probe

P(root) probe

Λ profile scale

physical geometry map

Exact Entrance Reference Profile

σ in χ=H²/(H²+σ²)

Y probe

η probe

series tolerance

profile heatmap

Reference Pair / Pressure Datum Probe

P₀ family

conditional P ≥ 1

conditional quadratic c ≥ 0

reference-pair heatmap

SchedulePressure Family Parameters

core P (theorem path uses P≥2)

core m > 0

core λ (0<λ<0.1)

core wait > 25

stepBound witness S

pressure quadrature

Nonlinear Coefficient Fixed Point — v0.8

Λ fixed-point scale

C normalization

radial degree N

η grid

max fixed-point iterations

fixed-point tolerance

nonlinear profile map

AnalyticInputs Witness Candidate

complex tube radius ρ

complex witness grid

regular-set margin

Cutoff / η-grid Convergence Ensemble

尚未執行 ensemble。

Empirical Jacobian / Lipschitz Audit — v1.1

random directions

base relative δ

power-style iterations

尚未執行 local Jacobian audit。

Jacobian Convergence + Precision Horizon Prototype — v1.2

ensemble Jacobian directions

precision safety bits

target retained bits

尚未執行 Jacobian convergence。

Double-Double Precision Audit — v1.3

DD hotspot mode

DD display floor

尚未執行 double-double audit。

Double-Double Fixed-Point State — v1.4

DD max iterations

DD fixed-point tolerance

DD precision ensemble

尚未求解 double-double fixed-point state。

DD Source-Data Pipeline — v1.5

source DD mode

尚未執行 DD source-data pipeline。

DD Transcendental Source — v1.6

DD transcendental terms

DD transcendental tolerance

尚未執行 DD transcendental source pipeline。

Arbitrary-Exponent Scaled-DD Runtime — v1.7

singularity stress −log₁₀ q = N

amplitude stress Λ

scaled plot samples

尚未執行 arbitrary-exponent stress。

Robustness & Reachability Audit — v0.1

perturbation norm

directions / family

ε minimum

ε maximum

ε samples

recovery iterations

success reduction factor

source pressure max |ε|

尚未執行 robustness audit。

Robustness Phase Diagram — v0.2

phase family

phase norm

phase directions

phase epsilon max

schedule perturbation size

尚未執行 v0.2 phase / schedule audit。

Formal Margin Ladder + Physical Entrance Bridge — v0.3

physical bridge family

physical perturbation ε

Y samples

η samples

physical directions

尚未執行 formal/physical bridge audit。

TransitionRamp → ActivationCone Margin Propagation — v0.4

reference upper bound B candidate

comparison constant C candidate

normalized T₀

retained damping κ

normalized axial ramp w₁

normalized angular ramp w₂

尚未執行 transition/activation margin propagation。

Mref / Cs / Cr Bound Inflation Microscope — v0.5

Mref candidate

Cs candidate

Cr candidate

T₀ normalization

尚未執行 bound inflation audit。

Direct inverseRelativeError / Cᵣ Extraction — v0.6

Cr source σ

Cr source Λ

T max

T samples

u samples

η samples

NaturalProfile η resolution

Simpson panels

尚未執行 Cᵣ extraction。

Direct P/Q Stock-Factor Extraction — v0.7

stock source σ

stock source Λ

NaturalProfile η resolution

T max

u samples

history panels

phase quadrature panels

尚未執行 stock-factor extraction。

粒子向量箭頭失穩自停

目前狀態

事件紀錄

t / τ

—

adaptive dt

—

CFL + viscosity

ℓ/Δx

—

L∞ candidate / solver

—

relative tracking error

—

RMS solver-candidate / RMS candidate

div u RMS

—

projection quality

solver energy

—

2D slice ∫|u|²

candidate sampled / true L∞

—

fixed-grid miss ratio

forcing fraction

實際餵給 solver 的 λ(t)

OpenAI exact Q / η

—

repo axis speed theorem

—

$(1-t)^{-A(h)}j$

radial / axial core length

—

carrier k / wavelength

—

exact Φ_ref(Y,η)

—

profile ODE residual

—

2(YΦʺ+2Φʹ)+χΦ

entrance min Φ

—

theorem target > 1/4

u_ref / B_ref

—

second reference / average

Z* / ∂ηB_ref

—

pressure-dependent exact formula

entrance coneSize

—

p₁+p₂²/p₁

stepBound witness / scan max

—

Classical.choose realization audit

scheduled P₀ / P₀′

—

at η probe

endpoint / tailStart

—

log-radius clock

nonlinear FP residual

—

||x-F(x)||∞

empirical contraction ratio

—

last residual ratio

shift / tail ratio

—

||x-x₀||∞ / highest-degree ratio

reconstructed f / U / V / Pr

—

at scaled Y, η probe

real-axis log Cmin / Cmin

—

lower threshold from real axis only

tube-candidate log Cmin / Cmin

—

numerical AnalyticInputs witness

C / tube candidate

—

not a Lean certificate

complex regular-set margins

—

min |L| / min |H²+σ²|

radiusLoss / amplitudeBound

—

ε=ρ/2 ⇒ q=1/2

sampled field B / coefficient bound

—

numerical common-field witness candidate

log10 resolvent norm majorant

—

Σ K^k/(k!(k+1)!)

log10 profileError majorant

—

remainderBound upper-majorant

log10 stabilityScale majorant

—

1+(14000/9)K

log10 contraction threshold

—

1+B+Lip

selected Λ / proof-majorant Λ₀

—

numerical behavior vs proof bound

empirical local Lipschitz max

—

multi-scale central differences

power-style Jacobian growth

—

dominant-direction probe

proof / empirical gap

—

decimal orders of magnitude

finite-difference plateau spread

—

scale-conditioning audit

Jacobian N=10→12 drift

—

raw / source-like jet norm

Jacobian η81→101 drift

—

raw / source-like jet norm

empirical jet-power Λ crossing

—

m≤1 source-like norm, repeated J action

worst cancellation / bits lost

—

Σ|term| / |Σterm|

recommended precision

—

target + lost + safety

precision hotspot

—

nonlinear remainder operator path

DD worst relative correction

—

|S_DD−S_53| / |S_DD|

DD observed bits lost

—

53 − retained relative bits

DD worst hotspot

—

group / η / radial degree

predicted vs observed bits lost

—

v1.2 proxy / full-DD operator difference

DD state fixed-point residual

—

||x₁₀₆−F_DD(x₁₀₆)||∞

x₅₃ vs x₁₀₆ relative state drift

—

max coefficient relative correction

x₅₃ vs x₁₀₆ agreement bits

—

−log₂(relative drift)

DD probe φ / u correction

—

at selected Y, η

DD precision ensemble drift

—

state correction under refinement

DD P₀ source correction

—

pressure accumulation correction at probe η

DD χ / Z* source correction

—

max relative fixed-axis drift

referencePair source drift

—

DD-source pair vs Float64-source pair

x₁₀₆ source-induced drift

—

DD source+solver vs Float source+DD solver

total x₅₃ → full-DD-source state

—

global / source-like jet agreement

DD exp/log self-consistency

—

max |log(exp(x))−x|

σ transcendental correction

—

DD σ vs Float64 σ on source nodes

g(y) / shape source correction

—

finalAngular² / shapeExponent

P₀ transcendental correction

—

v1.6 DD-trans vs v1.5 DD-algebra

x₁₀₆ transcendental source drift

—

DD-trans source vs DD-algebra source

total x₅₃ → v1.6 state

—

global / source-like weighted drift

first raw range horizon

—

earliest Float64/DD overflow or underflow in q-scaling

U_core at stress N

—

Scaled-DD scientific representation

ℓ_r at stress N

—

Scaled-DD scientific representation

Γ at stress N

—

amplitude / radial-scale separation

NaturalProfile max amplitude

—

stress Λ, scaled exp(Λ phase)/C

raw amplitude overflow Λ

—

Float64/DD raw exponent-range wall

proof Λ₀ materialized

—

v1.0 proof majorant as actual scaled number

scaled arithmetic self-test

—

10^100000 · 10^-99999 and exp(100000)

empirical ε₅₀ basin proxy

—

50% recovery threshold across perturbation families

success at largest ε

—

fraction returning to same fixed point

worst perturbation family

—

lowest recovery fraction near transition

max transient amplification

—

max distance / initial distance

reference-line reach proxy

—

largest successful source-like proxy distance from reference x₀

pressure-source susceptibility

—

state drift / |pressure scaling ε|

source perturbation convergence

—

successful perturbed fixed-point solves

robustness interpretation

—

finite-map basin proxy only

phase min ε₅₀

—

minimum tested basin threshold over N×Λ

phase collapse index

—

log-slope of ε₅₀ with N / Λ

η-grid robustness drift

—

last-step ε₅₀ change

worst schedule parameter

—

largest state susceptibility

schedule family convergence

—

admissible perturbed solves converged

sampled entrance φ minimum

—

finite-lattice nonlinear profile diagnostic

formal perturbation layers

—

source-verified compact perturbation uses

numeric global formal δ

—

existential vs quantitatively extracted

sampled φ−1/4 margin

—

Y∈[0,4], η∈[-1,1]

sampled min shear A

—

A = −2X f_X/f

sampled min shear-size−2

—

A(1+(B/A)²)−2

physical velocity susceptibility

—

max Δ(E,U) / coefficient ε

physical shear susceptibility

—

max Δ(A,B) / coefficient ε

physical inequalities preserved

—

sampled φ>1/4, A>0, shearSize>2

bridge derivative identity error

—

analytic coefficient derivative vs finite-X difference

formal activation c

—

actual proof call uses c=1/8

ActivationCone error tolerance s*

—

min(1/4,c/2,1/[4(B+1)])

activation collar θ candidate

—

σ(θ)=c/[4(B+1)] worst-case κ=0

T*/T₀ candidate

—

min(1,s*/[(C+1)T₀])

retained ramp P margin

—

P > 2+c/4

retained collar v margin

—

v > 2+c/2

TransitionRamp stock→slope gain

—

max local perturbation gain

v0.3 reference margin reserve

—

sampled r_min−(2+c)

sampled center g lower bound

—

|B|+|B/A|+|B²/A|+|r|

combined M

—

max(Mref,Cs,Cr)

comparison constant Cerr

—

M+2M²+M³

certified-form T*/T₀ candidate

—

s*(Mref)/(Cerr+1)/T0

cubic inflation factor

—

Cerr/M

dominant hidden factor

—

Mref vs Cs vs Cr

Cᵣ sampled sup

—

max |inverseRelativeError|

Cᵣ hotspot

—

(T,κ,u,η)

max |∂ᵧ log f|

—

reference natural segment

factorization identity error

—

ratio vs controlledErrorFactor form

Cᵣ / Mref-center

—

does reciprocal error dominate?

T→0 stability

—

sup difference between T=0 limit and smallest positive T

M₁ sampled sup |P|

—

stockOne smooth factor

M₂ sampled sup |Q|

—

stockTwo smooth factor

Cₛ sampled

—

max(M₁,M₂)

dominant stock factor

—

P vs Q hotspot

stock extraction path

—

history stock vs direct p₁/p₂

κ→1 boundary drift

—

0.99 vs 0.999 envelope

combined sampled M

—

max(g-center,Cₛ,Cᵣ)

sampled Cerr / T*/T₀

—

cubic proof-budget diagnostic

formal perturbation ladder

4 layers

NaturalEntrance → ReferenceBounds → MatchingCone → ActivationContinuation

步數

forward solver steps

數值狀態

READY

—

解析 candidate（隨時間真正動畫）

Forward projection solver

動態歷史

candidate L∞ solver L∞ tracking error ℓ/Δx

這版到底在測什麼？

不是問 Lean 對不對，而是把同一個解析 forcing 丟給普通有限網格的 forward solver。若解析 candidate 真能被有限計算解析，右邊應先跟著左邊；當核心尺度跌破網格、CFL 變嚴、pressure projection 與 cancellation 開始失真時，兩條 trajectory 會分離。

因此這版第一次真的有： state(t) → state(t+dt)，而不是上一版只拿不同時間切片各自畫圖。

OpenAI Lean Exact-Layer Adapter — Phase 1

以下數值不是 surrogate：公式直接對應 repo 的 NaturalAxisData.lean 與 SimilarityCoordinates.lean。coordinateQ 在 Lean 中是由唯一正根經 Classical.choose 定義；這裡用 monotone bisection 做可執行 realization。

曲線：forwardScalar(q)=q-z²q^2h；水平線：τ=1-t；交點即 coordinateQ。橘點為數值 bisection 根。

OpenAI physical core geometry — $(r,z)$ slice

Exact source-derived scale laws

顯示 repo `Scaling.lean` 與 `NaturalCore.lean` 的精確尺度律；不是 surrogate。

Exact OpenAI Entrance Reference Profile

Series convergence & ODE audit

ReferencePair second profile / average / cone

NaturalEntrance sourceJets (6D)

Schedule clock: g(y) & shape exponent a(y)

Scheduled axis pressure P₀(η)

Truncated nonlinear NaturalProfile

Fixed-point convergence

AnalyticInputs complex-tube witness

Normalization threshold audit

Radial cutoff convergence

按 Run convergence ensemble。

η-grid convergence

按 Run convergence ensemble。

Proof-bound tower — log10 scale

Complex fixed-field sup candidates

Empirical local Lipschitz vs perturbation scale

按 Run local Jacobian audit。

Sampled Jacobian direction distribution

按 Run local Jacobian audit。

Power-style Jacobian iteration

按 Run local Jacobian audit。

Proof majorant vs empirical map

按 Run local Jacobian audit。

Empirical Jacobian vs radial cutoff

按 Run Jacobian convergence。

Empirical Jacobian vs η-grid

按 Run Jacobian convergence。

Empirical contraction scale vs Λ

按 Run Jacobian convergence。

Precision hotspot — cancellation bits

Condition-aware precision recommendation

Float64 vs Double-Double correction

按 Run double-double audit。

Predicted lost bits vs observed DD low part

按 Run double-double audit。

DD fixed-point residual convergence

按 Solve DD fixed point。

x₅₃ → x₁₀₆ correction by radial degree

按 Solve DD fixed point。

DD precision ensemble

按 Run precision ensemble。

Float64 vs DD probe correction

按 Solve DD fixed point。

DD source corrections

按 Build DD source + solve。

Precision-error decomposition

按 Build DD source + solve。

ReferencePair source correction by degree

按 Build DD source + solve。

Full source-DD state correction by degree

按 Build DD source + solve。

Transcendental correction decomposition

按 Build DD transcendental source + solve。

DD exp/log round-trip self-test

按 Run DD exp/log self-test。

Schedule source correction along y

按 Build DD transcendental source + solve。

Precision-layer state decomposition

按 Build DD transcendental source + solve。

Singularity dynamic-range stress

按 Run arbitrary-exponent stress。

NaturalProfile amplitude range

按 Run arbitrary-exponent stress。

Raw-format horizons

按 Run arbitrary-exponent stress。

Scaled-DD mantissa / exponent audit

按 Run arbitrary-exponent stress。

State perturbation recovery vs ε

按 Run state robustness。

Family-dependent fragility

按 Run state robustness。

Transient amplification

按 Run state robustness。

Reference-line reachability

按 Run line reachability。

Pressure-datum source perturbation

按 Run source robustness。

Worst-case recovery trajectory

按 Run state robustness。

N × Λ basin phase diagram

按 Run N×Λ phase。

N × Λ transient amplification

按 Run N×Λ phase。

η-grid basin refinement

按 Run η-grid phase。

SchedulePressure parameter susceptibility

按 Run SchedulePressure family perturbation。

Sampled nonlinear entrance φ under source-family perturbation

按 Run SchedulePressure family perturbation。

Formal Robustness Ladder

repo 中已發現的 formal local-perturbation layers。