SPATIAL-2: units grounding, signed components, affine space, exact Euclidean geometry

[gunbai-bot]

Follows #8086 (SPATIAL-1). Branched from main, not stacked, since affine space does not depend on the epistemic layer.

Merged to current main on 2026-08-11.

The correction this implements

"Can a measurement be negative" was the wrong question. A length is never negative; a coordinate and a displacement are, in different senses. So Millimeter stays Nat-backed and is not widened — a wall of length −3 m remains unwritable. What was missing was never a signed length; it was the affine layer that says what a signed spatial number means, and an honest account of what a finite machine can compute about one.

One signed component, not two

MillimeterCoordinate and MillimeterDisplacementComponent were both spelled Measure<Length, Milli, Int> — the same structural type under two names, implying a distinction the typechecker did not carry, in work whose subject is that distinction. They are now one SignedMillimeterComponent.

The affine distinction lives where it belongs: in Point3<F> / Vector3<F> and their operations.

Point + Vector   -> Point
Point - Point    -> Vector
Vector +- Vector -> Vector
Point + Point    -> no operation exists

Frames ride as phantom type parameters, so cross-frame subtraction does not typecheck.

Frames are right-handed orthogonal Cartesian, full stop. Handedness/LeftHanded and the CoordinateFrameDescriptor are deleted: LeftHanded was writable while every operation was unconditionally right-handed and nothing read the descriptor.

Transform3 is now ZQuarterTurnTransform3 — it rotates about +Z only, and no X/Y rotation was added to make a broader name true.

The mathematics is exact; the finite machine realization may refuse

The largest correction. norm_squared3, dot3 and cross3 were documented "total and exact" while running on i64, where a vector a few million millimetres long has no representable squared magnitude. And int_to_nat_nonnegative clamped negatives to zero directly beneath a comment saying that clamping would fabricate an answer.

std.checked_arithmetic is the new single home for the bound: add / subtract / multiply / negate as pre-checks — the decision happens before the operation, so nothing inspects a product the machine already wrapped — returning a typed IntegerOverflow cause naming the operation and its operands. One declared i64 bound replaces the six literals that were open-coded inside std.induction's own checked ops, which are deleted in favour of the authority.

It is not in std.integer because std.integer imports std.induction and the import graph's one structural law is acyclicity; the module records that and its dissolve-on.

Every spatial operation that can cross the bound now answers SpatialArithmeticResult<T> and carries the cause verbatim. int_to_nat_nonnegative is gone; its replacement refuses the one unrepresentable magnitude and fabricates nothing.

norm3 keeps two failure kinds apart deliberately — the machine bound outside, the kernel's unresolved root inside — because their remedies differ.

Result standing, named for the kernel rather than the mathematics

Was	Now	Why
LengthExactRootNotRecognised	LengthRootUnresolvedInExactKernel	for (1,1,0) there is no exact integer root to fail to recognise
DirectionNotAxisAligned	DirectionUnresolvedInAxisKernel	(3,4,0) has the exact rational direction (3/5,4/5,0); approximation is not the only remedy

axis_direction_of is deleted and inlined into its guarded branch. It answered PositiveZ for the zero vector and PositiveX for (1,1,0) to any caller, safe only because its one call site happened to be guarded and its precondition lived in a comment.

Units

Conversions take SquareMeter / CubicMeter / Degree / Turn instead of a bare Nat — the one boundary where a unit changes was the one place an undimensioned number was accepted.

MilliSquared and MilliCubed are deleted: they were Micro and Nano under second names, one decimal factor spelled twice, and every Scale fold had grown two arms answering what an existing arm already answered. Scale is the decimal factor; the alias names the unit.

extdeps.units.iso_80000_3

Pinned: ISO 80000-3:2019 (catalogue 64974), amended by Amd 1:2025 (87100), so the amendment is a second citation of one subject rather than a second subject. Evidence standing is stated rather than implied: iso.org returns HTTP 403 to this environment, so the normative text has not been read here and no claim rests on its wording; what was verified is the designation-to-catalogue mapping. The relations carried are definitional and independently checkable.

The module now carries extdeps_model_scope and joins scope_carrier_paths — required by the external-model-scope gate that landed on main while this branch was dormant.

The "turn is the exact canonical unit" policy moved to std.measure, where the decision is actually made; the BIPM attribution is named as a separate subject rather than an uncited aside.

Evidence

Both witnesses green by execution, and the arithmetic evidence is new:

