allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-08-13 09:20:35 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(lean): expand bare TODOs in GeometricCompressionWorkspace and NGemetry

Browse source 
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>
This commit is contained in:
Brandon Schneider 2026-05-26 23:38:47 -05:00
parent 042473574d
commit afeda7aa28
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
0-Core-Formalism/lean/Semantics/Semantics/GeometricCompressionWorkspace.lean
View file

@ -205,7 +205,7 @@ def lowRankCollapseTemplate (rank : Nat) : CollapseOperator :=
(embedToSurface2D (codingFromRatio 9 10 "end") "end") (embedToSurface2D (codingFromRatio 9 10 "end") "end")
rank rank
(codingFromRatio 95 100 "phi_0.95")], (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 -- §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. -- Projection preserves ordering for positive values.
-- Proof relies on ofRatio preserving ordering for positive args. -- Proof relies on ofRatio preserving ordering for positive args.
-- theorem projectionOrdering (s1 s2 : SourceValue) (max : Q16_16) -- theorem projectionOrdering (s1 s2 : SourceValue) (max : Q16_16)

4
0-Core-Formalism/lean/Semantics/Semantics/NGemetry.lean
View file

@ -311,7 +311,7 @@ theorem zeroVectorMagnitude (_n : Nat) :
let v2 := VectorND.fromArray (#[Q1616.ofNat 4, Q1616.ofNat 5, Q1616.ofNat 6]) 3 let v2 := VectorND.fromArray (#[Q1616.ofNat 4, Q1616.ofNat 5, Q1616.ofNat 6]) 3
VectorND.dot v1 v2 -- Expected: dot product VectorND.dot v1 v2 -- Expected: dot product
-- TODO(lean-port): Add n-dimensional camera orientation 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 n-dimensional depth ordering example -- 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 end Semantics.NGemetry