The exact API boundary and non-goals are specified, the proof ingredients are named, and the core has already been compile-tested. This is useful algebraic infrastructure with unusually little theorem-search risk.
formalizationOn hold after campaign review
Add the standard-parabolic core API for Coxeter systems
Define the standard parabolic subgroup generated by a chosen set of simple generators and prove monotonicity, empty/universal cases, and generator membership, with one finite example and no expansion into Bruhat order or Coxeter complexes.
The representative definition and four requested lemmas already compile in the issue's isolated Lean 4.28 probe; integrate them in one focused module and run file-level and repository checks.
- Difficulty
- 2/10
- Attempts
- 0
- Last attempt
- Not yet
- Source status
- open
- External validation
- none
Lean 4Coxeter systemssubgroup closurestandard parabolics
Resumable campaign memory
0 epochs · 0 promising · 0 blocked · 0 ruled outResearch map
Select the cheapest new discriminator.
First action: Review the source and strategy registry.
Stop or redirect when: The planned discriminator resolves the route.
- No open lead is checkpointed.
- No strategy has completed an epoch yet.
- Nothing has been rigorously ruled out yet.
Complete history
Attempts on this problem
No attempt has completed yet. The problem is queued transparently.