| name | pep-full-proof |
| description | Find tight PEPFlow performance guarantees with explicit full-PEP dual certificates, sparse lambda structure, S matrices, and algebraic proof state. Use when the user asks for /pep-full-proof, pep-full-proof, Block 2, full PEP proof, sparse dual certificates, or generating examples_peppy/{ALGO_NAME}/state/{ALGO_NAME}_b2.json from examples_peppy/{ALGO_NAME}/state/{ALGO_NAME}_b1.json. |
PEP Full Proof
Quick Start
Read references/workflow.md, then execute it as the authoritative Block 2 workflow.
Use the algorithm name from the user request or from examples_peppy/{ALGO_NAME}/state/{ALGO_NAME}_b1.json. Keep the workflow's dense solve, sparsity detection, relaxed solve, and symbolic verification phases intact.
Codex Adaptation
- Load
examples_peppy/{ALGO_NAME}/state/{ALGO_NAME}_b1.json first and confirm algo_name, obj_tag, params_json, N_verify, and conjectured_rate.
- Use
.venv/bin/python3 for Python calls when available.
- When displaying matrices, summarize the nonzero or structurally important entries instead of dumping huge tables unless the user asks for full output.
- In proof notebooks, use
pf.pprint_labeled_matrix(...) for proof-bearing matrices such as candidate lambda formulas, S candidates/decompositions, Lyapunov coefficient matrices, and proof residuals; summarize raw dense/relaxed certificate matrices unless full tables are requested.
- Store durable output in
examples_peppy/{ALGO_NAME}/state/{ALGO_NAME}_b2.json; later Lyapunov skills depend on the same keys.
- Avoid system-level temporary directories; store dense/relaxed solver outputs and scratch JSON under
examples_peppy/{ALGO_NAME}/state/.
- Treat near-zero dual entries carefully: state the tolerance used and rerun verification after imposing sparsity.
- Before using LDL for the Gram certificate
S, inspect any existing examples_peppy/_references/{ALGO_NAME}/ notebook/module for verified S_guess, S_piece, square-term, or rank-profile constructions; adapt those proof-specific decompositions into S_code and, when possible, named pieces for Block 3.
- If the numerical certificate disagrees with the conjecture, pause the proof workflow and diagnose the setup, parameters, and relaxation before proceeding.
Related Skills
Run lyap-define next for Block 3, or use pep-analyze for the combined analysis flow.
