feat(math): add combinatorial maps domain with faces and dual operations (#1728) - #2030
feat(math): add combinatorial maps domain with faces and dual operations (#1728)#2030morluto wants to merge 3 commits into
Conversation
Add the combinatorial_maps domain implementing exact, bounded, deterministic combinatorial-map operations over an immutable dart/rotation representation: - face_orbits: complete face-orbit family with per-dart face assignment and the dart-successor permutation along each face - euler_characteristic: per-component and total V - E + F under the disconnected-surface convention (each component is an independent closed surface) - orientable_genus: per-component and total g = (2 - chi) / 2 for a valid orientable cellular embedding - orientation_reverse: reverse every local cyclic order with the induced face bijection (double-reversal is the identity) - connected_components: vertex, dart, and face component partition - dual_map: exact embedded dual (one dual vertex per primal face, one dual dart per primal dart, bridges become dual loops, parallel edges retained distinctly) - vertex_face_incidence: per-(vertex, face) multiplicity and boolean per-vertex face set The FiniteCombinatorialMap value parses only well-formed maps: every dart has a declared tail/head, reverse is a fixed-point-free involution exchanging endpoints, and every rotation is a cyclic order of exactly the outgoing darts of its vertex. These are value-construction invariants, not a public .check operation. Closes #1728
- Add combinatorial_maps to the root jacobian.math exports and the public API ROOT_MATH_DOMAINS contract. - Import the domain's TOOLS and ADMISSIONS in catalog/builtins.py. - Update the frozen admission baselines (KEEP 239->246, candidates 399->406) and add the combinatorial_maps schema-snapshot fragment.
36 focused tests covering: - face-orbit family completeness (every dart in exactly one face) - Euler characteristic for the 4-cycle (sphere), minimal torus cellulation, tree, disconnected components, and isolated vertex - orientable genus (sphere g=0, torus g=1, disconnected sum) - orientation reversal: double-reversal identity, Euler/genus invariance, face bijection size - connected components for single and disconnected maps - dual: vertex count = face count, dual-of-dual vertex count, primal-to-dart bijection, torus dual - vertex-face incidence multiplicity and boolean sets - well-formedness validation: rotation length, involution, fixed-point-free reverse, foreign darts, vertex-count bound - rotation successor cyclic behavior
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
morluto
left a comment
There was a problem hiding this comment.
Review verdict: blocked on representation validity and orientation reversal
1. Invalid dart indices can pass FiniteCombinatorialMap
_validate_rotation() indexes darts[dart_index] before checking that the index lies in 0..dart_count-1. Positive out-of-range values leak IndexError; negative values use Python's negative indexing and can be accepted as aliases. For a one-vertex two-dart loop, a rotation row such as (-1, 0) can pass even though dart 1 is absent as an ID; rotation_successor(map, 1) then fails because 1 is not in the row.
Require every rotation entry to be a nonnegative in-range dart ID before dereferencing it, and require the row set to equal the exact outgoing-dart set.
2. The induced face bijection under global orientation reversal is computed incorrectly
With face permutation phi = alpha sigma, reversing every rotation gives phi' = alpha sigma^{-1} = alpha phi^{-1} alpha. Therefore an old face orbit O corresponds to the new orbit alpha(O)—the reverses of its darts—not generally to a new orbit with the same dart set.
The current code searches for frozenset(new_walk) == frozenset(old_walk). A concrete sphere counterexample is the theta graph with three parallel edges:
darts = ((0,1,1),(1,0,0),(0,1,3),(1,0,2),(0,1,5),(1,0,4))
rotations = ((0,2,4),(1,5,3))Its old face sets are {0,3}, {1,4}, {2,5}; after reversing rotations they are {0,5}, {1,2}, {3,4}. No same-set match exists, so orientation_reverse() raises on this valid map. Match each old walk after applying the dart-reversal involution.
3. The claimed isolated-vertex support is absent
The value rejects every dartless map. The test named _isolated_vertex() silently substitutes a self-loop, changing E from 0 to 1 and producing two dart-boundary faces. That is not an isolated vertex. Either support degree-zero components explicitly (including their one empty-boundary face under this PR's independent-closed-surface convention), or remove the isolated-vertex claim and state the restricted category of maps.
These are core value/kernel failures. The face-orbit, Euler, genus, dual, and incidence operations should also gain cross-operation property tests after the representation is fixed; checking only dual(dual(M)).vertex_count is much weaker than a transported map isomorphism.
Deep review summaryVerdict: REQUEST CHANGES — there are core representation and orientation-reversal correctness failures. 1. Invalid dart IDs can pass validation
Validate every rotation entry before dereferencing it, and require the row set to equal the exact outgoing-dart set. 2. The face bijection under orientation reversal is wrongWith face permutation Counterexample: the theta graph with three parallel edges darts = ((0,1,1),(1,0,0),(0,1,3),(1,0,2),(0,1,5),(1,0,4))
rotations = ((0,2,4),(1,5,3))has old face sets 3. The claimed isolated-vertex support is not presentThe value rejects every dartless map. The After fixing the representation, add stronger cross-operation properties. Checking only |
Closes #1728.
Summary
Add the
combinatorial_mapsdomain implementing exact, bounded, deterministic combinatorial-map operations over an immutable dart/rotation representation. This is a direct structural mathematics layer for embedded finite graphs: a well-formed finite combinatorial map — a graph with a cyclic order of darts around each vertex — from which ordinary exact functions derive faces, Euler characteristic, orientable genus, orientation reversal, connected components, the dual map, and vertex–face incidence.Design and library choices
The domain uses a small exact permutation/orbit kernel over immutable dart IDs. No backend embedding object crosses the boundary and no planarity solver, Kuratowski search, coordinate drawing, or theorem-specific API is introduced — per the issue, the reusable object is the well-formed map itself, not a planarity certificate.
Representation (
values.py).FiniteCombinatorialMapcarriesvertex_count, a tuple of(tail, head, reverse)dart records, and one cyclic rotation row per vertex. The value parses only well-formed maps:reverseis a fixed-point-free involution exchanging endpoints;These are value-construction invariants; they are not exposed as a public
.checkoperation.Operations (
operations_module.py). All functions are deterministic and complete for accepted values — noUNKNOWN, timeout-as-mathematics, search budget, or solver outcome.face_orbits— complete face-orbit family, per-dart face assignment, and theface = reverse ∘ rotation_successordart permutation. Every dart occurs in exactly one facial walk.euler_characteristic— per-component and totalV − E + Funder the disconnected-surface convention (each component is an independent closed surface).orientable_genus— per-component and totalg = (2 − χ) / 2; exact nonnegative integer for a valid orientable map.orientation_reverse— reverse every local cyclic order and return the resulting map plus the induced face bijection. Double-reversal is the identity.connected_components— vertex, dart, and face component partition.dual_map— exact embedded dual: one dual vertex per primal face, one dual dart per primal dart, dual reversal inherited from primal reversal, dual tail/head from the two incident face sides. The dual of a bridge becomes a loop; parallel dual edges are retained distinctly.vertex_face_incidence— per-(vertex, face) multiplicity (a vertex may occur several times on one facial boundary) plus the boolean per-vertex face set.Invariances verified by tests
V, E, F, χ, gand reverses facial orientation.dual(dual(M))has the same vertex count asM.Validation
make checklint + typecheck pass; the domain imports cleanly with no catalog side effects.dual(dual)round-trip, vertex-face multiplicities, and boundary/limit cases).tests/math/, 79tests/catalog/+tests/math/public_api/+tests/dispatch/tests pass.combinatorial_mapsschema-snapshot fragment added.CLI smoke
The 4-cycle on the sphere:
V=4, E=4, F=2, χ=2, g=0✓. The minimal torus cellulation (1 vertex, 2 loops):V=1, E=2, F=1, χ=0, g=1✓.Continue this on Linzumi