src/kernel/Anytype/Core/Conversion.idr:34 decides conversion as structEq (normalise s) (normalise t) — correct shape, but there is no soundness/completeness theorem connecting it to declarative conversion (ET-2), and no adequacy statement vs the intended model (ET-3). systemet's MECH-1 (Lean, PR #17) has the totality core + stability landed and records the exact remaining statements (defEq_iff_nf, decDefEq) as OPEN; when they land, this kernel should pin and cite them, or discharge its own Idris2-side proofs. Cites: ET-2, ET-3.
🤖 Generated with Claude Code
src/kernel/Anytype/Core/Conversion.idr:34decides conversion asstructEq (normalise s) (normalise t)— correct shape, but there is no soundness/completeness theorem connecting it to declarative conversion (ET-2), and no adequacy statement vs the intended model (ET-3). systemet's MECH-1 (Lean, PR #17) has the totality core + stability landed and records the exact remaining statements (defEq_iff_nf,decDefEq) as OPEN; when they land, this kernel should pin and cite them, or discharge its own Idris2-side proofs. Cites: ET-2, ET-3.🤖 Generated with Claude Code