formats: +0x08 is the animation length - checked against the keyframe times

The rate/duration reading of the bundle header came from the values alone, so it
was checked against something the file states independently: the keyframe `time`
fields in the placement region.

Over the 2313 bundles that have both, the largest keyframe time is <= +0x08 in
EVERY one, none exceeds it, and 444 reach it exactly. The refutation attempt is
in the same data: a large unrelated constant would bound every time too, but the
max_time/+0x08 ratio would then pile up near zero - instead it peaks at exactly
1.0 with 520 bundles. Asserted, including the shape of that histogram, so the
bound cannot later be waved through as vacuous.

Stated precisely because the units are a separate claim: what is proven is that
+0x08 is the animation length in the SAME UNIT as a keyframe's time. That the
unit is frames still rests on the values (30/60/120/1200) and on the 16.16
reading of +0x04, which stays amber - the only new evidence for it is that the
twelve 30.0 bundles cap at +0x08 = 30 while the 2843 60.0 ones reach 1440, and
twelve bundles is not a demonstration.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PMRJjbxLqZtsb5Vb7KunPE

docs/re/structures/ui-rat-layout.md

@@ -508,7 +508,7 @@ composable bundles with a real declaration table
 | offset | distinct values | reading |
 |---|---|---|
 | `+0x04` | **3** — `0x3C0000` ×2 843, `0x1E0000` ×12, `0x3C0001` ×4 | 🟡 **frame rate in 16.16**: `0x3C0000` is exactly `60.0`, `0x1E0000` exactly `30.0` |
-| `+0x08` | 22 — 30, 1200, 120, 60, … | 🟡 a **duration in frames** (0.5 s, 20 s, 2 s, 1 s at 60) |
+| `+0x08` | 22 — 30, 1200, 120, 60, … | ✅ the **animation length**, in the same unit as a keyframe's `time` — see below |
 | `+0x0c` | 170 | ❔ |
 | `+0x10` | 83 — `0x9400`, `0x9200`, `0x8212`, … | ❔ flags; bit 15 set on **91 %** of all bundles |
 | `+0x18` | **2** — `1280` ×2 829 | ✅ **design width** |
@@ -542,3 +542,40 @@ Element counts over those 2 859 bundles: **min 1, p25 1, median 2, p75 5, p95 23
 max 56**, and only **365** carry a full-screen element. The population really is
 mostly fragments, and the separation is **shape** — or which bundle references
 which, which the PAK cannot answer directly because its entries are name-hashed.
+
+
+### ✅ `+0x08` is the animation length — checked against the keyframe times
+
+The rate/duration reading came from the values alone, so it was checked against
+something the file states independently: the `time` field of the keyframes in the
+placement region (`tests/ui_header_time_disc.rs`).
+
+Over the **2 313** bundles that have both keyframe times and a non-zero `+0x08`:
+
+| | |
+|---|---|
+| largest keyframe time **≤** `+0x08` | **2 313 — every one** |
+| largest keyframe time **>** `+0x08` | **0** |
+| reaches it **exactly** | **444** |
+
+and the ratio `max_time / +0x08` peaks at **1.0** (520 bundles) rather than near
+zero:
+
+```
+tenths: 0.0→92  0.1→128  0.2→201  0.3→198  0.4→92  0.5→110
+        0.6→194 0.7→159  0.8→293  0.9→326  1.0→520
+```
+
+That histogram is the refutation attempt, and it is why the bound is not vacuous:
+a large unrelated constant would also bound every time, but the ratios would then
+pile up near zero. They peak at exactly 1.
+
+**Stated precisely, because the units are a separate claim:** what is proven is
+that `+0x08` is the animation's **length in the same unit as the keyframe `time`
+field**. That the unit is *frames* still rests on the values themselves
+(30 / 60 / 120 / 1200) and on the 16.16 reading of `+0x04`.
+
+🟡 **`+0x04` stays amber.** The one new piece of evidence is weak but points the
+right way: the twelve bundles whose rate word is `0x1E0000` (30.0) have a largest
+`+0x08` of **30**, while the 2 843 at `0x3C0000` (60.0) go up to **1 440**. Twelve
+bundles is not a demonstration, and nothing here measures a wall-clock duration.