Bfloat16

[SmoothThunk]

liftFloatUnop was missing a case for bfloat16, so trig/transcendental ops would throw on bf16. Added | .float16 | .bfloat16 => using the shared decode/encode helpers.

[seanmcl]

Code review — bfloat16

Reviewed at high effort. Every numeric/logic claim below was verified empirically: I ran the exact functions in Lean 4.30.0 and cross-checked bit patterns and promotion/cast tables against ml_dtypes + numpy (the dep this PR adds). The core bf16 encode/decode math is sound — all eight #guard magic numbers in Float.lean match the ml_dtypes oracle, and encode/decode of finite/subnormal/inf/NaN/overflow inputs is correct. The findings are elsewhere.

🔴 Correctness

1. join regression: int16 no longer promotes with wider types — TensorLib/Dtype.lean:157

Inserting

| .uint16, .bfloat16 => none

between .int16, _ and .uint16, _ => y regroups .int16, _ into the none arm. Verified in Lean 4.30.0:

call	before	now
join int16 int32	int32	none
join int16 int64	int64	none
join int16 uint32	int64	none
join int16 uint64	float64	none
join int16 float16	float32	none

This flows into Ufunc.liftBitwiseBinop (Ufunc.lean:302); a none result makes binop return "Implicit type conversions are not supported", so bitwiseAnd/Or/Xor on an int16 tensor and an int32 tensor now errors where it previously promoted to int32 and succeeded. Suggest an explicit .int16, .bfloat16 => none arm (mirroring the uint16 one) so the fallthrough .int16, _ => y is preserved.

2. lossless int8 → bfloat16 is false but should be true — TensorLib/Dtype.lean:181

bf16 exactly represents every value in [-128, 127] (verified: empty non-exact set), and np.can_cast(int8, bfloat16, 'safe') is True. int8 → float16 is already marked true. The .uint8, .bfloat16 => true arm was added but the symmetric .int8, .bfloat16 was omitted, so it falls through .int8, _ => false.

3. bf16 npy dtype only round-trips at little-endian — TensorLib/Npy.lean:124

dtypeNameToNpyString maps bfloat16 → "V2", but the inverse special case lives only in fromNpyString and only for .littleEndian. Verified: a bfloat16 dtype with order = notApplicable serializes to "|V2" and fromNpyString "|V2" returns error "Can't parse V2 as a dtype" (same for ">V2"). Mitigated in practice because Tensor.toNpy (Tensor.lean:659) always stamps littleEndian, so first-party writes round-trip; reachable only via a manually constructed non-LE dtype. Low severity, but the asymmetry is worth a note or guard.

🟡 Correctness (doc)

4. NaN-sign comment is inaccurate — TensorLib/Float.lean:161

The comment says dropping the NaN sign bit "matches ml_dtype's bfloat16 constructor behavior." It doesn't: ml_dtypes.bfloat16(view of 0xFFC00000) encodes to 0xFFC0 (sign preserved), whereas toBFloat16Bits yields 0x7FC0 because Lean's Float32.toBits normalizes every NaN to 0x7FC00000 first. The behavior is an acceptable consequence of that upstream Lean limitation — but the comment should say it diverges from ml_dtypes because of the Lean toBits NaN normalization, not that it matches.

🟡 Test quality

5. Weak / missing arithmetic + cast tests — TensorLib/Dtype.lean:1120

Dtype.add .bfloat16 xa xb == Dtype.add .bfloat16 xb xa holds for any commutative-but-wrong add (e.g. one that ignores its inputs or rounds incorrectly), so it can't catch a bad bf16 add. And nothing exercises the ~15 new bf16 castOverflow arms at all. Consider comparing bf16 add/cast output bytes against ml_dtypes (as testBFloat16EdgeCases already does for decode).

6. Round-trip PBT NaN escape hatch — TensorLib/Float.lean:289

f.toBFloat16Bits == bits ∨ f != f: for every NaN-encoding bits, f != f is true, so the property passes without ever checking encode/decode consistency on NaN patterns.

7. Max-value assertion too weak — TensorLib/Test.lean:141

v6 > 3.0e38 passes for a huge range of values (including +inf), so it can't distinguish a correct max-value decode from a buggy one. An exact-bits check (like v0..v5) would be a real assertion.

🟢 Cleanup

