Repository navigation
Reduce frame validation to complement masks - #338
Conversation
Greptile SummaryThe PR replaces ternary
Confidence Score: 5/5The PR appears safe to merge. No blocking failure remains.
|
| Filename | Overview |
|---|---|
| LeanPool/FrontierMathOpenHypergraphs/Uniform/FrameDefs.lean | Introduces the complement reduction, binary mask enumeration, and kernel-checked soundness proof while removing the raw ternary checker. |
| LeanPool/FrontierMathOpenHypergraphs/Uniform/FrameBoosters.lean | Migrates booster certificates to complement masks, retaining correctly staged leaves for the larger specifications. |
| LeanPool/FrontierMathOpenHypergraphs/Uniform/FrameExact.lean | Migrates all exact small-frame certificates to the complement checker without changing bank indices. |
| LeanPool/FrontierMathOpenHypergraphs/Uniform/FrameResidues.lean | Migrates all residue-gadget certificates to the complement checker without changing bank indices. |
Flowchart
%%{init: {'theme': 'neutral'}}%%
flowchart LR
A[Choose support mask U] --> B[Check witnesses for T = univ and I = complement U]
B --> C[Bound witnesses by sum of capacities over U]
D[Arbitrary I subset T] --> E[Set U = T minus I]
E --> F[Original witnesses are included in complement witnesses]
C --> G[Original frame inequality]
F --> G
Reviews (2): Last reviewed commit: "Reduce frame validation to complement ma..." | Re-trigger Greptile
Proof profile (new / modified Lean files)Statement changes
|
| File | Δ lines | HB base | HB head | Δ HB | Δ HB % | Wall base (s) | Wall head (s) |
|---|---|---|---|---|---|---|---|
LeanPool/FrontierMathOpenHypergraphs/Uniform/FrameBoosters.lean ⚠ |
+44/-282 | 164 | 8 | -156 | -95.1% | 618.06 | 6.28 |
LeanPool/FrontierMathOpenHypergraphs/Uniform/FrameExact.lean ⚠ |
+21/-21 | 44 | 2 | -42 | -95.5% | 47.26 | 6.37 |
LeanPool/FrontierMathOpenHypergraphs/Uniform/FrameResidues.lean ⚠ |
+12/-12 | 26 | 2 | -24 | -92.3% | 10.88 | 2.44 |
LeanPool/FrontierMathOpenHypergraphs/Uniform/FrameDefs.lean |
+92/-367 | 213 | 191 | -22 | -10.3% | 23.38 | 10.03 |
| Total | +169/-682 | 447 | 203 | -244 | -54.6% | 699.6 | 25.1 |
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
|
The proof-profile warning is understood and the statement changes are intentional: all affected declarations are private certificate leaves whose types now mention the replacement binary checker. The profile’s head-side 6.28s row is partial because modified A valid same-machine comparison, invoking Lean directly with each revision’s own dependency setup and writing the target artifacts to a fresh temporary directory, gives:
Both commands completed successfully. The hosted profile independently records the base at 618.06s under runner load and deterministic heartbeat totals falling 447 → 203 overall; its 3 head-side error markers are the expected cross-revision dependency limitation, not proof failures. Fresh-head Lean Action CI is green. |
|
/review |
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | checker redesign and certificate migration |
| Introduces tech debt | ✅ no |
| Maintainability | ✅ improved |
| Brittleness | ✅ more_robust |
| Risk | ✅ low |
The smaller checker, simpler two-branch soundness proof, and reduced certificate tree leave this code easier to maintain and cheaper to compile without replacing structure with opaque automation.
Tokens: 18,799 in / 1,698 out · Tier: flex · Effort: xhigh · Cost: $0.0725
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
1 participant
Summary
U = T \ I, replacingIbyUᶜpreserves the capacity side and can only add frame witnesses2^tsupport masks instead of all3^tpairsI ⊆ Trflcertificates, with nonative_decide, trust escape hatch, option change, or resource-limit increaseThe change removes 682 lines and adds 169.
FrameBoosters.leanshrinks from 350 lines to 113 while keeping only private staged certificate leaves plus one general public combination theorem.Validation
lake build LeanPool.FrontierMathOpenHypergraphslake exe lint-styleon all four changed moduleslake exe runLinteron all four changed modulesgit diff --checkProof profiling reports 447 → 203 deterministic heartbeat units (-54.6%) and 197 → 74 declarations. Its head-side file rows are partial because the profiler measures modified files against base dependency oleans, where the new checker does not exist. A valid same-machine direct Lean comparison with each revision’s own dependencies and fresh target outputs gives
FrameBoosters265.18s → 84.16s wall (-68.3%) and 702.30s → 218.21s user CPU (-68.9%); both runs completed successfully. Current-head LLM review approves with no tech debt, improved maintainability, greater robustness, and low risk; current-head Greptile gives 5/5 with no findings.