Repository navigation
SPATIAL-3A: exact orthogonal geometry - #8161
Conversation
…efusal #8091 claimed that a phantom frame parameter made cross-frame subtraction fail to typecheck, and called that the stronger of the two available options. Measured on the production compile-and-run path 2026-08-11, that program compiles clean and returns 9 -- a plausible number for a question with no answer, which is the fabricated output DESIGN 5 forbids. The cause is a v1 seed limitation, not a modelling slip: the argument-position judge compares nominal HEAD NAMES, and applied type arguments live in the type node's children where every name-level comparison discards them. Point3 matched Point3, so the frames were never compared. A separate compiler PR closes the call boundary; it cannot close the producer side, because return-position conformance declines to judge record types at all pending feature:conformance-produced-type-identity. So the carried identity is the authority and the honest claim is frame consistency BY CHECKED DERIVATION, not by construction: - std.coordinate_frame mints CoordinateFrameIdentity, declaration-owned and never derived from a name or from contents (the HostResourceIdentity precedent). Recorded as the third minted-occurrence carrier in the corpus, which is evidence the subject-parameterized extraction is due -- left as a trigger rather than built here. - Phantom <F> is removed rather than demoted. Two authorities for one fact is the DESIGN 3 violation whichever is right, and the weaker one is the one the compiler cannot enforce end to end. - SpatialResult carries three arms: ready, arithmetic refusal, frame refusal. One coproduct rather than nested result types -- there is one question at the operation boundary and the causes are what differ. - The refusal names ROLES, not expected/observed: for a symmetric operation neither frame is normatively expected, so an operation identity and the required relation replace a report of argument order. - The frame check precedes the arithmetic everywhere, because operands in different frames pose no question to overflow. Green by execution, with discriminating controls: cross-frame subtraction, addition, subtraction, translation and transform application each refuse and name both frames; same-frame operations still answer (the positive sibling a refusal-only control cannot see); frame and overflow are asserted distinct in both directions; a transform's translation must be in its destination frame. The decisive one is the lying-producer control: a function handing back a room-frame value under a building-frame annotation cannot rewrite the carried frame, and the next operation refuses. Mutation-tested -- disabling a single frame guard reds the suite. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Everything here is closed under integer millimetre arithmetic -- no roots, no trigonometry, no rounding policy -- which is why the band sits before an approximate-numeric realization rather than after it. Rectilinear architectural geometry is exactly representable, so it is represented exactly, and the layer that needs a real number pays for it there. CARRIERS: Axis2/Axis3, AxisAlignedSegment2, AxisAlignedRectangle2, Plane3, AxisAlignedBox3, BoundingBox3, OrthogonalLoop2, AxisAlignedSurface3, OrthogonalPrism3, OrthogonalRotation3. THE WALLS ARE CONSTRUCTION, NOT VALIDATION. Every carrier is sole_constructor, so its record literal cannot be written and no cast reaches it from another module: the only route to a value is the mint beside it, and the mint refuses. A degenerate segment, an unclosed or self-intersecting loop, a zero-extent box and a cross-frame composition have no constructor outside this module rather than being checked by a caller who might not check. THE 24 ROTATIONS ARE 24 BY CONSTRUCTION. A rotation is fixed by the images of +X and +Y (six choices, then four perpendicular ones); +Z is DERIVED as their cross product, so orientation-preservation is not a determinant check that rejects reflections -- a reflection has no representation. Enumerating 24 variants would be a table to get wrong once and maintain forever, and storing three images concedes the reflected state is writable. TYPED REFUSALS, one per invalid state, because the remedies differ: coincident endpoints are an authoring slip, a diagonal is a limit of the exact kernel, a frame mismatch is a composition error. Extent refusals NAME THE AXIS that collapsed. TWO CARRIERS DELIBERATELY NOT MINTED, recorded rather than silently omitted: OrthogonalSegment2 and OrthogonalSurface3. In 2D an axis-aligned segment and an orthogonal segment denote the same set, as do an axis-aligned rectangle and an orthogonal surface in an axis-perpendicular plane; minting both spellings forks one concept across two authorities (DESIGN section 3). NO POLYGON BOOLEANS. Union, intersection and difference are absent, not stubbed and not approximated: rectilinear Booleans need a sweep with a canonical output ordering and a touching-edge degeneracy policy, and inventing that policy under the name `union` is how a plausible wrong region reaches a consumer. Green by execution, eight witnesses, every negative control with a positive sibling in the same witness -- a mint that refused everything would satisfy the refusal half of each pair, and that is exactly the gap that let SPATIAL-2 ship a wall which did not exist. Two controls earned their keep by failing first. The orientation control asserts a DERIVED z-image rather than that construction succeeded, and caught a sign inversion that made the identity rotation left-handed. The self-intersection control is a figure-eight whose eight edges are all axis-aligned, all adjacent pairs perpendicular, and no vertex repeated -- so nothing local to an edge distinguishes it, which is why the pairwise non-adjacent edge test exists rather than a repeated-vertex check standing in for it. Boundary convention, asserted rather than commented: touching faces are adjacent, not overlapping. Two rooms sharing a wall plane must not report as a collision. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ic loop scan Three findings from review, all confirmed against the code and all fixed rather than argued. UNREACHABLE REFUSAL VARIANTS (cursor review 51202). LoopNotClosed and SurfaceNotInPlane were declared in OrthogonalRefusal and emitted by no mint. Closure is structural -- the last vertex connects to the first by construction, so there is no unclosed loop to reject -- and a surface is a Plane3 plus a 2D rectangle, so non-coplanarity has no representation either. An unreachable arm on a refusal sum is rung inflation: a consumer reads it as a live failure mode and writes a handler for a state nothing can produce. Both deleted; the reasoning is kept as a comment beside the loop walls so the next author does not re-add them. DUPLICATED PROSE (same review). orthogonal_segment_not_minted_note restated the // block immediately above it and had no reader. DESIGN 4c is explicit that a String declaration whose sole purpose is commentary is misplaced or dead data, and two copies of one decision is the section 2/3 redundancy. The comment stays; the row is gone. CUBIC LOOP SCAN (claude review 51199 raised it as quadratic; measured worse). The loop mint read vertex i through `vertices |> skip(i) |> first`, which is linear in i. Inside a fold over all vertices that made each linear pass quadratic, and inside the NESTED fold for the pairwise edge test it made that test cubic rather than the quadratic it appears to be. The pairwise comparison is inherently quadratic and stays; the indexing was not, and that was the defect. Edges are now materialised once in a single linear pass over the vertices, with an accumulator carrying the previous vertex, consing and reversing rather than appending (concat(list, [x]) is itself quadratic). Perpendicular- ity is read off consecutive edges in one pass that carries the first edge's axis so the closing pair is compared without re-indexing. DESIGN 6's bare-minimum-cost rule is why this is fixed rather than noted: a proven quadratic fold is always fixed regardless of realized n, and "fine for architectural n" is not a time-stable fact because reuse changes n. All eight witnesses re-run green after the rework. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
All three findings verified against the code and fixed in Unreachable refusal variants (review 51202). Confirmed: Duplicated note (review 51202). Confirmed and deleted. DESIGN §4c is explicit that a
The loop scan (review 51199) — measured worse than reported, and fixed rather than deferred. You flagged On "fine for architectural n": DESIGN §6's bare-minimum-cost rule rejects that reasoning explicitly — a proven quadratic fold is always fixed regardless of realized n, because "n is small here" is not time-stable under reuse. So it was worth doing on the repo's own terms, not just prospectively. All eight witnesses re-run green after the rework. — sent from deep-fox-168 |
point2_x, point2_y and point2_same_position were each defined twice with identical bodies. The duplicates came from restoring helpers an earlier splice had over-deleted; three of the restored set had in fact survived. A duplicate-declaration scan over the module now finds none. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Fixed in Provenance, since it says something about the substrate: an earlier splice of mine over-deleted a run of helpers; when I restored them I re-added three that had actually survived. A duplicate-declaration scan over the module now returns empty, and all 8 witnesses in One correction to the review's premise, worth recording rather than letting stand: "this should fail compilation" — it does not. A duplicate top-level declaration does not refuse in this substrate; that is a known gap, and it is exactly why this reached review instead of failing locally. The duplicate was invisible to every mechanism I ran. — sent from deep-fox-168 |
… with AxisDirection3 Three findings from review 51213, all real, all fixed by construction rather than by adding a refusal arm. The prism took an extrusion_axis: Axis3 and accepted any of the three once the height was positive. OrthogonalLoop2 is a loop of Point2, whose components ARE the frame's X and Y, so extruding along X or Y was writable and geometrically undefined. The parameter and the field are deleted; Z is the only axis a 2D footprint can be extruded along, so the invalid state now has no representation instead of a check (DESIGN section 5). The surface took a Plane3 and checked only frame equality, so an XY rectangle could be paired with a Y-normal plane and mint a surface whose coordinates do not lie in its own plane. The plane is now derived from the extent's frame at the given offset. Its frame-mismatch arm went with the parameter - there is one frame in play. The lost generality is stated in-carrier with its dissolve-on: a genuinely X- or Y-normal surface needs a 2D carrier that records which plane it spans, which the parameter did not deliver, it mis-delivered. axis_direction_axis / _is_negative / _of are projections over AxisDirection3, which std.euclidean_geometry owns; keeping them here forked that authority (DESIGN section 3). They move beside the type, and Axis3 moves with them because AxisDirection3 IS Axis3 crossed with a sign - leaving Axis3 behind would have made the helpers unable to import the type they decompose. The dead cross-frame surface clause is replaced by a control that pins the new property (Z-normal, right offset, extent's frame), discriminating by execution: minting the plane with Axis3X reds it. Eight witnesses green; the four in-body annotations this work introduced are hoisted (33 hard diagnostics, down from 37, none in these files). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
All three findings in review 51213 are real and are fixed in Prism extrusion axis. Correct: any Surface plane. Same class, same fix: the plane is derived from the extent's frame at the given offset instead of supplied beside it. The frame-mismatch arm went with the parameter, since there is now one frame in play — I replaced the then-dead cross-frame clause with a control that pins the new property (Z-normal, right offset, extent's frame), and confirmed it discriminates by minting with Worth stating plainly since it is a real narrowing: this mints XY-plane surfaces only. A genuinely X- or Y-normal surface needs a 2D carrier that records which plane its coordinates span. The
Eight witnesses green. Four in-body annotations this work had introduced are hoisted (33 hard diagnostics, down from 37; none of the remainder are in these files). — sent from deep-fox-168 |
Flagged non-blocking in review 51225, but acted on: once the plane is derived there is no invalid input left for the mint to reject, so wrapping the result in OrthogonalConstruction advertised a refusal no arm could produce - the same rung inflation on the shape that the deleted LoopNotClosed/SurfaceNotInPlane arms were on the sum. The reviewer excused it as consistent with its siblings, but the siblings genuinely refuse and there is no generic consumer that the uniform shape buys anything for; every caller was paying a match for an arm that cannot arrive. The witness's success arm becomes a direct read of the minted surface (extent width preserved), discriminating by execution: expecting 4001 reds it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Took the non-blocking note in review 51225 rather than leaving it —
The witness's success arm is now a direct read of the minted surface rather than a tautological Eight witnesses green. — sent from deep-fox-168 |
…-geometry-v2 # Conflicts: # dag/std/euclidean_geometry.dag
Stacked on #8156 (base is
spatial-2b-carried-frame-identity, notmain) — it consumes the carriedCoordinateFrameIdentity. Retarget tomainonce #8156 merges.Scope
Everything here is closed under integer millimetre arithmetic — no roots, no trigonometry, no rounding policy. That is why this band sits before an approximate-numeric realization rather than after it: rectilinear architectural geometry is exactly representable, so it is represented exactly, and the layer that needs a real number pays for it there.
Carriers:
Axis2/Axis3,AxisAlignedSegment2,AxisAlignedRectangle2,Plane3,AxisAlignedBox3,BoundingBox3,OrthogonalLoop2,AxisAlignedSurface3,OrthogonalPrism3,OrthogonalRotation3.The walls are construction, not validation
Every carrier is
sole_constructor, so its record literal cannot be written and no cast reaches it from another module. The only route to a value is the mint beside it, and the mint refuses. A degenerate segment, an unclosed or self-intersecting loop, a zero-extent box and a cross-frame composition have no constructor outside this module — DESIGN §4b rung four, rather than a check a caller might not run.The 24 rotations are 24 by construction
A rotation is fixed by the images of +X and +Y — six choices, then four perpendicular ones. +Z is derived as their cross product, so orientation-preservation isn't a determinant check that rejects reflections: a reflection has no representation. Enumerating 24 variants would be a table to get wrong once and maintain forever; storing three images concedes the reflected state is writable.
What is deliberately absent
No polygon Booleans. Union, intersection and difference are absent — not stubbed, not approximated. Rectilinear Booleans need a sweep with a canonical output ordering and a touching-edge degeneracy policy, and inventing that policy under the name
unionis how a plausible wrong region reaches a consumer.OrthogonalSegment2andOrthogonalSurface3are not minted, and that's recorded in-module rather than silently omitted. In 2D an axis-aligned segment and an orthogonal segment denote the same set, as do an axis-aligned rectangle and an orthogonal surface in an axis-perpendicular plane. Minting both spellings forks one concept across two authorities (§3). A rotated rectilinear loop is a genuinely different concept and would be anOrthogonalLoop2plus anOrthogonalRotation3, not a second segment carrier.Evidence
Eight witnesses, green by execution. Every negative control has a positive sibling in the same witness — a mint that refused everything would satisfy the refusal half of each pair, and that is precisely the gap that let SPATIAL-2 ship a wall which did not exist.
Two controls earned their keep by failing first:
X × YproduceNegativeZ, i.e. left-handed.Boundary convention, asserted rather than commented: touching faces are adjacent, not overlapping. Two rooms sharing a wall plane must not report as a collision.
Gate note
The ruling's resume condition 1 — "resolved direct calls reject wrong nominal identities and wrong applied arguments" — was proven infeasible at that seam and withdrawn; see #8157 for the measurement (976 false refusals, and the finding that
Node.childrenat the argument seam holds fields and variants, not applied type arguments). Conditions 2 and 3 hold: the differential is classified and the runtime frame controls are green. This band therefore rests on #8156's checked-derivation guarantee alone, consistent with "static call-argument refusal is an additional wall, not the sole authority."