# Hafner step 1: split and move the twenty pyramids ## The annotated recipe ```geom Start icosahedron, icosidodecahedron. # Centered, equally scaled solids in separate material assemblies. Let tetrahedra[20] be polyhedron. # Twenty slots for the placed tetrahedra. Let base_faces[20] be face of icosahedron. # Original triangular faces, ordered for connected residuals. Let triangular_faces[20] be face[3] of icosidodecahedron. # Read candidate receiving triangles. Match triangular_faces by base_faces, outward_docking into receiving_faces. # Reorder all faces; Move chooses their vertex correspondence. Point space by 0, 0, 0 into apex. # The common coordinate origin. Let residual be icosahedron. # Source material still waiting to be placed. Cycle 19 into i: # Indices 0–18: nineteen cuts, each followed by a move. Let triangle be base_faces[i]. # Original base of the next tetrahedron. Polycone space by triangle, apex into wedge. # Build the side region using the shared subroutine. Split residual by wedge into tetrahedron, residual. # Retain the entire remainder. Move tetrahedron by triangle, receiving_faces[i] into tetrahedron. # Dock outward with exact face contact. Let tetrahedra[i] be tetrahedron. # Store the moved piece's current handle. Move residual by base_faces[19], receiving_faces[19] into tetrahedron. # The last residual is already a tetrahedron. Let tetrahedra[19] be tetrahedron. # No twentieth split or empty remainder. Finish augmented_icosidodecahedron by icosidodecahedron, tetrahedra. # Stationary core and all twenty moved tetrahedra. ``` [Full construction roadmap](hafner_dissection_roadmap.md) · [Executable recipe](../../construction/examples/hafner_nineteen_splits.geom) · [Proof runner](../../construction/examples/split_move_hafner.py) `Cycle 19 into i:` performs **cut → move → verify the face contact** nineteen times. A separate final `Move` places the remaining tetrahedron without cutting. There is no endpoint conditional and no special last-iteration behavior. There are 19 splits, 20 moves, and 20 verified contacts. The dodecahedron is untouched during this step and is outside this two-solid certificate. `Polycone` is a shared recipe subroutine, defined below using ordinary geometry operations. It works for either a triangle or a pentagon; only the fixed array size changes. Indentation closes each cycle, without `End`. ```geom Define Polycone ambient by base, apex into wedge: Let sides[size(base)] be halfspace. # Allocate one fixed slot per base edge. Cycle base by j into a, b, c: # Edge a,b; next vertex c witnesses the interior. Plane ambient by apex, a, b into divider. Half ambient by divider, c into side. Let sides[j] be side. Bound ambient by sides into wedge. # Side cone only; Split supplies the base. ``` [Shared definition](../../construction/library/geometry.geom) · [Subroutine syntax](language_syntax.md#subroutines) `size(base)` reads the number of vertices and fixes the array capacity when the call begins. The subroutine constructs the side cone of a pyramid over a strictly convex base, with an apex outside its plane. It does not add a base halfspace or create material: `Split` intersects that region with the residual solid, whose boundary supplies the base. Its local names do not overwrite the caller's names. `Finish augmented_icosidodecahedron by icosidodecahedron, tetrahedra` names our descriptive target: **the icosidodecahedron with twenty triangular pyramids attached**. It is not yet the rhombic hexecontahedron; twelve pentagonal pyramids still have to be removed in step 2. The name refers to the independently defined target below, not a new fused material piece. `by icosidodecahedron, tetrahedra` specifies the stationary solid and all twenty moved tetrahedra as its constituents. The declaration checks that every live piece appears exactly once in the correct assembly; the separate proof runner verifies geometric coverage. ## Two centered solids, one growing assembly `Start icosahedron, icosidodecahedron` loads the canonical solids at the origin with the same edge length $2/\phi$, where $\phi=(1+\sqrt5)/2$. Their orientations make corresponding triangular faces parallel with the same outward direction. The two roots initially belong to **separate material assemblies**. Their coordinates overlap, but their material is counted separately. Splitting preserves the source assembly; docking moves the detached tetrahedron into the receiver's assembly. The unplaced residual therefore does not count as overlapping the receiving solid. Every piece already placed there does count. This is coordinate bookkeeping, not a claim that two physical solids can occupy the same space. `base_faces` captures the original faces in an order that keeps the residual connected. `tetrahedra` has 20 fixed slots, filled with the current handles after moving. The final certificate requires all material to have reached one assembly. ## Choosing faces and moving ```geom Let triangular_faces[20] be face[3] of icosidodecahedron. Match triangular_faces by base_faces, outward_docking into receiving_faces. Move tetrahedron by triangle, receiving_faces[i] into tetrahedron. ``` `Match` with the explicit `outward_docking` relation reorders all candidate receiving faces in the order of `base_faces`. For each source triangle it requires a **unique unused congruent triangle with the same outward normal direction**, using exact arithmetic. It rejects missing or ambiguous matches. Both arrays must have the same length, and every candidate is used exactly once. Subset selection is reserved for a future `Select` operation. This is a geometric face-correspondence rule, with no Hafner-specific sums or placement table. A triangle has several possible vertex correspondences. `Match` preserves each selected face exactly, including its vertex order. `Move` chooses a deterministic correspondence among cyclic vertex orders and their reversals, then computes a proper rigid motion placing the two pieces on opposite sides. It records the chosen correspondence for exact replay. This is a geometric choice, not a search for a collision-free orientation: if the chosen placement overlaps other pieces, the operation fails. `Add`, `Subtract`, and `Align` are no longer recipe keywords; the geometry kernel computes the motion. The receiving face remembers which live piece it belongs to. A stale or foreign receiving-piece handle is rejected. Original source faces remain usable as geometric references after the source is cut: the move checks that the referenced triangle really is the detached piece's complete exposed face. ## What gets checked For a residual $P$ and the intersection $W$ of the three selected halfspaces, splitting still means $$T=P\cap W,\qquad P'=\overline{P\setminus T}.$$ Both outputs must be nonempty and face-connected; the whole remainder is retained. This makes conservation and disjoint interiors part of the split operation. There is no separate target assertion after each cut. For a face-based move $x\mapsto Rx+t$, the checker establishes: 1. **A rigid motion:** $R^TR=I$ and $\det R=1$ exactly. 2. **The complete faces coincide:** each ordered source vertex maps exactly to its receiving vertex. Both triangles must be complete exposed faces of their pieces, not arbitrary triangles chosen in their interiors or smaller patches of larger faces. 3. **An outward contact:** the two pieces occupy opposite closed halfspaces of the common face plane. Their shared boundary is allowed; their material does not interpenetrate. 4. **No overlap with previous placements:** the moved tetrahedron is checked against all pieces already in the receiving assembly. Faces may be internally subdivided. The checker compares exact projected polygon areas and their intersections to establish equality of the full face; it does not require a triangle to appear as one unsplit mesh polygon. The original implementation supported triangular faces; [step 2](hafner_pentagonal_transfer.md) extends it to convex polygonal **supporting faces**: each whole piece must lie on one side of its face plane. A nonconvex piece can satisfy that condition, but a concave piece that wraps around the contact plane is rejected. General exposed-face contacts on such pieces need a further boundary check before we can support them safely. These contacts are implicit joins: material identities stay separate. No `Join` operation glues, merges, or discards pieces. ## The complete step 1 certificate The [saved report](certificates/hafner_step1_split_move/verification.json) records **19 splits, 20 proper nonidentity rotations, 20 checked face contacts, and 21 final physical pieces**, including the stationary icosidodecahedron. There are **210 final piece-pair checks** and **zero uncovered target volume**. The [replayable history](certificates/hafner_step1_split_move/history.json) uses `scissors-split-move-v2`. Every face-based move records its receiving piece, both ordered faces, and the exact rotation and translation. Replay reconstructs the material from the declared roots and rechecks the contact; it does not trust a producer's claim that two faces coincide. At the end, the proof checks that all material belongs to the receiving assembly and that each of its 20 triangular faces received exactly one pyramid. It also retains the independent full-region check against $$U=D\cup\bigcup_{(A,B,C)}\operatorname{conv}\{A+B,\ A+C,\ B+C,\ A+B+C\},$$ where $D$ is the icosidodecahedron and $(A,B,C)$ ranges over the centered icosahedron's faces. This formula specifies the target for the checker; it is not an instruction in the recipe. The final material is interior-disjoint, has the original total volume, and covers exactly $U$. Everything is checked with algebraic-number arithmetic, without floating-point tolerances. The trusted Python arithmetic and geometry kernels establish endpoint geometry and the recorded face contacts. They do not certify continuous collision-free paths, glue strength, or manufacturing tolerances. ## Reproduce the proof From the project root: ```sh python3 -m construction.examples.split_move_hafner --output-dir /tmp/hafner-step1 ``` This executes the displayed recipe, certifies the final assembly, then serializes and replays its history with the expected centered-solid problem fixed by the proof runner. The output directory contains `history.json` and `verification.json`, including implementation hashes. To run just the operations and their local contact checks, or inspect their Python translation: ```sh python3 -m construction.language steps construction/examples/hafner_nineteen_splits.geom python3 -m construction.language transpile construction/examples/hafner_nineteen_splits.geom --operations-only ``` `Cycle` blocks close by dedenting; `Finish augmented_icosidodecahedron by icosidodecahedron, tetrahedra` closes the program and names the expected target and its constituents without silently running the full endpoint certificate. Continue with the now-certified [step 2: twelve pentagonal-pyramid transfers](hafner_pentagonal_transfer.md).