8. floatVariant simplification — TensorLib/Dtype.lean:773 — the four leading if dtype == .floatXX then .floatXX branches equal if dtype.isFloat then dtype else … (verified equivalent over all 13 dtypes); the isFloat form extends to future float dtypes automatically.

9. New decode/encode helpers not reused — TensorLib/Dtype.lean:666 — decodeFloat16OrBFloat16 / encodeFloat16OrBFloat16 were added to remove exactly this duplication, but isZero (line 620) and the fp16/bf16 arms of castOverflow (lines 666, 669, 673, 676, 690, 693, 697, 700, 703, 713) still open-code the decode ~10 times.

10. Duplicated comment + typo — TensorLib/Dtype.lean:159 — the np.result_type(np.int16, m.bfloat16) comment is pasted on both lines 155 and 159; the second copy has a stray space: result_type( np.int16.

---

_{Also checked and refuted (no action needed): toBFloat16Bits top == 0xFFFF wrap-to-zero and "NaN → inf/zero" — impossible, since the only fp32 inputs with top == 0xFFFF are NaNs and Lean normalizes NaN toBits to 0x7FC00000 before the shift, so every NaN encodes to a valid bf16 NaN 0x7FC0; castOverflow reaching impossible — enumerated all 156 non-equal dtype pairs, none reach it; join bfloat16 + bool/int8/uint8 — correctly return bfloat16.}

[SmoothThunk]

Correctness:

1. Added int16, _ => y inside join so it doesn't incorrectly fall through to none.
2. Added .int8, .bf16 to the lossless true list.
3. Added comment explaining asymmetry in fromNpyString

Correctness (doc):

4. Fixed comment saying ml_dtypes preserves sign of NaN.

Test Quality:

5. Added arithmetic test cases comparing output bytes against ml_dtypes results. Also added casting tests (bf16->f32, bf16->int8, fp32->bf16, fp16->bf16, -0->bool, inf->f32) comparing output bytes against ml_dtypes.
6. NaN bits can't round-trip because Lean's Float32.toBits normalizes all NaN to 0x7FC00000 before we see them. The escape hatch is intentional; I dont think there's no way to test NaN round-trip through Float32 in Lean. I've added a comment on the PBT as a note.
7. Replaced v6 > 3.0e38 with bit check.

Cleanup:

8. Called isFloat inside floatVariant to reduce code duplication. Note that bf16 will be caught in the if block which correctly remains unchanged.
9. Called helpers inside isZero for fp16 and bf16. Also rewrote castOverflow to call helpers and reduce duplicate code in fp16/bf16 cases.
10. Removed extra space in comment and fixed 2nd comment to reflect np.uint16 instead of np.int16

[SmoothThunk]

Code Review Findings

Bug: join commutativity violation (Dtype.lean:157)

join(.int16, .float16) returns .float16 but join(.float16, .int16) (line 131) returns .float32. Both have itemsize = 2 so the swap guard doesn't fire, and the wildcard | .int16, _ => y catches it incorrectly. NumPy's np.result_type(np.int16, np.float16) returns float32.

This means int16 values > 2048 silently lose precision when promoted to float16, and binary ops give different dtypes depending on operand order.

Fix: add explicit patterns before the wildcards:

      | .int16, .bfloat16 => none
      | .int16, .float16 => float32   -- add this
      | .int16, _ => y
      ...
      | .uint16, .bfloat16 => none
      | .uint16, .float16 => float32  -- add this
      | .uint16, _ => y

Same issue exists for uint16 at line 161.

Minor / Cosmetic

• Dtype.lean:749 — Stale comment says "we don't have all the types available in NumPy (e.g. float16)" but float16 is fully supported now.
• Dtype.lean:631 — Leading space on def castOverflow (every other def starts at column 0).
• Test.lean:183 — Typo: -< should be ->.
• Test.lean:194 — 3-space indent on comment where rest of block uses 2.

[SmoothThunk]

Fixes for PR:

1. Added | .int16, .float16 => float32, | .uint16, .float16 => float32  before catch all guard in join.
2. Updated comment on line 750
3. Removed leading space from castOverflow function definition
4. Fixed typo to ->
5. Removed extra indent in comment line 194

[SmoothThunk]

Re-review after fix commit (905743c)

All previously flagged issues have been addressed. The branch is clean:

• Join commutativity — fixed with explicit | .int16, .float16 => float32 and | .uint16, .float16 => float32 patterns. Verified symmetric for all same-itemsize pairs.
• Leading space on castOverflow — fixed.
• Stale float16 comment — updated.
• Test typo and indent — fixed.

No new issues found. LGTM.

[seanmcl]

Reviewed the revision (max-effort pass: 10 finder angles + a verification pass, with the numeric/join/npy claims checked by running the actual logic in Lean 4.31 and against real ml_dtypes/numpy). This is a big step up from the previous cut — I verified that all four issues from the earlier review are genuinely fixed:

• ✅ isFloat now includes .bfloat16 (Dtype.lean:108) — the bf16 -0.0→bool and bitwise-op bugs are gone.
• ✅ join bf16 rows are now commutative and match ml_dtypes (bf16+int8/uint8 → bfloat16 via the itemsize-swap; bf16+{int16,uint16,int32,int64,float16} → none, which matches ml_dtypes raising DTypePromotionError; bf16+float32/64 → float32/64).
• ✅ npy V2 gate is correct: I confirmed ml_dtypes bf16 writes on-disk descr <V2 (littleEndian) while every genuine numpy void array writes |V2 (byteorder normalizes to |), so nameStr == "V2" && order == .littleEndian is exactly the right discriminator. The comment is accurate.
• ✅ castOverflow refactor is byte-for-byte behavior-preserving (checked all 24 from/to pairs; the helper wiring passes fromDtype to decode and toDtype to encode correctly), and floatVariant's one-liner is equivalent to the old chain for all 13 dtypes.

One new correctness regression

join .int16, _ => y overshoots for signed×unsigned (Dtype.lean:158).
The old code had | .int16, _ fall through to none (safe refusal). Changing it to => y correctly fixes int16+int32/int64/float16, but it now returns the wrong dtype for the unsigned-wider pairs. Verified against np.result_type:

pair	PR join	numpy
int16, uint32	uint32	int64
int16, uint64	uint64	float64

join feeds Ufunc.liftBitwiseBinop (Ufunc.lean:302), so bitwiseAnd/Or/Xor on an int16 and a uint32 tensor now silently computes in uint32 — truncating/misinterpreting values that need int64 — where it previously errored. Suggest restricting the new arm to the cases numpy actually promotes, e.g. | .int16, .int32 | .int16, .int64 => y and letting the signed×unsigned-wider pairs fall to none (same shape as the .bfloat16 handling right above). Note the pre-existing .int8, _ => y arm has the identical latent bug (int8+uint16 → uint16, numpy says int16); worth fixing in the same pass.

Pre-existing, surfaced by this change (not blocking, but the PR touches the surface)

• bf16→integer cast of negative / inf / NaN diverges from numpy (Dtype.lean:666,673). These route through Float32.toNat/toInt, which clamp negatives to 0 and inf to UInt64::MAX (verified: (-1.5)→0, inf→2^64-1, NaN→0), whereas numpy gives 255/INT_MIN/etc. Same for fp16/fp32/fp64 — pre-existing — but the new cast test c13 only covers the in-range +42 case, so it gives false confidence over the cast matrix. Consider a negative/inf case.
• toFloat32Tree/toFloat64Tree panic on 2-byte floats (Tensor.lean:597,603): they decode every element with Float32.ofLEByteArray! (needs 4 bytes) / Float.ofLEByteArray! (needs 8), so printing/inspecting a bf16 (or fp16) tensor via these panics. Pre-existing and Tensor.lean isn't in this diff, but bf16 is a second 2-byte float landing in the same hole.

Cleanup / robustness (optional)

• Redundant double-dispatch (Dtype.lean:470-478): decode/encodeFloat16OrBFloat16 match the dtype, then delegate to byteArrayToFloat16/byteArrayToBFloat16 which re-match the same dtype (dead _ => .error arm). The helpers could call the pure kernels (UInt16.toFloat32FromFloat16 / Float32.toFloat16Bits) directly. Correct as-is, just two dispatch layers for one operation.
• Test wiring (Test.lean:202): the terminal return c0 && c1 && … && c17 is hand-maintained — add a cN and forget the && cN and the assertion is silently dropped. A small checkBits (label) (expected : UInt16) (act : Err ByteArray) : IO Bool fold over a list would make the conjunction automatic and collapse the ~11 near-identical c7..c17 blocks. Also stray triple/quad blank lines at Test.lean:200-206.
• Test hermeticity (Test.lean:109): the bf16 npy test shells out to .astype(ml_dtypes.bfloat16), and saveNumpyArray (Test.lean:28) discards the subprocess result (let _output <-) without checking the exit code — so a missing ml_dtypes surfaces as an opaque downstream "file not found" rather than a clear skip/failure. A hermetic #guard Npy.Dtype.fromNpyString "<V2" == .ok { name := .bfloat16, order := .littleEndian } (plus a |V2→not-bf16 case) would pin the parse contract independent of the Python toolchain.
• Doc parity (Float.lean:104-153): toFloat16Bits has the same NaN-sign non-preservation as toBFloat16Bits (both read the sign from f.toBits, which Lean canonicalizes), but only the bf16 encoder documents it now.

Verified and not an issue

I checked and cleared several plausible-looking concerns by running them: every c6..c17 test constant is numerically correct; the top + 1 carry in toBFloat16Bits cannot wrap to +0.0 for a negative NaN (Lean canonicalizes NaN to 0x7FC00000, so bits >>> 16 maxes at 0x7FC0); and the ==-on-Float32 test comparisons are safe (NaN cases correctly use !=).

[seanmcl]

One more join case worth folding into the same fix, since this PR's title is "fix join commutativity" — it's still non-commutative (and wrong) for bool × int8/uint8 (Dtype.lean:147-151):

pair	PR join	numpy result_type
join int8 bool	bool	int8
join bool int8	int8	int8
join uint8 bool	bool	uint8
join bool uint8	uint8	uint8

join int8 bool hits .int8, _ => y → bool (wrong), while join bool int8 hits .bool, _ => y → int8 (right), so the result flips with argument order and one direction disagrees with numpy. Same reachability as the int16 case above (Ufunc.liftBitwiseBinop). It's the same root cause as the pre-existing .int8+unsigned issue I mentioned — the bool/int8/uint8 size-1 arms decide by match order because the itemsize-swap never fires when both operands are 1 byte. An exhaustive 13×13 commutativity sweep shows these four bool×{int8,uint8} pairs are the only remaining non-commutative ones, so pinning bool (| .bool, .int8 | .int8, .bool => int8, likewise uint8) would close out the commutativity goal.

[SmoothThunk]

Fixes for PR Revision:

• Join: Replaced |.int16, _ => y with cases for each promotion target and remaining non-promotable pairs fall to none. Similarly in int8, added explicit cases for int8, uint16; int8, uint32; int8, uint64 before the catch all. Also added explicit | .int8, .bool => int8 and | .uint8, .bool => uint8 cases so both directions agree with numpy's type.

Pre-existing / not blocking:

• Added tests for bf16 -1.5 and +inf -> uint8 to cover edge cases. The negative cast gives 0 (npy gives 255 via wrapping). Inf case matches npy.
• Panic on 2 byte floats: Fixed; Added dtype checks in toFloat32Tree and toFloat64Tree so fp16 / bf16 tensors decode through their 2-byte decoders instead of crashing.

Cleanup:

• Removed the double dispatch -- decodeFloat16OrBFloat16 and encodeFloat16OrBFloat16 now call the conversion functions directly (UInt16.toFloat32FromFloat16, Float32.toFloat16Bits, etc.) instead of going through intermediate wrappers that re-matched the same dtype.
• Test wiring: Refactored both testFloat16EdgeCases and testBFloat16EdgeCases to use mutable checks list and a shared checkBits helper. This avoids writing c0 && c1 && ... && cN chain — each check appends to the list and checks.all id folds at the end. Removed extra blank lines before return statement.
• Hermeticity: saveNumpyArray now checks the subprocess exit code and throws a clear error with stderr if Python fails. Also included hermetic #guard tests in Npy.lean that pin <V2 -> bfloat16 and |V2 != bfloat16 without needing Python.
• Doc: Added the NaN sign non-preservation comment to toFloat16Bits.

[SmoothThunk]

Code review findings (recall-biased, high effort):

1. Tensor.toFloat32Tree/toFloat64Tree silently swallow decode errors — TensorLib/Tensor.lean:598,607

The new float16/bfloat16 branches use .toOption.getD 0, which substitutes 0.0 when decoding fails instead of propagating the error. The enclosing do already returns Err, so this can and should be threaded through:

| .float16 => t.mapM (fun b => Dtype.byteArrayToFloat16 .float16 b)

Failure scenario: A Tensor with dtype = .float16 but a mis-sliced view (e.g. a corrupt .npy or a chunk that isn't 2 bytes) will produce a Format.Tree filled with 0.0 for the bad elements — callers see plausible-looking data with no signal that anything went wrong.

2. saveNumpyArray leaks temp files on Python failure — TensorLib/Test.lean:25-32

The new throw $ IO.userError ... path fires after IO.FS.createTempFile created a file but before any cleanup:

let (_root_, file) <- IO.FS.createTempFile
...
if output.exitCode != 0 then throw $ IO.userError s!"..."   -- file never removed

On any machine without ml_dtypes installed, each test run leaks a temp file. Consider try/finally or removing the file before throwing.

3. checkBits indented inconsistently — TensorLib/Test.lean:35

Every other top-level def in the file is at column 0, but checkBits is indented two spaces. Small nit but it breaks grep '^private def' and formatter expectations.

4. Dead let mut pass := true — TensorLib/Test.lean:59

pass is assigned true, then immediately overwritten by pass := v0 == ... before it's ever read. Either drop the initializer (declare pass at first use) or match the style used in testBFloat16EdgeCases (line 152+), which uses let pass := ... per case with no mut.

5. Quadratic list append checks := checks ++ [pass] — TensorLib/Test.lean:65+

Repeated ~20 times across testFloat16EdgeCases and testBFloat16EdgeCases. Each ++ [x] traverses the whole list, so building the list is O(n²). Negligible at n≈20 but the copy-paste pattern is worth fixing once: checks := pass :: checks (order doesn't matter for checks.all id).

---

The join additions, the castOverflow refactor, the shared decodeFloat16OrBFloat16/encodeFloat16OrBFloat16 helpers, and all the ml_dtypes bit patterns in the new arithmetic assertions (16512=4.0, 49024=-1.0, 16496=3.75, 16154=0.6, 16320=1.5, 16457=3.14) all check out.

[seanmcl]

Re-reviewed after 0d51e23 ("fix acc to PR review feedback"). I built the branch at this head (Lean v4.23.0, all 208 jobs) and ran the full Lean test suite — it compiles clean and every Lean test passes (the exit-255 I saw was only the follow-on pytest not being installed locally; Test.runAllTests returned true). I also re-derived the entire join promotion table (all 169 dtype pairs) against real numpy+ml_dtypes.

Almost everything from the prior review is genuinely fixed — verified, not assumed:

• ✅ join int16 + {uint32, uint64} now correct (int64/float64); the old .int16, _ => y overshoot is gone.
• ✅ join bool×int8/uint8 now commutative and correct (int8/uint8 both orders).
• ✅ int8 + {uint16,uint32,uint64} promotions added and correct.
• ✅ toFloat32Tree/toFloat64Tree now dispatch on dtype and decode 2-byte fp16/bf16 correctly (no more ofLEByteArray! panic on those).
• ✅ Two hermetic #guards pin the <V2-vs-|V2 parse contract — I confirmed they compile and pass (a failing #guard would break the build; the build succeeded).
• ✅ saveNumpyArray now checks the subprocess exit code and fails with a clear message instead of an opaque downstream error.
• ✅ New bf16→uint8 tests document the -1.5 → 0 (clamp) and inf → 255 behavior, and the fp16 max assertion is now the exact bit pattern (0x477FE000 = 65504.0, verified).
• ✅ decode/encodeFloat16OrBFloat16 now call the kernels directly; I confirmed byte-for-byte equivalence to the prior versions.

One remaining join gap (same class as the int16 fix)

join int32 uint64 = uint64, but numpy/ml_dtypes give float64 (Dtype.lean:175, the .int32, _ => y arm).
numpy promotes every signed + uint64 to float64 (a signed value doesn't fit uint64, and uint64's top half doesn't fit int64). This commit got int8 + uint64 and int16 + uint64 right (both float64), but the int32 row was missed: int32 + uint64 falls through .int32, _ => y and yields uint64. It's reachable via Ufunc.liftBitwiseBinop (x.dtype.join y.dtype), so bitwiseAnd/Or/Xor on an int32 and a uint64 tensor silently resolves to uint64 instead of float64.

Fix: add | .int32, .uint64 => float64 before the .int32, _ => y catch-all (mirroring the .int16, .uint64 => float64 line you just added). This was the only remaining concrete-wrong entry in the full 169-pair table — everything else either matches numpy or is the library's intentional float32/float64 => none refusal.

(Related, lower severity: int64 + uint64 returns none where numpy gives float64. That's a conservative refusal rather than a wrong value, so it errors instead of silently mis-typing — but for consistency with the int8/16 + uint64 => float64 rule you added, int64 + uint64 => float64 would complete the pattern. Only the int32 case produces a wrong concrete dtype.)

Cleanup (optional, non-blocking)

• The refactor left byteArrayOfFloat16 (Dtype.lean:395) and byteArrayOfBFloat16 (Dtype.lean:459) with no production callers — each is now referenced only by its own round-trip #guard helper. So the production encoder (encodeFloat16OrBFloat16) has no dedicated encode→decode round-trip guard, and the two encoders could silently drift while the guards keep passing. Either delete the orphaned encoders and point byteArrayTo*RoundTrip at encode/decodeFloat16OrBFloat16, or add a round-trip #guard through the production path. (The two decoders byteArrayToFloat16/byteArrayToBFloat16 are still live — used in Tensor.lean and Test.lean — so keep those.)
• checkBits (Test.lean:35) is indented 2 spaces under saveNumpyArray; it compiles fine (Lean top-level private def isn't indentation-scoped) but reads as if nested — worth dedenting to column 0 for clarity.

Nice work turning this around — modulo the one int32+uint64 line, the promotion table and the bf16 surface now match ml_dtypes everywhere I checked.

[seanmcl]

One more low-severity note on the new toFloat32Tree/toFloat64Tree dispatch (Tensor.lean:598-608), plus minor test cleanup — none of this is blocking.

fp16/bf16 tree arms swallow decode errors to 0.0. The new branches decode with (Dtype.byteArrayToFloat16 .float16 b).toOption.getD 0 (and the bf16/.toFloat variants), so a decode .error is turned into a real 0.0 value — whereas the _ => catch-all in the same function uses ofLEByteArray!, which panics on a bad decode. So one function has two different failure modes (silent-zero vs. panic) and never uses its own Err return channel for a decode failure.

In practice this is latent: for a well-formed tensor, toByteArrayTree yields exactly-itemsize (2-byte) chunks, so the fp16/bf16 decode can't fail and the getD 0 fallback is unreachable. It'd only surface for a malformed/hand-constructed tensor. Since these functions already return Err, t.mapM propagating the error (the monadic style used elsewhere in this file) would be more consistent than .toOption.getD 0.

Minor test cleanup (Test.lean, all harmless): bf16Inf is bound twice with identical RHS (~L248 and ~L264 — the second shadows the first); negBf16 (~L257) duplicates negA (~L211); and let mut pass := true (~L59) in testFloat16EdgeCases is initialized to a value that's overwritten before first read — testBFloat16EdgeCases uses a fresh let pass per check, so the two are gratuitously inconsistent in style.

That's everything from my side — the int32 + uint64 join line is the only correctness item worth acting on.

[SmoothThunk]

Fixes:

• mapM vs map: Replaced .map and toOption.getD 0 with monadic map so errors propagate instead of being replaced with 0.
• Added IO.FS.removeFile before the throw so the temp file is cleaned up when python fails. Without it, every failed run leaves a temp file that isn't deleted.
• Removed let mut pass := true. Switched to shadowing in let pass per check since each is independent of the others. This is also consistent with the bfloat16 edge cases.
• Replaced checks ++ [pass] with pass :: checks for O(1) prepend instead of O(n) append.
• Join: Added | .int32, .uint64 => float64 before the catch-all. Also added | .int64, .uint64 => float64 for consistency with the int8/int16 pattern.

Cleanup:

• Fixed indentation in checkBits.
• Round-trip #guards now test the production encode/decode path. Deleted the unused byteArrayOfFloat16 / byteArrayOfBFloat16 wrappers.
• Removed duplicate bf16Inf binding and replaced negBf16 with the existing negA.

[SmoothThunk]

Two remaining findings from code review:

1. join not commutative for int64/uint64 (TensorLib/Dtype.lean:178) — join int64 uint64 returns float64, but join uint64 int64 falls through to none. Same class of bug as the int16/uint16 and float16 commutativity fixes earlier in this branch. Suggested fix:

   | .int64, .uint64 | .uint64, .int64 => float64

2. Typo (TensorLib/Tensor.lean:596) — "Errors progate" → "Errors propagate".

[SmoothThunk]

• Added | .uint64, .int64 to the float64 case and removed the redundant | _, .int64 wildcard (all its cases are either handled explicitly or caught by the size swap)
• Corrected typo in comment