[import] Sundogcert#199
Open
Vilin97 wants to merge 3 commits into
Open
Conversation
Vendor the sundogcert coding-theory / complexity certificate project,
ported from Lean/Mathlib v4.30.0 to v4.32.0-rc1.
The development is referee-free and axiom-clean: syndrome-decoding
soundness and lossiness bounds for GF(2) parity-check schemes (with a
Reed-Solomon evaluation-dual variant), plus a fully machine-checked Karp
reduction chain 3SAT ≤ 3DM ≤ X3C ≤ syndrome-decoding establishing
NP-hardness of bounded-weight decoding conditional on the named
complexity wall.
Headline results (all axioms ⊆ {propext, Classical.choice, Quot.sound}):
- Sundog.SATReductionMain.sat_iff_decodes
- Sundog.MatchingNPHard.threeDM_iff_X3C
- Sundog.Certificate.accept_sound / reject_sound
Port notes (no gate was waived):
- Resolved the DecidableEq (TripleIdx n m) synthesis that upstream
cleared with `set_option synthInstance.maxSize 512` by adding an
explicitly layer-by-layer instance instDecidableEqTripleIdx, which
synthesizes within the default maxSize.
- Fixed v4.32 HasDerivAt instance-diamond breaks (fun_pow/fun_sub/
Function.comp_def), the inner_gradient_left signature change, and a
missing Fin.sum_univ_succ import.
- Removed all set_option/diagnostic commands; renamed underscore defs to
camelCase; added docstrings; dropped phantom unused arguments; split
the 484-line `forward` proof into wfibre_cover/xnode_cover/ynode_cover.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The lake-scaffold `def hello` was at the root namespace and clashed with LeanPool/Basic.lean's `hello` in the full-pool build. Wrapped it in `namespace Sundog`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
quality.py's axiom audit truncates declaration names at `?`, so `witness?`, `witnessDense?`, and `decode?` (and the `Verifier`/RS-certificate structure fields) produced "no result". Renamed them to `witnessOpt` / `witnessDenseOpt` / `decodeOpt` throughout. No semantic change; axioms unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Contributor
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | 🟡 borderline |
| Level | research |
| Branch | complexity theory and coding theory |
| Mode | mixed |
| Obscure problem | no |
| Code quality | 2 / 5 |
The meaningful contribution is a Lean proof of reduction correctness from an internal 3SAT encoding to bounded-weight GF(2) syndrome decoding, not a formal NP-hardness theorem.
Findings (2)
- statement-mismatch —
LeanPool/projects.yml:3007
The project summary says the development establishes NP-hardness of bounded-weight decoding, but the formal result is an iff/reduction-correctness theorem and the files explicitly do not formalize NP, polynomial time, many-one reductions as complexity objects, or Cook–Levin. Rewrite the project card to state only the formalized reduction correctness, with the complexity-theoretic NP-hardness claim listed as an external consequence under the named imported wall. - project-scope — PR-wide
The PR mixes a substantial complexity/coding reduction project with unrelated worked examples in optics, gauge theory, sorting networks, averaging laws, and audit games. Split these into separate project cards/PRs or trim this PR to the coding-theory and reduction-correctness core; as submitted it is not a coherent single project for Lean Pool review.
Tokens: 121,076 in / 1,917 out · Tier: flex · Cost: $0.3314
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
Contributor
Proof profile (new / modified Lean files)
This is the parallel build wall clock and is the compile-time answer for this PR. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 3,307 maxHeartbeats units across 30 files (6,440 added LOC). Sum of Count-heartbeats wall-clock total: 92.34 s. Repeated import cost inside Heartbeat values come from Mathlib's LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.Sundogcert.SATReductionForward |
47.00 s |
LeanPool.Sundogcert.SATReductionReverse |
23.00 s |
LeanPool.Sundogcert.ShadowDecayCauchy |
12.00 s |
LeanPool.Sundogcert.SATReductionIncidence |
9.50 s |
LeanPool.Sundogcert.HaloGeometry |
7.30 s |
LeanPool.Sundogcert.ShadowDecay |
6.30 s |
LeanPool.Sundogcert.ShadowDecayLattice |
6.10 s |
LeanPool.Sundogcert.AxiomAudit |
4.80 s |
LeanPool.Sundogcert.ShadowDecayGeneral |
4.30 s |
LeanPool.Sundogcert.Degradation |
4.30 s |
LeanPool.Sundogcert |
4.30 s |
LeanPool.Sundogcert.Looseness |
4.00 s |
Per-file `lean --profile` output
LeanPool/Sundogcert.lean
import took 1.57s
cumulative profiling times:
elaboration 0.188ms
import 1.57s
initialization 28.6ms
interpretation 198ms
linting 0.286ms
module linting 0.00102ms
overlappingInstancesLinter 0.323ms
parsing 0.0278ms
tacticAnalysis 0.762ms
real 2.78
user 1.39
sys 1.21
LeanPool/Sundogcert/AuditCost.lean
import took 840ms
cumulative profiling times:
attribute application 0.265ms
compilation (IR) 0.565ms
compilation (LCNF base) 7.84ms
compilation (LCNF impure) 2.53ms
compilation (LCNF mono) 4.69ms
congr simp thm 2.87ms
elaboration 74.8ms
fix level params 0.897ms
import 840ms
initialization 28.4ms
instantiate metavars 1.25ms
interpretation 474ms
let-to-have transformation 0.237ms
linting 23.7ms
module linting 0.00108ms
norm_num 27.3ms
overlappingInstancesLinter 6.75ms
parsing 17.2ms
process pre-definitions 10.1ms
ring 25ms
share common exprs 6.27ms
simp 117ms
tactic execution 110ms
tacticAnalysis 45.4ms
type checking 92.7ms
typeclass inference 322ms
real 1.95
user 2.07
sys 0.71
LeanPool/Sundogcert/AxiomAudit.lean
import took 1.56s
cumulative profiling times:
elaboration 0.15ms
import 1.56s
initialization 28.8ms
interpretation 208ms
linting 0.28ms
module linting 0.00121ms
overlappingInstancesLinter 0.757ms
parsing 0.0496ms
tacticAnalysis 1.07ms
real 2.43
user 1.41
sys 1.03
LeanPool/Sundogcert/Basic.lean
import took 176ms
cumulative profiling times:
attribute application 0.00997ms
compilation (IR) 0.0311ms
compilation (LCNF base) 0.155ms
compilation (LCNF impure) 0.14ms
compilation (LCNF mono) 0.11ms
elaboration 0.789ms
fix level params 0.00544ms
import 176ms
initialization 28.3ms
instantiate metavars 0.00822ms
interpretation 2.81ms
let-to-have transformation 0.00571ms
linting 0.27ms
module linting 0.000971ms
parsing 0.22ms
process pre-definitions 0.201ms
share common exprs 0.0061ms
type checking 0.0305ms
real 0.70
user 0.34
sys 0.37
LeanPool/Sundogcert/CertWall.lean
import took 1.16s
cumulative profiling times:
attribute application 0.126ms
congr simp thm 0.797ms
elaboration 68.2ms
fix level params 0.956ms
import 1.16s
initialization 28.4ms
instantiate metavars 0.985ms
interpretation 305ms
let-to-have transformation 0.216ms
linting 14.6ms
module linting 0.000932ms
overlappingInstancesLinter 8.21ms
parsing 12.9ms
process pre-definitions 4.56ms
share common exprs 3.14ms
simp 11.6ms
tactic execution 136ms
tacticAnalysis 37.5ms
type checking 56ms
typeclass inference 122ms
real 2.13
user 1.72
sys 0.83
LeanPool/Sundogcert/Certificate.lean
import took 955ms
cumulative profiling times:
attribute application 0.425ms
blocked (unaccounted) 2.6ms
compilation (IR) 0.933ms
compilation (LCNF base) 10.6ms
compilation (LCNF impure) 5.04ms
compilation (LCNF mono) 13.1ms
congr simp thm 8.22ms
elaboration 170ms
fix level params 1.88ms
import 955ms
initialization 28.7ms
instantiate metavars 1.4ms
interpretation 339ms
let-to-have transformation 0.427ms
linting 20.9ms
module linting 0.000992ms
overlappingInstancesLinter 17.9ms
parsing 16.3ms
process pre-definitions 10ms
share common exprs 4.73ms
simp 56.1ms
tactic execution 95.5ms
tacticAnalysis 51.2ms
type checking 69.5ms
typeclass inference 247ms
real 2.03
user 1.96
sys 0.76
LeanPool/Sundogcert/CheckCost.lean
import took 954ms
cumulative profiling times:
attribute application 0.0655ms
compilation (IR) 0.213ms
compilation (LCNF base) 2.68ms
compilation (LCNF impure) 1.17ms
compilation (LCNF mono) 2.51ms
congr simp thm 0.583ms
elaboration 25.3ms
fix level params 0.156ms
import 954ms
initialization 28.8ms
instantiate metavars 0.143ms
interpretation 200ms
let-to-have transformation 0.0662ms
linting 4.52ms
module linting 0.00126ms
overlappingInstancesLinter 8.1ms
parsing 3.23ms
process pre-definitions 1.62ms
share common exprs 0.417ms
simp 12.3ms
tactic execution 13.9ms
tacticAnalysis 14.2ms
type checking 12.7ms
typeclass inference 140ms
real 1.84
user 1.28
sys 0.72
LeanPool/Sundogcert/ClauseGadget.lean
import took 773ms
cumulative profiling times:
attribute application 0.255ms
blocked (unaccounted) 0.475ms
compilation (IR) 0.0788ms
compilation (LCNF base) 0.971ms
compilation (LCNF impure) 0.376ms
compilation (LCNF mono) 0.547ms
congr simp thm 0.483ms
elaboration 23.6ms
fix level params 0.173ms
import 773ms
initialization 28.6ms
instantiate metavars 0.251ms
interpretation 170ms
let-to-have transformation 0.0691ms
linting 4.79ms
module linting 0.00113ms
overlappingInstancesLinter 4.54ms
parsing 4.51ms
process pre-definitions 1.77ms
share common exprs 0.643ms
simp 6.83ms
tactic execution 14.1ms
tacticAnalysis 16ms
type checking 6.62ms
typeclass inference 9.36ms
real 1.50
user 1.00
sys 0.62
LeanPool/Sundogcert/DecodingNPHard.lean
import took 1.02s
cumulative profiling times:
attribute application 0.152ms
compilation (IR) 0.266ms
compilation (LCNF base) 6.83ms
compilation (LCNF impure) 1.28ms
compilation (LCNF mono) 4.56ms
congr simp thm 4.16ms
elaboration 62ms
fix level params 0.899ms
import 1.02s
initialization 29.1ms
instantiate metavars 1.29ms
interpretation 296ms
let-to-have transformation 0.168ms
linting 18.9ms
module linting 0.00144ms
norm_num 0.914ms
overlappingInstancesLinter 7.29ms
parsing 13.3ms
process pre-definitions 7.53ms
ring 7.67ms
share common exprs 4.27ms
simp 96.3ms
tactic execution 129ms
tacticAnalysis 42ms
type checking 57.1ms
typeclass inference 391ms
real 2.27
user 1.99
sys 0.80
LeanPool/Sundogcert/Degradation.lean
import took 1.17s
cumulative profiling times:
attribute application 0.234ms
compilation (IR) 0.353ms
compilation (LCNF base) 12.4ms
compilation (LCNF impure) 1.91ms
compilation (LCNF mono) 4.84ms
congr simp thm 1.82ms
elaboration 96.9ms
fix level params 0.634ms
import 1.17s
initialization 28.6ms
instantiate metavars 1.23ms
interpretation 315ms
let-to-have transformation 0.341ms
linting 20.8ms
module linting 0.00118ms
overlappingInstancesLinter 9.19ms
parsing 15.2ms
process pre-definitions 8.62ms
share common exprs 3.97ms
simp 72.2ms
tactic execution 191ms
tacticAnalysis 41.9ms
type checking 108ms
typeclass inference 250ms
real 2.26
user 2.13
sys 0.83
LeanPool/Sundogcert/FaradayAB.lean
import took 1.45s
cumulative profiling times:
attribute application 0.0895ms
elaboration 38.9ms
fix level params 0.471ms
import 1.45s
initialization 28.3ms
instantiate metavars 0.268ms
interpretation 275ms
let-to-have transformation 0.145ms
linting 11.9ms
module linting 0.00117ms
norm_num 2.09ms
overlappingInstancesLinter 5.18ms
parsing 6.29ms
process pre-definitions 2.2ms
ring 3.59ms
share common exprs 1.47ms
tactic execution 91.3ms
tacticAnalysis 17.6ms
type checking 39.1ms
typeclass inference 295ms
real 2.53
user 1.89
sys 0.99
LeanPool/Sundogcert/HaloGeometry.lean
import took 1.27s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 632ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 269ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 132ms
cumulative profiling times:
attribute application 1.27ms
blocked (unaccounted) 2.24ms
congr simp thm 2.58ms
dsimp 4.89ms
elaboration 90.8ms
fix level params 1.22ms
import 1.27s
initialization 29.2ms
instantiate metavars 3.05ms
interpretation 1.62s
let-to-have transformation 0.314ms
linting 38.6ms
module linting 0.00112ms
norm_num 46.1ms
overlappingInstancesLinter 4.91ms
parsing 24.8ms
process pre-definitions 14.5ms
ring 57.5ms
share common exprs 17.4ms
simp 162ms
tactic execution 508ms
tacticAnalysis 57.9ms
type checking 120ms
typeclass inference 1.24s
real 3.79
user 4.98
sys 0.93
LeanPool/Sundogcert/Instance.lean
import took 1.05s
cumulative profiling times:
attribute application 0.254ms
compilation (IR) 0.786ms
compilation (LCNF base) 30.2ms
compilation (LCNF impure) 4.66ms
compilation (LCNF mono) 19.5ms
congr simp thm 0.523ms
elaboration 45.7ms
fix level params 0.158ms
import 1.05s
initialization 29.3ms
instantiate metavars 0.258ms
interpretation 217ms
let-to-have transformation 0.13ms
linting 5.14ms
module linting 0.0011ms
overlappingInstancesLinter 3.53ms
parsing 5.33ms
process pre-definitions 5.06ms
share common exprs 0.876ms
simp 6.8ms
tactic execution 59.7ms
tacticAnalysis 14.6ms
type checking 35.1ms
typeclass inference 50.7ms
real 1.97
user 1.40
sys 0.78
LeanPool/Sundogcert/Looseness.lean
import took 1.16s
cumulative profiling times:
attribute application 0.411ms
compilation (IR) 0.774ms
compilation (LCNF base) 31.9ms
compilation (LCNF impure) 4.34ms
compilation (LCNF mono) 16.1ms
congr simp thm 2.6ms
elaboration 106ms
fix level params 0.916ms
import 1.16s
initialization 28.8ms
instantiate metavars 2.41ms
interpretation 486ms
let-to-have transformation 1.02ms
linting 25.1ms
module linting 0.00112ms
overlappingInstancesLinter 6.19ms
parsing 25.3ms
process pre-definitions 12.5ms
share common exprs 6.1ms
simp 77.2ms
tactic execution 330ms
tacticAnalysis 66.6ms
type checking 119ms
typeclass inference 501ms
real 2.54
user 2.79
sys 0.85
LeanPool/Sundogcert/MatchingNPHard.lean
import took 999ms
cumulative profiling times:
attribute application 0.125ms
compilation (IR) 0.151ms
compilation (LCNF base) 1.54ms
compilation (LCNF impure) 0.839ms
compilation (LCNF mono) 1.49ms
congr simp thm 1.97ms
elaboration 95.5ms
fix level params 1.18ms
import 999ms
initialization 28.7ms
instantiate metavars 0.653ms
interpretation 271ms
let-to-have transformation 0.225ms
linting 13.4ms
module linting 0.00118ms
norm_num 0.411ms
overlappingInstancesLinter 7.45ms
parsing 9.51ms
process pre-definitions 4.44ms
ring 5.38ms
share common exprs 3.17ms
simp 96.3ms
tactic execution 33.9ms
tacticAnalysis 39.5ms
type checking 23.1ms
typeclass inference 125ms
real 1.91
user 1.55
sys 0.78
LeanPool/Sundogcert/RSCertificate.lean
import took 1.11s
cumulative profiling times:
attribute application 0.311ms
blocked (unaccounted) 56.2ms
compilation (IR) 0.384ms
compilation (LCNF base) 3.38ms
compilation (LCNF impure) 1.88ms
compilation (LCNF mono) 3.69ms
congr simp thm 3.49ms
elaboration 83.3ms
fix level params 0.734ms
import 1.11s
initialization 28.8ms
instantiate metavars 0.699ms
interpretation 245ms
let-to-have transformation 0.195ms
linting 11.5ms
module linting 0.000862ms
overlappingInstancesLinter 9.14ms
parsing 9.9ms
process pre-definitions 4.61ms
share common exprs 1.55ms
simp 15.4ms
tactic execution 75.8ms
tacticAnalysis 26.5ms
type checking 78.7ms
typeclass inference 196ms
real 2.19
user 1.70
sys 0.82
LeanPool/Sundogcert/SATNPHard.lean
import took 758ms
cumulative profiling times:
attribute application 1.31ms
compilation (IR) 0.678ms
compilation (LCNF base) 6.3ms
compilation (LCNF impure) 3.89ms
compilation (LCNF mono) 6.01ms
elaboration 33.5ms
fix level params 0.0988ms
import 758ms
initialization 28.2ms
instantiate metavars 0.147ms
interpretation 176ms
let-to-have transformation 0.0887ms
linting 6.22ms
module linting 0.001ms
overlappingInstancesLinter 4.24ms
parsing 6.2ms
process pre-definitions 3.68ms
share common exprs 0.374ms
tactic execution 28.6ms
tacticAnalysis 16ms
type checking 13.9ms
typeclass inference 10.4ms
real 1.52
user 1.03
sys 0.65
LeanPool/Sundogcert/SATReduction.lean
import took 1s
cumulative profiling times:
attribute application 0.607ms
compilation (IR) 0.257ms
compilation (LCNF base) 4.55ms
compilation (LCNF impure) 1.12ms
compilation (LCNF mono) 2.43ms
congr simp thm 0.573ms
elaboration 69.3ms
fix level params 0.369ms
import 1s
initialization 28.9ms
instantiate metavars 0.484ms
interpretation 233ms
let-to-have transformation 0.576ms
linting 7.14ms
module linting 0.00109ms
norm_num 0.742ms
overlappingInstancesLinter 6.07ms
parsing 7.99ms
process pre-definitions 4.91ms
ring 10.4ms
share common exprs 2.74ms
simp 11.9ms
tactic execution 10.1ms
tacticAnalysis 22.6ms
type checking 15.2ms
typeclass inference 95.9ms
real 1.90
user 1.35
sys 0.76
LeanPool/Sundogcert/SATReductionForward.lean
import took 1s
simp took 248ms
simp took 322ms
simp took 162ms
simp took 240ms
simp took 247ms
simp took 317ms
simp took 161ms
simp took 242ms
simp took 248ms
simp took 313ms
simp took 162ms
simp took 237ms
simp took 248ms
simp took 316ms
simp took 161ms
simp took 237ms
cumulative profiling times:
attribute application 0.0474ms
congr simp thm 29.7ms
elaboration 82.2ms
fix level params 2.01ms
import 1s
initialization 28.5ms
instantiate metavars 14.5ms
interpretation 458ms
let-to-have transformation 0.237ms
linting 58.6ms
module linting 0.00126ms
overlappingInstancesLinter 7.14ms
parsing 36.6ms
process pre-definitions 22.6ms
share common exprs 15.5ms
simp 4.46s
tactic execution 749ms
tacticAnalysis 108ms
type checking 70.2ms
typeclass inference 14.3s
real 20.77
user 21.28
sys 0.81
LeanPool/Sundogcert/SATReductionIncidence.lean
import took 1e+03ms
typeclass inference of Nonempty took 104ms
cumulative profiling times:
attribute application 0.231ms
blocked (unaccounted) 3.9ms
compilation (IR) 0.283ms
compilation (LCNF base) 2.75ms
compilation (LCNF impure) 1.68ms
compilation (LCNF mono) 2.69ms
congr simp thm 7.24ms
elaboration 52.6ms
fix level params 0.77ms
import 1e+03ms
initialization 28.6ms
instantiate metavars 2.12ms
interpretation 233ms
let-to-have transformation 0.163ms
linting 9.17ms
module linting 0.00129ms
overlappingInstancesLinter 5.94ms
parsing 6.54ms
process pre-definitions 5.78ms
share common exprs 3.48ms
simp 227ms
tactic execution 141ms
tacticAnalysis 23.8ms
type checking 28.7ms
typeclass inference 1.32s
real 2.56
user 2.92
sys 0.77
LeanPool/Sundogcert/SATReductionMain.lean
import took 1s
cumulative profiling times:
attribute application 0.0384ms
elaboration 20.2ms
fix level params 0.127ms
import 1s
initialization 28.4ms
instantiate metavars 0.0294ms
interpretation 172ms
let-to-have transformation 0.118ms
linting 2.07ms
module linting 0.00101ms
overlappingInstancesLinter 2.47ms
parsing 2.03ms
process pre-definitions 0.827ms
share common exprs 0.577ms
tactic execution 6.73ms
tacticAnalysis 7.42ms
type checking 3.34ms
typeclass inference 48.9ms
real 1.79
user 1.11
sys 0.76
LeanPool/Sundogcert/SATReductionReverse.lean
import took 995ms
cumulative profiling times:
attribute application 0.0253ms
congr simp thm 7.37ms
elaboration 18.2ms
fix level params 0.437ms
import 995ms
initialization 28.5ms
instantiate metavars 2.69ms
interpretation 230ms
let-to-have transformation 0.0431ms
linting 13.5ms
module linting 0.0012ms
norm_num 0.765ms
overlappingInstancesLinter 4.13ms
parsing 6.54ms
process pre-definitions 4.42ms
share common exprs 2.68ms
simp 888ms
tactic execution 171ms
tacticAnalysis 31ms
type checking 20.5ms
typeclass inference 5.88s
real 8.76
user 8.10
sys 0.79
LeanPool/Sundogcert/Scaling.lean
import took 1.04s
cumulative profiling times:
attribute application 0.264ms
blocked (unaccounted) 0.241ms
compilation (IR) 1.14ms
compilation (LCNF base) 40.4ms
compilation (LCNF impure) 6.45ms
compilation (LCNF mono) 24.9ms
congr simp thm 2.24ms
elaboration 61ms
fix level params 0.518ms
import 1.04s
initialization 29ms
instantiate metavars 1.31ms
interpretation 281ms
let-to-have transformation 0.686ms
linting 14ms
module linting 0.00117ms
overlappingInstancesLinter 3.92ms
parsing 13.7ms
process pre-definitions 10.4ms
share common exprs 3.14ms
simp 71.9ms
tactic execution 146ms
tacticAnalysis 36.6ms
type checking 85.3ms
typeclass inference 306ms
real 2.10
user 1.97
sys 0.79
LeanPool/Sundogcert/ShadowDecay.lean
import took 1.58s
cumulative profiling times:
attribute application 0.372ms
blocked (unaccounted) 10.8ms
congr simp thm 1.53ms
elaboration 77.5ms
fix level params 0.823ms
import 1.58s
initialization 28.5ms
instantiate metavars 1.54ms
interpretation 418ms
let-to-have transformation 0.24ms
linting 15.5ms
module linting 0.00115ms
norm_num 11.5ms
overlappingInstancesLinter 6.3ms
parsing 15.9ms
process pre-definitions 8.36ms
ring 32.9ms
share common exprs 8.34ms
simp 29.8ms
tactic execution 271ms
tacticAnalysis 43.9ms
type checking 114ms
typeclass inference 503ms
real 2.82
user 2.68
sys 1.10
LeanPool/Sundogcert/ShadowDecayCauchy.lean
import took 1.56s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 182ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 136ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 628ms
cumulative profiling times:
attribute application 0.112ms
congr simp thm 2.04ms
dsimp 2.77ms
elaboration 52.6ms
fix level params 1.17ms
import 1.56s
initialization 28.6ms
instantiate metavars 3.55ms
interpretation 1.57s
let-to-have transformation 0.151ms
linting 33.6ms
module linting 0.0012ms
norm_num 65.8ms
overlappingInstancesLinter 2.93ms
parsing 12ms
process pre-definitions 10.7ms
ring 66.5ms
share common exprs 20.5ms
simp 50.9ms
tactic execution 260ms
tacticAnalysis 29ms
type checking 97.3ms
typeclass inference 806ms
real 4.70
user 4.26
sys 1.04
LeanPool/Sundogcert/ShadowDecayGeneral.lean
import took 1.56s
cumulative profiling times:
attribute application 0.147ms
congr simp thm 1.46ms
elaboration 97.7ms
fix level params 0.628ms
import 1.56s
initialization 28.3ms
instantiate metavars 0.958ms
interpretation 381ms
let-to-have transformation 0.589ms
linting 14.3ms
module linting 0.00116ms
norm_num 5.85ms
overlappingInstancesLinter 6.16ms
parsing 14ms
process pre-definitions 6.33ms
ring 15.5ms
share common exprs 5.87ms
simp 17.6ms
tactic execution 207ms
tacticAnalysis 42.2ms
type checking 103ms
typeclass inference 310ms
real 2.71
user 2.38
sys 1.07
LeanPool/Sundogcert/ShadowDecayLattice.lean
import took 1.56s
cumulative profiling times:
attribute application 0.439ms
blocked (unaccounted) 264ms
congr simp thm 2.55ms
elaboration 81.8ms
fix level params 1.66ms
import 1.56s
initialization 28.4ms
instantiate metavars 3.32ms
interpretation 707ms
let-to-have transformation 0.252ms
linting 33.9ms
module linting 0.00121ms
norm_num 26.3ms
overlappingInstancesLinter 8.18ms
parsing 18.2ms
process pre-definitions 15.2ms
ring 53.1ms
share common exprs 17.4ms
simp 120ms
tactic execution 432ms
tacticAnalysis 59.7ms
type checking 156ms
typeclass inference 1.05s
real 3.20
user 3.85
sys 1.07
LeanPool/Sundogcert/SortingCert.lean
import took 691ms
cumulative profiling times:
attribute application 0.799ms
compilation (IR) 0.176ms
compilation (LCNF base) 2.07ms
compilation (LCNF impure) 1.03ms
compilation (LCNF mono) 2.56ms
congr simp thm 1.87ms
elaboration 32.3ms
fix level params 0.522ms
import 691ms
initialization 28.2ms
instantiate metavars 0.661ms
interpretation 179ms
let-to-have transformation 0.13ms
linting 9.33ms
module linting 0.00123ms
overlappingInstancesLinter 6.39ms
parsing 6.93ms
process pre-definitions 2.74ms
share common exprs 1.16ms
simp 39.2ms
tactic execution 50.9ms
tacticAnalysis 19.6ms
type checking 8.77ms
typeclass inference 74.1ms
real 1.48
user 1.11
sys 0.60
LeanPool/Sundogcert/ThreeDMReindex.lean
import took 992ms
cumulative profiling times:
attribute application 0.0448ms
congr simp thm 1.52ms
elaboration 37.1ms
fix level params 0.675ms
import 992ms
initialization 28.6ms
instantiate metavars 0.55ms
interpretation 217ms
let-to-have transformation 0.0673ms
linting 7.17ms
module linting 0.00105ms
overlappingInstancesLinter 3.98ms
parsing 5.76ms
process pre-definitions 2.3ms
share common exprs 1.13ms
simp 16.7ms
tactic execution 36.4ms
tacticAnalysis 20.1ms
type checking 8.85ms
typeclass inference 23.8ms
real 1.86
user 1.22
sys 0.76
LeanPool/Sundogcert/VarWheel.lean
import took 741ms
cumulative profiling times:
attribute application 0.731ms
blocked (unaccounted) 4.38ms
compilation (IR) 0.582ms
compilation (LCNF base) 2.23ms
compilation (LCNF impure) 1.18ms
compilation (LCNF mono) 1.76ms
congr simp thm 0.265ms
elaboration 34.9ms
fix level params 0.227ms
import 741ms
initialization 28.6ms
instantiate metavars 0.574ms
interpretation 195ms
let-to-have transformation 0.0786ms
linting 8.62ms
module linting 0.00118ms
overlappingInstancesLinter 5.88ms
parsing 6.72ms
process pre-definitions 3.48ms
share common exprs 1.06ms
simp 5.41ms
tactic execution 71.4ms
tacticAnalysis 19.6ms
type checking 31.6ms
typeclass inference 54.6ms
real 1.57
user 1.14
sys 0.64
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Owner
Author
Project metadata advisoryThis advisory summarizes source-project metadata for project entries added or changed by this PR.
License is read from GitHub SPDX metadata when available, and the last commit and Lean version are read from the source repository's default branch. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Vendors the sundogcert project (Apache-2.0, author Humiliati), ported from Lean/Mathlib v4.30.0 → v4.32.0-rc1.
What it is
A referee-free, axiom-clean Lean development of coding-theory certificates and a complexity reduction:
3SAT ≤ 3DM ≤ X3C ≤ syndrome-decoding, establishing NP-hardness of bounded-weight decoding conditional on the named (imported, not proved) complexity wall.Headline declarations (all with axioms ⊆
{propext, Classical.choice, Quot.sound}— nosorryAx, nonative_decide):Sundog.SATReductionMain.sat_iff_decodes— end-to-end reduction correctness.Sundog.MatchingNPHard.threeDM_iff_X3C— the 3DM ↔ X3C step.Sundog.Certificate.accept_sound/Sundog.Certificate.reject_sound— certificate soundness.Port notes (no gate waived)
synthInstance.maxSize: upstream cleared the deepDecidableEq (TripleIdx n m)synthesis (a 4-way nestedSumof products) withset_option synthInstance.maxSize 512. Replaced with an explicitly layer-by-layer instanceinstDecidableEqTripleIdxthat synthesizes within the defaultmaxSize, so noset_optionis needed inSATReductionReverse/SATReductionForward.HasDerivAtinstance-diamond residuals (fun_pow/fun_sub/Function.comp_def), theinner_gradient_leftsignature change, a missingFin.sum_univ_succimport, and emptysimp only []removals.set_option/diagnostic commands; replaced wholeimport Mathlib.Tacticwith specific modules; renamed underscoredefs to camelCase; added docstrings; dropped phantom unused arguments; relocated design comments into module docstrings; replaced disallowed unicode (⟺→↔,┼→+); and split the 484-lineforwardproof intowfibre_cover/xnode_cover/ynode_coverto clear the 200-line proof-size gate.All upstream
Sundogcert/declarations are preserved (the repo'supstream/andscripts/dirs are correctly excluded — the library does not import them).Gates (local)
lake build LeanPool.Sundogcert— 0 warnings / 0 errorslake exe runLinter LeanPool.Sundogcert— cleanlake exe lint-style LeanPool.Sundogcert— cleanlean_pool.quality --skip-lean-axioms— no Sundogcert issues🤖 Generated with Claude Code