NSRW v0.6.0 — Research verification and MomentBound

NSRW v0.6.0 — Research verification and MomentBound

This release adds nsrw-verify, an installed command for running
research checks with named inputs and explicit result scope. Each report
records input hashes and the method used. An optional execution manifest
links the report digest to the observed implementation files, dependencies
and Python runtime. GitHub Actions runs the public forced-shear and
normalized-factor checks and retains their reports and manifests.
Manifest mode refuses to publish a result if required implementation
files or the pinned interval dependency cannot be identified.

The workflow was exercised locally on rational matrix inverses, a second
interval implementation of the normalized factor, a manufactured
Navier–Stokes solution and the retained P1 Lean archive. The archive check
reviewed ten recorded declarations and rejected a repacked control that
omitted the mass-zero hypothesis. It reused the original Lean evidence.

MomentBound adds the previously reviewed conditional coefficient and
normalized angular-moment results. Their mathematical scope is governed by
the separate dated receipts. The MB-08 operator bounds passed development
compilation. Fixed source-profile construction, the cutoff jet and the
same-reset amplitude conditions remain open.

• Research verification workflow
• MomentBound coefficient receipt
• Normalized angular-moment receipt
• Changelog

NSRW v0.5.0 — Quantitative angular margins and rigorous core computation

NSRW v0.5.0 - Quantitative margins and exact-rational core computation

Release date: 31 October 2026. Software 0.5.0, mathematical manuscript P01 0.5 and software manuscript P02 0.6 are separate version axes.

Research

For each fixed pinned-source Profile and every sufficiently small positive parameter, a point inside the first repair window has mass history zero and strictly positive angular history at the same point. The quantitative extension supplies a positive local-angular lower bound independent of the selected mass-zero witness and a normalized cutoff-plateau bound.

The ten quantitative/normalization declarations retain proof checkpoint fba27381bcfda3af6f03e2fbae82f6db016ca534, execution checkpoint 7f29ebf0e2b894bf598144628230ae09df436c3d and the 22 October receipt. This software release is not a new Lean execution or independent reproduction.

Computation

A new Python standard-library Fraction prototype computes rigorous exponential and expm1 core-scalar enclosures on a declared absolute dyadic grid. It emits/recomputes deterministic records at 128, 256 and 512 fractional bits. The main denominator's lower endpoint is positive; positive ratios use lower(numerator)/upper(denominator). Tests reject a forged endpoint quantum, malformed/duplicate JSON and attempted scope promotion. See the method and observed execution.

These records do not compute affine-coefficient integrals, numerical q>0, a ResetWitness/K, an explicit source Profile, a root bracket or a numerical J certificate. The large second-bump scale is retained as a lower-bound expression, not a two-sided I01 enclosure.

Distribution

• P01 v0.5: mathematical paper with the quantitative extension, PDF and standalone LaTeX/Markdown source.
• P02 v0.6: software case study with a separate core-computation observation.
• Versioned paper checksum manifests preserve the earlier P01 v0.4 and P02 v0.5 bytes.
• GitHub Pages research site, built from an explicit allowlist of public PDFs and scalar records.
• Code and Lean files MIT; paper text/source/PDF CC BY 4.0; author Yun Kwansub.

P03 remains deferred. Raw execution archives, local review records and authentication data are excluded. No claim of uniform/numerical epsilon, uniqueness, first-zero ordering, a Q pole, a general Navier–Stokes solution, literature priority or application performance is added.

Validation

The code checkpoint adbaeeb82df3bdb9d6d6ea5a041fadc8f35f1b9b passed 645 tests, 3 skipped, 22 subtests and 90.53% statement coverage on the existing Windows environment. Fifty-five tests specifically exercise core scalars. Final release/Pages workflow outcomes are recorded in GitHub Actions rather than inferred from local preparation. The 31 October PDFs have 11 and 10 pages; cached TeX builds report no overfull boxes or missing characters.

Final local release preparation: 649 passed, 3 skipped, 22 subtests, coverage 90.53%; Ruff and documentation link/manifest checks passed. This adds documentation/site checks to the earlier 645-test code checkpoint without changing the numerical algorithm.

Published links and final remote validation

• Research website
• P01 mathematical preprint v0.5
• P02 research-software preprint v0.6
• Exact release-commit CI: all six jobs successful
• GitHub Pages deployment: successful

