From afeda7aa2859e819caf0eaf442ea80b7f7a35dd2 Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 23:38:47 -0500 Subject: [PATCH] fix(lean): expand bare TODOs in GeometricCompressionWorkspace and NGemetry Replace terse -- TODO(lean-port): stubs with one-line descriptions of the deferred proof/example 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> --- .../Semantics/Semantics/GeometricCompressionWorkspace.lean | 4 ++-- 0-Core-Formalism/lean/Semantics/Semantics/NGemetry.lean | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/GeometricCompressionWorkspace.lean b/0-Core-Formalism/lean/Semantics/Semantics/GeometricCompressionWorkspace.lean index 512e2d45..6dce437b 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/GeometricCompressionWorkspace.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/GeometricCompressionWorkspace.lean @@ -205,7 +205,7 @@ def lowRankCollapseTemplate (rank : Nat) : CollapseOperator := (embedToSurface2D (codingFromRatio 9 10 "end") "end") rank (codingFromRatio 95 100 "phi_0.95")], - collapse := fun coord => coord.x -- TODO: LLM implements actual collapse + collapse := fun coord => coord.x -- TODO(lean-port): Compute low-rank projection of SurfaceCoordinate (x, y, z) onto a single CodingAtom using the basis perturbation directions and rank constraint } -- ═══════════════════════════════════════════════════════════════════════════ @@ -642,7 +642,7 @@ def runAdversarialTrial -- §10 THEOREMS -- ═══════════════════════════════════════════════════════════════════════════ --- TODO(lean-port): Theorem projectionOrdering +-- TODO(lean-port): Theorem projectionOrdering — projectToCoding preserves strict ordering: for positive SourceValue pairs s1 < s2, their CodingAtom Q0_64 values satisfy (projectToCoding s1 max).value < (projectToCoding s2 max).value via monotonicity of Q0_64.ofRatio -- Projection preserves ordering for positive values. -- Proof relies on ofRatio preserving ordering for positive args. -- theorem projectionOrdering (s1 s2 : SourceValue) (max : Q16_16) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/NGemetry.lean b/0-Core-Formalism/lean/Semantics/Semantics/NGemetry.lean index 7df567ba..81d79dc2 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/NGemetry.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/NGemetry.lean @@ -311,7 +311,7 @@ theorem zeroVectorMagnitude (_n : Nat) : let v2 := VectorND.fromArray (#[Q1616.ofNat 4, Q1616.ofNat 5, Q1616.ofNat 6]) 3 VectorND.dot v1 v2 -- Expected: dot product --- TODO(lean-port): Add n-dimensional camera orientation example --- TODO(lean-port): Add n-dimensional depth ordering example +-- TODO(lean-port): Add #eval witness for computeCameraOrientationND applied to two CameraPoseND 3 poses, showing the resulting VectorND 3 direction between them +-- TODO(lean-port): Add #eval witness for computeDepthOrderingND sorting an Array of BoundingHyperbox 3 by Euclidean distance from a camera PointND 3, returning the depth-sorted index permutation end Semantics.NGemetry