Navier–Stokes Proof-to-Computation Dynamic Lab v1.7

動態 solver + Arbitrary-Exponent Scaled-DD Runtime。v1.7 將數值表示拆成 DD mantissa × 2^BigInt exponent，第一次把 significand precision 與 dynamic range 正式解耦，並加入 NS core scaling、NaturalProfile amplitude 與 proof-majorant range stress。

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。

粒子向量箭頭失穩自停

目前狀態

事件紀錄

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)

步數

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

Scaled-DD mantissa / exponent audit

按 Run arbitrary-exponent stress。

Navier–Stokes Proof-to-Computation Dynamic Lab v1.7

模擬參數

目前狀態

事件紀錄

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

Forward projection solver

動態歷史

這版到底在測什麼？

OpenAI Lean Exact-Layer Adapter — Phase 1

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

Exact source-derived scale laws

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

η-grid convergence

Proof-bound tower — log10 scale

Complex fixed-field sup candidates

Empirical local Lipschitz vs perturbation scale

Sampled Jacobian direction distribution

Power-style Jacobian iteration

Proof majorant vs empirical map

Empirical Jacobian vs radial cutoff

Empirical Jacobian vs η-grid

Empirical contraction scale vs Λ

Precision hotspot — cancellation bits

Condition-aware precision recommendation

Float64 vs Double-Double correction

Predicted lost bits vs observed DD low part

DD fixed-point residual convergence

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

DD precision ensemble

Float64 vs DD probe correction

DD source corrections

Precision-error decomposition

ReferencePair source correction by degree

Full source-DD state correction by degree

Transcendental correction decomposition

DD exp/log round-trip self-test

Schedule source correction along y

Precision-layer state decomposition

Singularity dynamic-range stress

NaturalProfile amplitude range

Raw-format horizons

Scaled-DD mantissa / exponent audit

Arbitrary-exponent runtime provenance

DD transcendental provenance

DD source-data provenance

Double-double fixed-point provenance

Double-double audit provenance

Precision-horizon prototype provenance

Empirical Jacobian provenance

Proof-bound tower provenance

AnalyticInputs / theorem-threshold provenance

Coefficient fixed-point provenance

SchedulePressure provenance

Exactness boundary — 目前真正接到哪裡？