8Braid · An inspectable proof component
When a proof’s assumptions change
Try “Bound fails, weights work,” then “Negative weight.” One loses a sufficient guarantee; the other has a checked obstruction for those exact inputs.
A small part of a large proof can have a simple reason. Two available directions surround a target. Positive weights combine them to reach it. The formal lemma gives a sufficient allowance for changes in those directions.
This explains the normalized covariance lemma in this repository. It does not simulate a fluid or prove Navier-Stokes blowup. Read the argument · Original Lean proof · Exact examples
Inside the sufficient guarantee
- Target slope s
- Margin m
- 2/5
- Error bound m/4
- 1/10
- First column
- Second column
- Determinant
- First weight p
- Second weight q
Changing the slider is a floating-point illustration. Only the named presets below are checked by the additional Lean examples. The original lemma covers its whole stated parameter domain.
The reason, in three steps
- With unperturbed columns, the equations are p + q = 1 and −p + q = s. Thus p = (1−s)/2 and q = (1+s)/2.
- Keeping |s| ≤ 1−m leaves room before a weight reaches zero. The perturbed proof bounds the determinant and both Cramer numerators.
- Entry errors of at most m/4 preserve positive numerators and a positive determinant. This proves a sufficient guarantee, not an optimal one.
| What you see | What the proof checks |
|---|
| Independent directions | determinant_bounds |
| Target retains positive weights | numerator_bounds, positive_weights |
| The combination reaches the target | cramer_reconstruction |
| The error budget is sufficient | quarter_margin_positive_weights |
The intended PDE application requires separate analytic error estimates, an orthonormal frame, positive physical scales and masses, cone inclusion, and edge-flatness estimates. These are not established by this picture or by the normalized covariance lemma.
The complete released theorem is the authors' forced construction. Our contribution here is a Lean-checked algebraic component and an explanation of its scope. The archived runs were performed by our project. No comprehension study has been run. Read the companion article · Replay record
Why we built this
When a research assumption changes, the next question is which conclusions still have support. At 8Braid, we are developing 8DB to keep claims, their premises and checking evidence connected through those changes. This companion makes one mathematical example inspectable; it runs locally in your browser and does not call the private database engine.
Explore the repository or suggest one changed-assumption example from your work. Public examples help us choose a useful next case.