Ranking geometry made machine-checkable
A source-audited Lean 4 formalization of the geometric core of planar ranking elicitation with pairwise queries.
Known items are points and an unknown user preference is another point. Comparing two items reveals which side of their perpendicular bisector contains the preference point.
The formalization connects distances, halfplanes, ranking predicates, profile consistency, one-dimensional structure, and concrete examples.
The tight planar worst-case query bound remains open. The repository presents the verified geometric foundation without claiming to close it.
where the effort went
the numbers
built with
delivery record
I wanted a precise foundation for an open ranking-elicitation problem where informal geometric intuition can easily hide degeneracies and tie cases.
Euclidean distance and pairwise preference definitions
Bisector-halfplane characterization of comparison answers
Ranking and multi-user profile consistency predicates
One-dimensional structural results
Concrete verified examples and source audit notes
The constraints mattered as much as the finished interface.
after shipping
Geometry becomes a better algorithmic interface when boundaries and ties are represented explicitly.
A useful formalization can map the terrain of an open problem without pretending to solve it.