What the uniruled-fourfold repository actually checks
Proved in Lean, without Mathlib
| Name | Statement |
|---|---|
poly_composition_coherence | If f(n) ≤ n^a+a and g(m) ≤ m^b+b, then g(f(n)) ≤ n^k+k for k = ab+(a+1)^b+b. |
suggested_degree_fails | The smaller exponent ab+b+1 fails: (1^2+2)^2+2 = 11 and 1^7+7 = 8. |
id_difference_quotient_rat | For a nonzero rational h, ((x+h)−x)/h = 1. Closed by grind. The real-number lemma deriv_id is not in this Lean. |
vacuous_separation_false | If both machine predicates are True, the stated P-versus-NP separation is false. |
draft_cook_false | If “satisfiable” is defined as True, the drafted Cook–Levin statement is false. |
theta_does_not_preserve_sign | The constants 1 and −1 match in absolute value, and only one is nonnegative. |
draft_chern_ignores_gauge | A Chern class defined as the constant 1 equals 1. The gauge is unused. |
Gaussian on a fixed grid
A standard Gaussian, σ = 1, translated from center −1.5 toward 1.44 on a 40×40 grid from −5 to 5. np.gradient uses spacing 1. The grid spacing is 0.256. The sum is noise only while the mass is centered.
Duffing energy is not invariant
The update is ḃ = a, ȧ = b − b³ − 0.35 a + 0.4 cos(1.2 t), from (−1.5, 0.5). The quantity a²/2 − b²/2 + b⁴/4 is plotted. It is not a cubic fourfold.
Eight-variable 3-SAT, counted
Forty random formulas, exhaustive search. The draft probabilities 0.92, 0.45, and 0.05 ignore the clauses.
Taylor–Green, one bad step
The initial field sin(x)cos(y)cos(z), −cos(x)sin(y)cos(z), 0 has discrete divergence about 10⁻¹⁵ when the grid spacing is included. The submitted update has no pressure and no z-derivative. After 100 steps the divergence of the two updated components has maximum 0.197. That is not a blow-up theorem.