From 042473574dff7d95c1f585211c0cabc5039d70af Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 23:37:26 -0500 Subject: [PATCH] fix(lean): expand bare TODOs in MathQuery and DomainKernel Replace terse -- TODO(lean-port): stubs with one-line descriptions of the deferred proof work. No code changes; comments only. Generated with [Devin](https://cli.devin.ai/docs) Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com> --- .../lean/Semantics/Semantics/DomainKernel.lean | 2 +- .../lean/Semantics/Semantics/Functions/MathQuery.lean | 7 +++---- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/DomainKernel.lean b/0-Core-Formalism/lean/Semantics/Semantics/DomainKernel.lean index ce4d246f..2e97390b 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/DomainKernel.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/DomainKernel.lean @@ -59,7 +59,7 @@ structure CellPatch where /-- Admissibility check for a patch on a cell. -/ def cellPatchAdmissible (_cell : Cell) (_patch : CellPatch) : Bool := - true -- TODO(lean-port): Define actual admissibility predicate + true -- TODO(lean-port): Define actual admissibility predicate - check deltaH/deltaS bounds and cell state constraints /-- Payload carrying both a gossip packet and a patch. -/ structure KernelPayload where diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Functions/MathQuery.lean b/0-Core-Formalism/lean/Semantics/Semantics/Functions/MathQuery.lean index fa408d45..0bdf2a5d 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/Functions/MathQuery.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/Functions/MathQuery.lean @@ -329,7 +329,7 @@ def testEntity2 : MathEntity := -- ═══════════════════════════════════════════════════════════════════════════ /-- Theorem: Subject cost is symmetric for adjacent indices -/ --- TODO(lean-port): Fix omega proof +-- TODO(lean-port): Fix omega proof - need to prove symmetry of adjacent-subject cost calculation -- theorem subjectCostSymmetric (s1 s2 : MathSubject) -- (hAdj : s1.toIdx.val + 1 = s2.toIdx.val) : -- subjectCost s1 s2 = subjectCost s2 s1 := by @@ -343,7 +343,7 @@ theorem exactSubjectZeroCost (s : MathSubject) : simp [subjectCost] /-- Theorem: Query cost is monotonic in complexity ceiling violation -/ --- TODO(lean-port): Fix proof - need to show (entity - c1) / entity > (entity - c2) / entity given c1 < c2 +-- TODO(lean-port): Fix proof - need to show monotonicity of complexity penalty when c1 < c2 < entity -- theorem complexityCostMonotonic (c1 c2 entity : Q16_16) -- (h1 : c1 < c2) (h2 : entity > c2) : -- complexityCost (some c1) entity > complexityCost (some c2) entity := by @@ -355,7 +355,6 @@ theorem exactSubjectZeroCost (s : MathSubject) : -- have h_c1_lt_entity : c1 < entity := by trans h1 h2 -- have h_c2_lt_entity : c2 < entity := by exact h2 --- TODO(lean-port): Theorem: Empty query matches all entities (zero or minimal cost) --- Fix implicit argument synthesis issue in theorem signature +-- TODO(lean-port): Theorem: Empty query (defaultQueryParams with all filters empty) yields zero cost for all entities end Semantics.MathQuery