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>

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)

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