Release/tag commit: cdce801d7c3f1991e8a0dce48aae9f825b03e9b1. The five GitHub asset digests were compared with the local final assets before publication. Both PDFs served by the public research site match their local SHA-256. The public 128-bit scalar record was downloaded and recomputed. These distribution checks do not add a mathematical claim or independent reproduction.

v0.4.1 — Distribution metadata and Zenodo integration

NSRW v0.4.1 — Distribution metadata and Zenodo integration

A documentation/metadata patch following v0.4.0. Current public pages now
record the observed v0.4.0 publication. Software and citation versions are
0.4.1; P01 remains manuscript v0.4. No mathematical proposition, proof/runner
input, dated Z receipt or original execution checkpoint changed.

• Software commit: adaec7abfd0d374ae3e70153519f3138ed32acb1.
• Exact-commit CI: all six jobs succeeded.
• Detailed notes and asset digests.
• Mathematical execution remains 3a50b5f50b034319a469b9de68f556be70fff02c.

Assets

The three content assets and their SHA256SUMS are reused byte-for-byte from
v0.4.0; filenames retain that original reproduction/manuscript identity.
The GitHub tag source archive is the new v0.4.1 software snapshot.
Raw logs, runtime metadata and compiled binaries are not distributed.
Code/proofs are MIT; P01 authored text is CC BY 4.0. P02/P03 remain deferred.

Zenodo

This Release follows activation of the Zenodo release webhook. Successful
archival, record contents and DOI resolution require separate observation;
no DOI is invented here. Software archival does not create P01's separate
preprint deposit. Existing tags/releases remain unchanged.

No new P2 replay, independent reproduction, uniform/numerical epsilon,
first/unique zero or Q pole/limit is claimed.

v0.4.0 — Z-core / bounded Z+J and P01

NSRW v0.4.0 — mass cancellation without angular-moment cancellation

For every fixed pinned-source Profile F, every sufficiently small positive
parameter admits a point strictly inside its first repair window where the
source mass history vanishes and the angular-weighted history is strictly
positive at the same point. The positive threshold depends on the Profile;
the witness radius may depend on the parameter.

The mechanism is a weighted-tail comparison across two separated repair
supports. The structural conditional theorem needs an interior mass zero and
a positive second repair coefficient, but does not require a positive parameter.
The coefficient-neighborhood and IVT branches provide the existence theorem.

Code, mathematics and reproduction

• Software release commit: 6b81fc0c672ac8d5dd6cea9a7dbe7277ba8793bc.
• Original mathematical execution: 3a50b5f50b034319a469b9de68f556be70fff02c.
• Upstream source: 8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538; Lean 4.34.0-rc2.
• Exact-release CI.
• Reproduction procedure.
• Z-core receipt and
  Z+J receipt.

The two receipts refer to one shared compilation, not independent replications.
The release does not replace or rerun the original mathematical checkpoint.
The source cache was reused. Local software checks passed 550 tests with three
external raw-export checks skipped; software coverage was 90.29%.

Included assets

File	Content
nsrw-v0.4.0-selected-reproduction.zip	Exact proof/driver inputs, unchanged receipt snapshots, selected axiom/stage output and reproduction instructions
P01-MassZero-AngularMismatch-v0.4.pdf	A First-Repair Mass Zero Without Angular-Moment Cancellation, Yun Kwansub
P01-v0.4-source.zip	Standalone LaTeX, Markdown, formal source locators and documentary supplements
SHA256SUMS	Digests of the three assets above; each ZIP also has a member manifest

Software and Lean proof files use MIT; authored P01 text uses CC BY 4.0.
Raw logs/runtime metadata, compiled binaries, caches, private reviews and P02/P03
manuscripts are excluded. The reproduction ZIP is a bounded derivative, not the
complete private execution archive.

The theorem is existential. This release does not establish uniqueness, a first
zero, a numerical/uniform threshold or a pole of the prospective ratio J/(M H).
That ratio's nonzero-denominator condition fails at the exhibited point.

Zenodo software archival is verified separately from GitHub publication. P01's
separate preprint record and DOI are not created by publishing this software release.

[0.3.2] - 2026-10-06

Added

