Constraint Resonance State Evolution

NS–SR Correspondence

Public Package 002 · Propagation-and-causality correspondence audit.
Native causal compatibility fails on the unrestricted seam; a conditional finite-speed sector reaches certified L2 admissibility.

Overview Source Models Correspondence Information Boundary Causality & Propagation Theorem Manifest Assumptions Lean Source Axiom Audit Explicit Nonclaims

CRSE · Public Package 002

Overview

This package performs a formal correspondence audit between the existing restricted classical Navier–Stokes source and a newly defined minimal Special-Relativity causal source. The target is deliberately narrow: whether the selected propagation information can cross a declared route while respecting the future-causal structure of flat Minkowski spacetime.

native NS mechanical evolution ≠ causal correspondence ≠ Lorentzian correspondence
Native VerdictThe unrestricted seam is obstructed: mere time ordering is insufficient for SR future-causal admissibility.
Conditional PassAn explicitly restricted finite-speed region reaches certified L2 causal-order admissibility.
Information BoundaryThe shared host carries aggregate mechanical channels but does not carry the spacetime event tag required for causal reconstruction.
Verification810-line Lean module; clean full build; no sorry/admit/new axioms or implemented_by; autoImplicit disabled.

Independent Native Structure

Source Models

Navier–Stokes. The package reuses the Public Package 001 source and adapter unchanged: unforced, constant-density, incompressible, viscous operator-form Navier–Stokes together with its existing evolution-preservation certificate.

Special Relativity. The new native block defines flat-spacetime events, the Minkowski interval with signature (+,−,−,−), timelike/null/spacelike separation, and a future-causal relation. The causal relation is proved reflexive, transitive and antisymmetric and is shown equivalent to the interval-based causal condition. Concrete timelike, null, spacelike, related and unrelated witnesses are supplied.

Δs² = c²(Δt)² − ‖Δr‖²

Declared Route

Correspondence

The package declares typed crossings from tagged Navier–Stokes data to the SR event layer and instantiates an actual route in the existing correspondence-network machinery. Capabilities are proved only where they hold; a shared CRSE codomain is never treated as a correspondence by itself.

Tagged NS data → declared crossing → SR event / causal layer

On the native unrestricted source region, the seam is not admissible: the NS-side guarantee used by the crossing supplies time order but not the spatial bound required by FutureCausal.

Representation Loss

Information Boundary

The existing host encoding preserves aggregate force and velocity channels but drops the spacetime tag. Two tagged states may therefore carry identical mechanical encodings while referring to different spacetime events. The package proves that no reader of the host state can reconstruct the lost event tag.

(flow, event₁) ≠ (flow, event₂)    while    host(flow,event₁) = host(flow,event₂)

No extra host slot is introduced to hide this limitation. The missing locality channel is recorded as an interface insufficiency.

Certified Ladder · Level L2 Conditional

Causality & Propagation

The unrestricted route fails the SR causal requirement. A separately named finite-speed region restores admissibility and yields a genuine causal-order certificate. The package additionally proves that this restriction is strict, load-bearing, non-vacuous, and not implied by the reused Navier–Stokes source law.

restricted pair: ‖Δr‖ ≤ c Δt    ⇒    FutureCausal

An explicit honesty receipt identifies the restricted region as the pullback of the SR causal cone along the declared crossing. The finite-speed bound is therefore imported, not derived from Navier–Stokes. No L3 interval-preservation or L4 Lorentz-covariant mechanical correspondence is claimed.

L0Typed declared route exists.
L1Finite-speed admissibility available only under an explicit added restriction.
L2Conditional future-causal / causal-order admissibility certified.
L3 / L4Not certified. Finite-speed admissibility is not promoted to Lorentzian or full relativistic-mechanical correspondence.

Formal Surface

Theorem Manifest

The delivered module groups its headline results into the following proved blocks:

  1. SR event and interval definitions
  2. timelike / null / spacelike trichotomy
  3. FutureCausal reflexivity
  4. FutureCausal transitivity
  5. FutureCausal antisymmetry
  6. interval / future-causal equivalence
  7. average-speed bound
  8. spacelike causal refusal
  9. translation invariance
  10. spatial-rotation invariance
  11. Galilean non-preservation witness
  12. functional tagging crossing
  13. declared route / network witness
  14. native seam incompatibility
  15. unrestricted route inadmissibility
  16. spacetime-tag loss
  17. event non-reconstructibility
  18. restricted finite-speed admissibility
  19. restriction strictness
  20. restriction load-bearing witness
  21. restriction non-vacuity
  22. restriction not implied by NS law
  23. pullback-of-causal-cone honesty receipt
  24. evolution preservation ≠ causal preservation
  25. shared codomain ≠ route
  26. finite-speed admissibility ≠ Special Relativity

Note. This web loadout preserves the delivered public theorem surface at the result level. Exact declaration names remain those in RequestProject/NavierStokesSRCorrespondence.lean and its companion report.

Load-Bearing Conditions

Assumptions

  • Navier–Stokes side retains the P001 restricted source: unforced, constant density, incompressible, viscous, operator form.
  • Special-Relativity side is flat Minkowski spacetime with positive invariant speed parameter c.
  • The native unrestricted NS certificate does not include event locality or finite-speed propagation.
  • The L2 pass assumes a separately declared finite-speed region; that assumption is not derived from the NS law.
  • No host-field reinterpretation is used to store spacetime tags.
  • No composition, relativistic-fluid repair, GR, QFT, Noether, accretion, FUSE, emergence, or old CRSE propagation constant is used to close the result.

Formal Artifact

Lean Source

Source: RequestProject/NavierStokesSRCorrespondence.lean
Namespace: ResonantEvolution.NavierStokesSRCorrespondence
Size: 810 lines

The source reuses the existing ReductionAdapter, CorrespondenceBridge and NavierStokesReduction modules without modifying or forking them. The complete Lean file and companion report belong to the formal project; they were not part of the website files supplied for this loadout, so this page does not fabricate an inline source copy.

Machine Check

Axiom Audit

BuildFull lake build reported successful.
Proof GapsNo sorry and no admit.
DeclarationsNo new axiom declarations and no @[implemented_by].
Headline AuditIn-file #print axioms results report only propext, Classical.choice and Quot.sound.

Scope Firewall

Explicit Nonclaims

  • No claim that Navier–Stokes reduces to Special Relativity.
  • No claim that CRSE repairs or relativizes classical Navier–Stokes.
  • No claim of a relativistic viscous-fluid theory.
  • No claim that the finite-speed restriction is derived from the Navier–Stokes source law.
  • No claim that finite-speed admissibility alone establishes Lorentz covariance or Special Relativity.
  • No identification of any CRSE/USST propagation constant with the physical speed of light.
  • No GR, QFT, Yang–Mills, quantum-gravity or cosmological claim.
  • No Navier–Stokes existence, uniqueness, regularity or Millennium Prize claim.
  • No claim that a shared CRSE codomain creates a route.
  • No composition, accretion, emergence or fused-system result.

Related Formal Work

Package Chain

Public Package 001 — Navier–Stokes Reduction
Return to Formal Work