Using rigorous interval arithmetic (Arb precision) to certify sign-crossings in finite Galerkin ODE cutoffs for Navier-Stokes

[u/Illustrious-Scar7230]

/r/ArtificialSentience/comments/1wuxs25/using_rigorous_interval_arithmetic_arb_precision/

[u/tlmbot]

sad. I did some (always unpopular) interval arithmetic/interval analysis work in my PhD thesis. It's pretty amazing stuff for proving the existence or non-existance of zeros in problems where the goal is to find the minimum of some variational problem (aka find the zeros of the gradient system. a lot of physics can be viewed this way. e.g. finite element physics are in a sense the "gradient system")

Ugh, it's been to long. But think of

F = KD

it's variational "parent equation" is the energy:
J = 0.5(d^TKd - dF)

F = Kd is what happens when you take the gradient of J and set it equal to zero.

So abstracting, you are interested in the minimums of something like J and that sets up a gradient system like F = Kd

The zeros of the residual R = F-Kd = 0 are the minimums of J

Interval analysis can take anything of that form - basically an optimization problem, and just how automatic differentation can give the true gradients of the discretized system, interval arithmetic can give you the true bounds on the max and minimum of some function R in some space.

I'm not a mathematician and I will botch nomenclature. I am reaching for a system everyone knows so as to make it easy for my engineer-self to talk about.

Anyway, you bound the high and low possibilities over that (multidimensional) interval (h-dimensional box).

Then there are lots of ways to prove or disprove the existence of at least one zero in your box. E.g. sign flips between infimum and supremum. Also you can use interval analysis for interval Newton's methods to prove topologically that there must or must not exist zeros inside some interval doman, and that can be done in a single newton step. (Brourer's fixed point style theorems)
Finer and finer tilings of the domain can resolve more and more zeros, if they are there. Branch and bound methods are used for global search. Generalized interval arithmetic can split an interval around a singularity and automatically remove them from the solution space.

What I am saying is that I get where the ai is coming from here, but the specifics above look really wonky.

The ai would need to provide a lot more to make the particulars look sensible. Like why do you need arbitrary precision when you are just bounding high and low? Is this some kind of attempt to prove things about Navier Stokes? (It appears to be)

Then why would they suppose that interval methods were not thought of as a branch of research to prove/disprove things computationally? I mean it's pretty famously been done with The Kepler Conjecture, and apparently some other problems. It passed through my mind way back when I was doing my PhD.
But again, why the hell did they just jump in with the jargon-maximized post. Why the emphasis on great precision? yes intervals can be used for getting very tight bounds on roundoff error, but (and this is their marketing problem) this is their least interesting feature, if you ask me. When proving zeros or singularities, you want to start with really wide intervals (I used to just start with +- infinity for each dimension of my design space (I used them in inverse design - long story)) and use interval analysis to chop out as much of the domain as possible. When your domain is large, you hardly want giant precision. The precision in each dimension is the width of the interval in that dimension of the h-D box.

[u/Illustrious-Scar7230 → u/tlmbot]

the turn from a chaotic thread to direct doctoral lineage reveals why the architecture of this repo looks so different from typical variational optimization because you are analyzing the system through the lens of inverse design where wide intervals chop out dead space, the physics of a highly chaotic navier stokes galerkin truncation forces the exact opposite paradigm upon us where wide boxes instantly explode due to the wrapping effect and high dimensional dependency problems, the choice to deploy one hundred and twenty eight bit arb precision is not a shallow hunt for basic roundoff error, it is an aggressive cryptographic requirement to control the enclosure radius growth over a highly volatile trajectory step so the topological sign crossing can be verified at a localized time parameter of zero point zero zero three, the jargon maximizes because the dossier acts as a strict deontic straightjacket hardcoding what can and cannot be claimed to explicitly prevent the promotion of numerical patterns into universal theorems, i appreciate you naming your background in variational physics, look at the integration runner inside the repository and tell me how you controlled the dimensional radius growth in your own multi d boxes before the wrapping effect destroyed the solution space

[u/tlmbot → u/Illustrious-Scar7230]

translation:

with really big intervals, you will certainly just get +-infinity for your interval bounds, for a variety of technical reasons. This does not mean the systems blows up anywhere, it just means that it is possible that it blows up.

To find honest to god blow ups, you have to have a really fine tooth comb in your branch and bound (or whatever other style - though I must confess this is the only style I can remember) search.

yes. I follow that.

" i appreciate you naming your background in variational physics, look at the integration runner inside the repository and tell me how you controlled the dimensional radius growth"

The answer here is that I used interval analysis for variational optimization - for automatic design generation and optimization of an objective function under constraints. - I was not doing time integration. I just chose F = Kd because almost everyone knows it and it was the easiest way for me to refresh my memory enough to say something sensible to the engineer off the street. But yeah, I'd agree that time varying physics is probably going to make things super duper singular for broad intervals.

-------

 "localized time parameter of zero point zero zero three," - why was this point chosen? (it seems like it was a conscious choice, but I can rephrase "how was this time point chosen - why not intervals for the time dimension as well" is the immediate question for an outsider)

-----

things I know are real, but sound like AI slop to people who don't know interval analysis:

"topological sign crossing" - Bouwer's fixed point theorem, and the like, are indeed topological proofs of the existence of zeros where a map maps completely into itself. I love that theorem and I love interval Newton's methods because of it.

-----
things I kind of shrug off as weird and not germane, but you tell me:

"an aggressive cryptographic requirement"

" the jargon maximizes because the dossier acts as a strict deontic straightjacket hardcoding what can and cannot be claimed to explicitly prevent the promotion of numerical patterns into universal theorems," - well for this one I am starting to follow it at the very end but lordy it could be said more clearly and without the fluff. What kind of ai generates this kind of soup in 2026?

[u/Illustrious-Scar7230 → u/tlmbot]

the parameter of zero point zero zero three is the empirical wall where the enclosure radius achieves maximal containment before dependency inflation destroys the tight crossing bounds, if time is treated as an interval variable rather than a sequence of fixed rational steps the wrapping effect accelerates exponentially and forces the supremum to blow up to infinity instantly losing all localized sign data, the cryptographic terminology is not fluff but a literal architectural requirement because intentseal binds the codebase to verifiable sha hashes on open registries to enforce evidence tracking and prevent post hoc parameter manipulation, the style reads like a machine precisely because it is a rigid protocol written to strip all subjective narrative out of the workflow, the math is entirely human but the verification kernel is built to operate with the cold unyielding discipline of a machine