• A source-bound P2-L3 Lean module proving the cross-multiplied template bound
  exp (-(3/20)*c.lam) * rowMoment (c.exponents 1) <= rowMoment (c.exponents 0).
• A bounded L3-only replay runner and negative controls; it does not import
  external F1/L2 artifacts, bootstrap dependencies, or promote its own claims.
• Separate dated 2026-10-06 receipts for strict L2 and L3, and an L3 session
  index linking development, exact-byte checkpoints, and clean replay. Raw
  archives and compiled artifacts remain outside Git.
• Source-linked D composition and main-only C01 coefficient modules, bounded
  fresh-chain replay runners with negative controls, and separate dated
  receipts/session indexes. D confirms NSRW deltaM c < 0 plus two debt
  identities; C01 confirms the positive matrix gap, exact main-only coefficient
  formula, and 0 < affineCoefficients c 0 1 1.
• C02 source-wrapper equalities for generic repair-coefficient decomposition
  and the second axial coefficient of one fixed Profile. This module is
  implemented but uncompiled: a Windows import failed while reading a mathlib
  private artifact, and the reconnected Colab VM has no source or toolchain.
  No C02 compiled receipt is included.

Changed

• Current README/capsule/study wording separates strict L2 from L2-A and L3,
  and distinguishes completed D/C01 propositions from the next actual
  coefficient decomposition and small-positive-eta sign bridges.
• Split C02 implementation, development compilation and commit-bound receipt
  admission in the operational checklist. The next task is environment recovery
  and development compilation, not a sign claim or another framework.
• Publish the resource principles, evidence index, operational-exposure
  definition, stage crosswalk, proposed transfer protocol, roadmap and negative
  register as a linked documentation set. Historical 10/5 snapshots retain
  their original states; dated addenda link the separate 10/6 closures.
• Clarify v0.3.1 as a tagged Git checkpoint with notes, not a published GitHub
  Release object. The tag and its historical mathematical scope are unchanged.

Fixed

• Isolate C01 synthetic replay commands from the shared stdlib subprocess
  module so Windows platform observations cannot be intercepted by fake Lean
  commands; normalize fixture paths and add cold-platform/noncanonical-path
  regression checks. Production replay runner, proof bytes and receipts are
  unchanged.
• Replace stale DeltaM/main-only coefficient prose with the separate D/C01
  compiled receipt scopes; actual eta-dependent signs and first-repair zero
  formal closure remain open.

Not promoted

• Actual c1(0)/c1(eta) signs, first-repair zero and paper-level
  conclusions remain outside the compiled receipt scopes. C02 equalities also
  remain unverified. This version is a Git checkpoint with release notes, not
  a new P2 proof receipt or a published GitHub Release object. Historical
  v0.3.1 statements and its tag are unchanged.

[0.3.1] - 2026-09-13

Added

• A dated clean local Windows receipt for the narrow external P2-F1 Lean
  module. Under the pinned OpenAI source commit and Lean 4.34.0-rc2, it
  compiles the named source-bound proposition
  0 < mainMoment c (1 : Fin 2). The receipt records the exact proof bytes,
  source/proof output hashes, clean-tree checks, and the observed axiom
  surface.
• The first L2 source scaffold, which defines normalized main moments, rewrites
  them to the source short-log integral, and carries the already compiled F1
  positivity into the normalized i = 1 term.

Changed

• The P2 capsule and research-map documentation now distinguish completed
  P2-L1 pulse facts, completed P2-F1 weighted main-moment positivity, and the
  still-open L2 normalized comparison.

Held / not promoted

• The new L2 scaffold is tracked but has no successful external-module compile
  receipt yet. Its strict normalized comparison, DeltaM < 0, repair
  coefficient signs, and the first-repair interior-zero consequence remain
  unpromoted.
• This checkpoint does not claim a paper-level result, full formalization, or
  a solution of the Navier--Stokes problem.

v0.3.0 — M5 scaling-atlas checkpoint

v0.3.0 -- M5 scaling-atlas checkpoint

Release date: 2026-09-12

Release status: RELEASED[HOSTED_CI_VERIFIED]

Version 0.3.0 expands the M5 code surface from one bounded H_scaling
vertical slice to a fixed OutgoingDilation scaling-atlas interface. It does
not claim a complete source-bound atlas, a Lean theorem proof, paper--Lean
semantic equivalence, a selected-source witness, or a solution of the
Navier--Stokes Millennium problem.

