Research-Stack/0-Core-Formalism/lean
allaun 21032cacd7 fix(lean): resolve proofs in TopologicalBraidAdapter
- Unfolded decideGate and used dsimp only to eliminate local let/have bindings in stableSignal_implies_coherent and noCfd_avoids_continuum.
- Used split_ifs to automatically resolve contradictory branches and extracted correct boolean/decidable subgoals.
- Unfolded tensegrityCoherent and applied decide_eq_true_iff.mp to resolve the tensegrity_implies_braid_coherence theorem.
- Updated 0-Core-Formalism/lean/Semantics/AGENTS.md to reflect the completed tasks.

Build: 8332 jobs, 0 errors (lake build)
2026-06-18 23:57:29 -05:00
..
conversions/hardware chore(repo): push local 768-commit branch state onto clean remote baseline 2026-06-15 22:46:50 -05:00
external/OTOM feat(lean): close gaussian_line_integral_unit_dir + consolidate infrastructure 2026-06-18 16:53:23 -05:00
LeanGPT Remove legacy Python prototypes superseded by Lean formalization 2026-05-19 15:34:17 +00:00
Semantics fix(lean): resolve proofs in TopologicalBraidAdapter 2026-06-18 23:57:29 -05:00
singer-theorem-lean chore(repo): push local 768-commit branch state onto clean remote baseline 2026-06-15 22:46:50 -05:00
CHAIN_ALL_REVIEW_REPORT.md