Formal Replay Preflight for PDE Packets

Status

This page is website copy for a working paper draft. The bounded BuildLang parity witness is BUILD_PARITY_MATCH. A first Lean algebraic cancellation rung is LEAN_REPLAY_MATCH. The finite cyclic first-difference sum is CYCLIC_SUM_REPLAY_MATCH. The finite paired-stencil theorem is CYCLIC_SUMMATION_BY_PARTS_MATCH. The typed finite-grid theorem is TYPED_FINITE_GRID_SBP_MATCH. The finite edge/operator theorem is FINITE_EDGE_OPERATOR_SBP_MATCH. The vector finite-operator theorem is VECTOR_FINITE_OPERATOR_SBP_MATCH. The continuous periodic integration-by-parts theorem is NOT_REPLAYED. Fresh arXiv metadata is SOURCE_LEAD_ONLY. The parent Navier-Stokes existence and smoothness problem remains UNVERIFIABLE.

Claim ledger

BuildLang parity witness

BUILD_PARITY_MATCH. The compiled parity kernel prints nonlinear transfer 1.41311e-14 and max divergence 0. Missing: native buildc relation-invariant receipt and negative fixtures.

Lean replay rung

LEAN_REPLAY_MATCH. A Lean 4.31.0 file now replays two integer cancellation lemmas with exit code 0. This is algebraic cancellation only, not the continuous PDE theorem.

Cyclic finite-sum rung

CYCLIC_SUM_REPLAY_MATCH. A second Lean file replays a finite closed-path first-difference theorem, the discrete shape of sum_i (a[i+1] - a[i]) = 0. This is still discrete List Int algebra.

Cyclic summation-by-parts rung

CYCLIC_SUMMATION_BY_PARTS_MATCH. A third Lean file replays a finite paired-stencil identity: sum_i u[i] * (phi[i+1] - phi[i]) + sum_i phi[i] * (u[i] - u[i-1]) = 0. This is still discrete List (Prod Int Int) algebra.

Typed finite-grid rung

TYPED_FINITE_GRID_SBP_MATCH. A fourth Lean file wraps the finite identity in GridSample and CyclicGrid structures. This is still finite integer grid algebra.

Finite edge/operator rung

FINITE_EDGE_OPERATOR_SBP_MATCH. A fifth Lean file introduces FiniteEdge, ForwardScalarDifference, and BackwardVelocityDifference. This is still finite integer edge/operator algebra.

Vector finite-operator rung

VECTOR_FINITE_OPERATOR_SBP_MATCH. A sixth Lean file introduces Vector2Int, VectorGridSample, VectorCyclicGrid, VectorFiniteEdge, and componentwise gradient/divergence-like operators. This is still finite two-component integer algebra.

Continuous theorem replay

NOT_REPLAYED. There are still no Lean definitions for smooth periodic fields, integrals, divergence-free vector fields, or Navier-Stokes equations in this packet.

Source intake

SOURCE_LEAD_ONLY. The current local demotion gate covers 30 retained arXiv metadata rows and 25 unique IDs for this replay rung. It queues leads; it does not prove source claims.

Tooling receipts

MATCH / VERIFIED. Crucible assessed three bounded packet claims as MATCH 3 / DRIFT 0 / UNVERIFIABLE 0. Learn reverified the prooflesson receipt as VERIFIED. These receipt verdicts cover local packet discipline only.

Grand problem

UNVERIFIABLE. The continuous Navier-Stokes parent claim is not established by a finite grid, a compiler run, metadata intake, or a paper draft.

Method

The preflight turns a grand target into smaller proof obligations that can fail cleanly.

• SOURCE_GATE captures official statements and paper leads without promoting them.
• SUBCLAIM_GATE isolates one bounded mathematical statement with assumptions.
• WITNESS_GATE runs a deterministic executable reference witness.
• RUNTIME_PARITY_GATE checks the witness through a second toolchain.
• FORMAL_ENV_GATE requires a theorem-prover runner before proof replay can be claimed.
• PUBLIC_COPY_GATE keeps outreach, website copy, and paper copy at the strongest proven evidence state and no stronger.

Demonstration

The current target subclaim is the periodic skew-symmetry identity for smooth divergence-free two-dimensional velocity fields.

integral_Omega u dot ((u dot grad)u) dx dy = 0

The BuildLang parity kernel uses the same finite-mode streamfunction design as the JavaScript reference kernel. It computes analytic velocity and derivatives on a periodic grid and sums the nonlinear energy-transfer term.

1.41311e-14
0

• 1.41311e-14 is below the 1e-10 nonlinear-transfer tolerance.
• 0 is below the 1e-12 divergence tolerance.
• The result is a bounded parity witness, not a continuous PDE proof.

Formal target

The next replay target should be intentionally smaller than the full PDE problem: for smooth periodic vector fields with divergence zero, the integral of u dot grad(|u|^2) over the periodic domain is zero.

This isolates integration by parts and periodic boundary cancellation before touching global regularity, weak solutions, turbulence, or three-dimensional existence.

Lean update

The theorem-prover ladder now reaches explicit vector finite-operator vocabulary, but only for finite integer algebra.

• Lean sources: PeriodicCancellationPreflight.lean, CyclicFiniteSumPreflight.lean, CyclicSummationByPartsPreflight.lean, TypedFiniteGridSummationByPartsPreflight.lean, FiniteEdgeOperatorPreflight.lean, and VectorFiniteOperatorPreflight.lean.
• Receipts: lean-periodic-cancellation-replay-2026-07-02.json, lean-cyclic-finite-sum-replay-2026-07-02.json, lean-cyclic-summation-by-parts-replay-2026-07-02.json, lean-typed-finite-grid-sbp-replay-2026-07-02.json, lean-finite-edge-operator-sbp-replay-2026-07-02.json, and lean-vector-finite-operator-sbp-replay-2026-07-02.json.
• Toolchain: Lean 4.31.0, Lake 5.0.0, elan 4.2.3.
• Verdict: VECTOR_FINITE_OPERATOR_SBP_MATCH for finite vector/operator summation by parts only.

Verification receipts

• Crucible: twentieth-wave-tooling-run-2026-07-02.json reports MATCH 3 / DRIFT 0 / UNVERIFIABLE 0 for bounded local packet claims.
• Learn: twentieth-wave-vector-finite-operator.prooflesson.json reverified as VERIFIED from its recorded hash chain.
• Gather: three twentieth-wave stores verify as content-addressed MATCH stores, still demoted to source leads.

BuildLang target

The language/runtime gap is now concrete.

abs(nonlinear_energy_transfer) <= 1e-10
max_divergence_abs <= 1e-12
parent_claim == UNVERIFIABLE

Current buildc receipts can support useful output-series checks, but this packet needs named relation invariants that can be carried as first-class scientific receipts.

Do not infer

• No theorem-prover replay of the continuous periodic integration-by-parts theorem is claimed.
• No claim that the finite cyclic-sum theorem proves smooth periodic integration by parts is made.
• No claim that the finite paired-stencil theorem proves smooth periodic integration by parts is made.
• No claim that the typed finite-grid theorem proves smooth periodic integration by parts is made.
• No claim that the finite edge/operator theorem proves smooth periodic integration by parts is made.
• No claim that the vector finite-operator theorem proves smooth periodic integration by parts is made.
• No global regularity, uniqueness, existence, turbulence, or physical-fluid validation claim is made.
• No native buildc relation-invariant receipt is claimed yet.
• No arXiv metadata row is treated as paper truth or exhaustive coverage.
• No warning-clean compiler status is claimed.