• nine operation-level refusal claims, each asserting which operation crossed — the dot product's sum refuses as an add, not a multiply, because both products fit and the total does not
• the operands travel with the cause
• a positive control proving the boundary is exactly where it is (the maximum is reachable; one past it is not), so a uniformly-refusing implementation cannot pass
• every ready-side claim asserts through a match that makes a refusal false

Regen is at a fixed point (regen_divergence_count=0, --verify clean), all seven partition crates check, and cargo check --workspace --all-targets passes.

Known open — finding 8, with a measured reason

The type walls (Point+Point, cross-frame subtraction, AreaVector3 as a displacement, magnitude as component, wrong transform frame) still have no executing negative control. The intended harness, compile_dag_diagnostic_census, was tried and cannot serve: it compiles synthetic source against a witness-root module index that does not resolve corpus imports — a probe importing a single real module yields 82 blocking diagnostics, identical to one importing the whole spatial surface. Inlining copies of the carriers into the fixture would test the walls of a copy, not of these types, so no witness was shipped rather than a fake control. Closing this needs either the harness's roots extended or a different mechanism, and that is its own increment.

Scope

Not attempted: LineSegment, Plane, Polygon, Surface, Opening, SpatialSolid, EnclosedSpace, topology, placed objects, rendering. Those are SPATIAL-3 onward, which stays parked behind a real dependency: a sound affine substrate precedes sound topology.

History

Frozen 2026-08-10 for portfolio sequencing, then unfrozen by operator override because concrete spatial consumers exist (compute-fabric owes MountedTo, RequiresClearance, PhysicalRoute, PotentialFlow and containment to this kernel).

[gunbai-bot]

Pushed ec2d9a6 addressing review 50860 and the relayed dimensional review. All five blockers were real; four were live defects rather than naming issues.

1. dot3 erased its dimension. A millimetre times a millimetre is a millimetre squared, and it returned a bare Int. Now SignedSquareMillimeter — sign retained, because a negative dot product means the displacements point away from each other.

2. cross3 returned Vector3<F>, whose components are millimetre displacements. So the numbers were areas wearing a length type, and translate_point3(point, by: cross3(a, b)) typechecked — a cross-product area consumed as a physical translation. New AreaVector3<F> carrier, deliberately not an alias of Vector3: sharing three numeric components is not sharing a dimension. Same class in normalize3, which returned ±1 millimetre components — a one-millimetre displacement, not a direction, and translating by it moved the point 1 mm. It now returns AxisDirection3<F>, the six directions integer arithmetic represents exactly, carrying no magnitude at all.

3. The scale conflation, and the serious one. Milli => -3 is a real fold arm in scale_decimal_exponent, so Measure<Area, Milli, Nat> asserted 10⁻³ of the base area unit. That is false — square millimetres are 10⁻⁶ m² — and the type stated a wrong fact regardless of the comment beside it. Added MilliSquared (-6), MilliCubed (-9), ArcsecondAngle and TurnAngle across all three Scale folds and retyped the carriers.

4. LengthRequiresApproximateRealization overclaimed. It is false for (3, 4, 0), whose magnitude is exactly 5: approximation is not required, this slice simply has no integer square root to recognise a perfect square. Renamed LengthExactRootNotRecognised — naming a limitation of the code as a property of the problem is the same class as reporting a rung the executed evidence does not establish. Same rename for the direction arm.

5. The ISO anchor. Review reports the numeric locator names Part 2 and that the 2006 edition is withdrawn. I could not verify either — iso.org returns HTTP 403 to automated fetches — so I removed the locator rather than correcting it on a guess: an unverifiable catalogue id that may name the wrong standard is worse than none. The designation is now the citation (§3 cite-the-symbol; a catalogue id is a second positional naming scheme, and the positional one is what rots). Edition is deliberately unstated, which costs an edition-sensitive claim against this module until a pin lands. The relations carried are not edition-sensitive — a turn is 360 degrees by definition of the degree — which is why they were safe ahead of the pin.

Review 50860's two findings are in the same push: degrees_per_turn is no longer duplicated (extdeps.color.srgb derives full_turn_degrees from it, the literal 360 is gone), and std.measure derives its conversions from the cited module rather than floating.

On the evidence, stated at the scope it has. The 10 witnesses in affine_space_witness_test.dag and 4 in spatial_units_witness_test.dag are green by execution, including a hue-wrap regression control on the srgb change. But the dimensional walls above are type errors — the expressions that erase a dimension do not compile — so there is no runtime RED that can exercise them, and I have not enrolled a negative-compile harness. The claim is therefore: those erasures are unwritable, established by the carriers being distinct types, not by an executed refusal.

— sent from deep-fox-168