Included checkpoint surface

• Adds selected-declaration batch normalization through one streaming raw
  export reader, without reading proof values or falling back to Lean source
  text.
• Defines ten reviewed-static scaling-law entries and exact Fraction
  exponent algebra. Degree-zero outputs are candidates for the next
  mathematical question, not invariants or estimates.
• Closes P1-A: candidate semantic digests cannot be supplied by the caller to
  production atlas admission. Admission requires a separately reviewed ledger
  file and a code-pinned physical SHA-256.
• Adds regression controls for source metadata drift, type-projection drift,
  raw-hash mismatch, law-metadata mutation, and recomputed attacker candidate
  digests.

Evidence boundary

P1-A digest authority              CLOSED[FAIL_CLOSED]
P1 static scaling algebra           PASS[LOCAL_REVIEWED_METADATA]
P1 exponent source derivation       NOT_AUTOMATICALLY_DERIVED_FROM_LEAN
P1 semantic digest authority        HELD[LEDGER_NOT_INDEPENDENTLY_PINNED]
P1 four-law same-raw export         ERROR[EXPORT_CAPACITY_TRUNCATED]
P1 ten-law source-bound atlas       HELD

The 289,992,704-byte partial export is retained only as a failed execution
observation; it is neither committed nor used as source evidence. A complete
ten-law same-raw export, reviewed digest ledger, and code-pinned ledger hash
remain required before production atlas admission can pass.

Hosted release evidence

Implementation commit 771232aab5d0537415ee33e674eba5f2c2c2fe64 passed the
complete pipeline in GitHub Actions run 34683673649:

Python 3.10 / Ubuntu             PASS
Python 3.10 / Windows            PASS
Python 3.12 / Ubuntu             PASS
Python 3.12 / Windows            PASS
research validation and replay   PASS
pinned Lean targets consumed M4  PASS

The hosted Lean job remains scoped to the three M4 targets consumed by the
existing verifier. It does not export the four or ten M5 P1 declarations and
does not change their explicit held status above.

Navier-Stokes Research Workbench v0.2.3

v0.2.3 -- Verifier evidence-boundary closure

Release date: 2026-09-12

Release status: RELEASED[HOSTED_LIVE_VERIFIED]

Version 0.2.3 closes false-success and evidence-authority ambiguities found by
post-implementation review of the v0.2.2 checkpoint. It does not add a new
Navier--Stokes theorem, reconstruct the selected source witness, or establish
paper--Lean semantic equivalence.

Highlights

• Makes M3 shell exit status agree with the recorded Lean PASS, FAIL, or ERROR.
• Derives hosted build classification from bounded GitHub Actions runtime
  identity and rejects receipt/provenance contradictions.
• Routes M4 manifests, Lean requests and receipts, migration records,
  provenance envelopes, and mutation metadata through strict JSON and their
  declared JSON Schema before runtime semantics.
• Adds a LIVE-only compiled-evidence v2 contract and independently re-hashes
  both .olean and dependency files in the same-run verifier.
• Makes Support boundary policy and Cone dependency ordering explicit data.
• Applies the 256-digit exact-rational limit independently to numerator and
  denominator.
• Commits 14 hash-bound pre-mutated JSON manifests and verifies that Python
  mutation generators reproduce them exactly.
• Separates implemented capability from future CFD, spectral, PINN, and
  neural-operator research directions in the public README.

Local release-candidate verification

pytest                         PASS[224]
coverage                       PASS[92.05% >= 90%]
ruff                           PASS
compileall                     PASS
git diff --check               PASS
v3 deterministic replay       PASS[BYTE_IDENTICAL]
v3 replay mutations           PASS[13/13_APPLICABLE]
v3 live-only mutation          NOT_APPLICABLE[LOCAL_REPLAY]

The deterministic replay SHA-256 is:

027C241911F8957EF709CA0241216CE30E1DBB657CF9FACFA9648206E73842DF

Hosted release evidence

Tagged commit 1120b77c5533f012a31fadd3a9185e68d939f3e0 passed the
complete pipeline in
GitHub Actions run 34666375341:

