IE-04: no uniform exponential Gaussian-smoothed GEPP tail
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete formally checked negative resolution of the uniform exponential Gaussian-smoothed GEPP tail, with all 21 frozen obligations, genuine product Gaussian measures, the full nonsingular perturbation box and arbitrary positive real proposed constants.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, IE-04/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-ie-04-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 15 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:04:13.051106
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.IE04.not_uniformExponentialTail | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00078 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.IE04.not_uniformExponentialTail
Not NLA.IE04.UniformExponentialTail
RegistryProblems.Problem_OP_00078
Prop
Build log
anDensity (17s) info: NLA/IE04/GaussianDensity.lean:71:0: 'NLA.IE04.exp_neg_two_lower' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/GaussianDensity.lean:73:0: 'NLA.IE04.standard_normal_density_lower' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/GaussianDensity.lean:75:0: 'NLA.IE04.gaussian_interval_lower' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3762/3773] Built NLA.IE04.Scalars (19s) info: NLA/IE04/Scalars.lean:124:0: 'NLA.IE04.scalar_budgets' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/Scalars.lean:125:0: 'NLA.IE04.quotient_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/Scalars.lean:126:0: 'NLA.IE04.scalar_schur_error' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3763/3773] Built NLA.IE04.GEPP (17s) info: NLA/IE04/GEPP.lean:294:0: 'NLA.IE04.entryMax_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/GEPP.lean:296:0: 'NLA.IE04.schurStep_bound_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/GEPP.lean:298:0: 'NLA.IE04.gepp_growth_bound_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/GEPP.lean:300:0: 'NLA.IE04.activeInjective_initial_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/GEPP.lean:302:0: 'NLA.IE04.activeInjective_nonzero_column_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/GEPP.lean:304:0: 'NLA.IE04.activeInjective_rowSwap_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/GEPP.lean:306:0: 'NLA.IE04.schurStep_mulVec_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/GEPP.lean:308:0: 'NLA.IE04.activeInjective_schur_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/GEPP.lean:310:0: 'NLA.IE04.firstTrajectory_activeInjective_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/GEPP.lean:312:0: 'NLA.IE04.firstPath_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3764/3773] Built NLA.IE04.GaussianBox (15s) info: NLA/IE04/GaussianBox.lean:106:0: 'NLA.IE04.gaussian_box_product' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/GaussianBox.lean:108:0: 'NLA.IE04.gaussian_box_probability' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3765/3773] Built NLA.IE04.StrictPivots (17s) info: NLA/IE04/StrictPivots.lean:125:0: 'NLA.IE04.noSwap_nonsingular_of_pivots' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/StrictPivots.lean:127:0: 'NLA.IE04.strictNoSwap_path_unique' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3766/3773] Built NLA.IE04.Measurability (17s) info: NLA/IE04/Measurability.lean:194:0: 'NLA.IE04.firstPath_admissibleRule_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/Measurability.lean:196:0: 'NLA.IE04.gaussianMatrix_probability_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/Measurability.lean:198:0: 'NLA.IE04.exceedanceEvent_measurable_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3767/3773] Built NLA.IE04.Witness (9.3s) warning: NLA/IE04/Witness.lean:47:15: This simp argument is unused: Fin.val_mk Hint: Omit it from the simp argument list. [apply] simp only at hv Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: NLA/IE04/Witness.lean:70:36: Variable name `hn` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hn Note: This linter can be disabled with `set_option linter.unusedVariables false` info: NLA/IE04/Witness.lean:144:0: 'NLA.IE04.witness_trajectory' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/Witness.lean:146:0: 'NLA.IE04.witness_strict_growth' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3768/3773] Built NLA.IE04.Robustness (9.1s) info: NLA/IE04/Robustness.lean:180:0: 'NLA.IE04.full_box_robust' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/Robustness.lean:182:0: 'NLA.IE04.growth_on_box' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3769/3773] Built NLA.IE04.ProbabilityTail (7.6s) info: NLA/IE04/ProbabilityTail.lean:55:0: 'NLA.IE04.gaussian_box_in_actual_event' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/ProbabilityTail.lean:57:0: 'NLA.IE04.gepp_gaussian_tail_lower' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3770/3773] Built NLA.IE04.Final (8.2s) warning: NLA/IE04/Final.lean:27:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` info: NLA/IE04/Final.lean:70:0: 'NLA.IE04.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE04/Final.lean:72:0: 'NLA.IE04.not_uniformExponentialTail' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3771/3773] Built Solution (8.0s) info: Solution.lean:45:0: 'NLA.IE04.entryMax_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:47:0: 'NLA.IE04.firstPath_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:49:0: 'NLA.IE04.firstPath_admissibleRule' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:51:0: 'NLA.IE04.gaussianMatrix_probability' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:53:0: 'NLA.IE04.exceedanceEvent_measurable' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:55:0: 'NLA.IE04.witness_trajectory' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:57:0: 'NLA.IE04.witness_strict_growth' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:59:0: 'NLA.IE04.scalar_budgets' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:61:0: 'NLA.IE04.quotient_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:63:0: 'NLA.IE04.scalar_schur_error' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:65:0: 'NLA.IE04.full_box_robust' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:67:0: 'NLA.IE04.growth_on_box' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:69:0: 'NLA.IE04.standard_normal_density_lower' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:71:0: 'NLA.IE04.gaussian_interval_lower' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:73:0: 'NLA.IE04.gaussian_box_product' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:75:0: 'NLA.IE04.gaussian_box_probability' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:77:0: 'NLA.IE04.gaussian_box_in_actual_event' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:79:0: 'NLA.IE04.gepp_gaussian_tail_lower' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:81:0: 'NLA.IE04.contradiction_dimension' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:83:0: 'NLA.IE04.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:85:0: 'NLA.IE04.not_uniformExponentialTail' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3772/3773] Built RegistryRecord (7.9s) Build completed successfully (3773 jobs).