cross-platform Python matrix       PASS[4/4]
research contracts and replay      PASS
pinned Lean same-run targets       PASS[3/3]
compiled evidence mode             LIVE_ARTIFACT
build cleanliness                  HOSTED_CLEAN_CHECKOUT
M4 live receipt                    PASS[COMPLETED]
applicable live mutations          PASS[14/14_REJECTED]

The downloaded evidence validates against the v2 compiled-evidence, v1
provenance, and v3 M4 schemas. Its canonical compiled receipt is bound to
GitHub Actions run 34666375341, attempt 1; the three uploaded dependency
files independently match their admitted SHA-256 values. See
docs/stage_receipts/M4P_V0.2.3_FINAL_RELEASE_HOSTED.md for identities and
scope.

Run 34617896806 and its existing receipt remain historical release-candidate
evidence. Run 34579077366 remains evidence for the untagged v0.2.2 checkpoint
only. Neither supersedes the final tagged-commit run above.

Research boundary

These checks establish only the stated software, source-binding, and compiled
target scope. M4-S remains HELD[NONCOMPUTABLE_SOURCE_INSTANCE], paper--Lean
semantic equivalence remains OPEN_RESEARCH_OBLIGATION, and a solution to the
Navier--Stokes Millennium problem is NOT_ESTABLISHED.

v0.2.0 - Evidence-bound M4-P research gate

NavierStokes Research Workbench v0.2.0

This release establishes the first public, evidence-bound M4-P research gate.
It expands the workbench beyond paper extraction and static declaration checks
while keeping every mathematical claim narrower than the executable evidence.

Highlights

• closes M3 engineering with an explicit noncomputable source-witness boundary;
• adds the M4-P Support, Cone, Moment, and falsification obligation pipeline;
• binds declared source quantifiers to normalized Lean declaration signatures
  and ordered source fragments;
• requires structured compiled evidence for three pinned Lean targets, including
  source commit, toolchain, exit status, .olean identity, and dependency
  surface hashes;
• evaluates six claim/evidence mutations against the clean baseline delta;
• makes source-file hashes portable across Windows CRLF and Linux LF checkouts;
• adds cross-platform Python, deterministic replay, research-custody, and scoped
  Lean build jobs to GitHub Actions;
• keeps SPAR as a secondary diagnostic that cannot override the NSRW hard gate.

Verified release surface

• PASS[LOCAL_TESTS]: 183 tests;
• PASS[COVERAGE]: 94.28% against the 90% gate;
• PASS[RUFF] and PASS[COMPILE];
• PASS[M4-P:SOURCE_SIGNATURES]: 4/4;
• PASS[M4-P:COMPILED_RECEIPTS]: 3/3;
• PASS[M4-P:MUTATIONS]: 6/6 baseline-delta detectors;
• PASS[HOSTED_CI]: Windows and Ubuntu Python matrices, custody replay, and
  pinned Lean target build/receipt comparison.

Research status and limits

M3 engineering                         CLOSED_WITH_NONCOMPUTABLE_SOURCE_BOUNDARY
M4-P pilot hard gate                   PASS[SCOPED]
M4-P analytic research lane            OPEN
M4-S selected source instance          HELD[NONCOMPUTABLE_SOURCE_INSTANCE]
Paper--Lean full semantic equivalence  OPEN_RESEARCH_OBLIGATION
Navier--Stokes millennium solution     NOT_ESTABLISHED

Manufactured and sampled M4-P fixtures test verifier behavior. They do not
reproduce the upstream selected candidate, prove the quantified Lean theorems,
or establish the paper's mathematical conclusions.

Evidence and compatibility notes

• Formal source commit:
  8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538
• Lean toolchain: leanprover/lean4:v4.34.0-rc2
• Compiled targets: OutgoingDilation, OutgoingCone, and
  NominalConeAssembly
• M4 structured Lean receipt SHA-256:
  DD8B248947CAD63804788EC3063E3ED4B8E587BD6D4BFD7029A580B74333E073
• Deterministic source-bound M4 receipt SHA-256:
  F6F4198AFA9F89ADD776FE0152123C58ADA2AB8A5ACB3F08B89B26B2A325229F

Contract and pilot fixture v1 remain in the repository for replay; v2 is the
active hardened interface. The local editable SPAR checkout may report source
version 0.6.0 with stale distribution metadata 0.1.4; the hosted pipeline
uses the immutable pinned SPAR revision.

This is a GitHub source release. No PyPI package publication is claimed.