gHashTag · gHashTag · Jul 5, 2026 · Jul 5, 2026
@@ -5,8 +5,8 @@
   "preprint": "https://arxiv.org/abs/2606.05017",
   "total_formats": 83,
   "total_packs": 83,
-  "bitexact_packs": 70,
-  "selfconsistent_packs": 5,
+  "bitexact_packs": 71,
+  "selfconsistent_packs": 4,
   "structural_packs": 8,
   "packs": [
     {
@@ -388,9 +388,9 @@
     {
       "id": "gf96",
       "file": "gf96_conformance_v0.json",
-      "kind": "bitexact_selfconsistent",
-      "source": "wide-rung GoldenFloat oracle (single decode law, dyadic-exact, no independent second witness)",
-      "sha256": "5b2ddc76f1c7a8c0ce50b1e4a8bf8bfcc7d3419916fa3b36780fdd5da02eb0bf"
+      "kind": "bitexact",
+      "source": "wide-rung GoldenFloat exact-dyadic pack promoted to strict bitexact by an analytic zero-rounding separation-bound + two structurally independent exact decoders (dyadic gf_wide_independent_witness.py + Fraction oracle gf96_decode_ref.py), 15/15 abs_error=0, 201512-code cross-check",
+      "sha256": "43127e758d653d26640d38801d42d4daf36fdc70df66a63aadac6a8ce06159fa"
     },
     {
       "id": "gf128",

@@ -160,5 +160,31 @@
       "value_encoding": "dyadic"
     }
   ],
-  "structural_reason": "Bit-precise round-trip defined; vectors emitted by encoder and confirmed by an INDEPENDENT second decoder (gf_wide_independent_witness.py, dyadic A*2^B exact comparison, abs_error=0) -> strict bitexact, not selfconsistent."
+  "structural_reason": "Bit-precise round-trip defined; every finite value is an EXACT dyadic rational odd*2^k (M=59 > 52 -> no FP lowering, no rounding; see SEPARATION_BOUND.md). Confirmed by TWO structurally independent exact decoders (gf_wide_independent_witness.py dyadic + gf96_decode_ref.py Fraction oracle), both 15/15 abs_error=0, cross-checked over 201512 representative codes. Strict bitexact, not selfconsistent. See the witnesses array.",
+  "witnesses": [
+    {
+      "kind": "sw_independent_dyadic",
+      "decoder": "gf_wide_independent_witness.py (from-scratch dyadic normalizer, integer (2^M+mant) -> odd*2^shift; does NOT reuse the encoder)",
+      "scope": "all 15 pack vectors (dyadic A*2^B exact comparison)",
+      "result": "15/15 bit-exact vs pack, abs_error=0 [e=36 m=59 bias=34359738367]",
+      "note": "Independent second decoder distinct from the software encoder that produced these vectors. In-repo witness. SW-only; not an on-silicon HW-conformance (Tier-E) claim.",
+      "source": "gHashTag/t27 conformance/gf_wide_independent_witness.py"
+    },
+    {
+      "kind": "sw_golden_fraction_oracle",
+      "decoder": "gf96_decode_ref.py (fractions.Fraction significand + symbolic integer shift; exact-dyadic target, no FP lowering)",
+      "scope": "all 15 pack vectors",
+      "result": "15/15 exact vs pack, abs_error=0",
+      "note": "Third-path-style independent decode with a DIFFERENT internal representation from the dyadic witness (Fraction significand vs integer odd*2^shift). Does not materialize 2^BIAS (~2^35 bits). SW-only.",
+      "source": "gHashTag/t27 conformance/witness/gf96/gf96_decode_ref.py"
+    },
+    {
+      "kind": "analytic_separation_bound",
+      "decoder": "SEPARATION_BOUND.md (zero-rounding lemma)",
+      "scope": "entire 2^96 domain (analytic; 2^96 exhaustive infeasible)",
+      "result": "decode has NO rounding: every finite value is an exact dyadic odd*2^k; max rounding error 0 < ULP/2 -> deterministic, abs_error=0 identically",
+      "note": "Because M=59 > 52 the pack target is the exact dyadic value, not a binary64 lowering, so the iverilog-FP64 witness (used for gf48) is NOT applicable and no RTL bit-model is required. Cross-check of the two exact paths over a representative sweep (201512/201512 agree, seed=96) supports the lemma empirically.",
+      "source": "gHashTag/t27 conformance/witness/gf96/SEPARATION_BOUND.md + cross_check_representative.py"
+    }
+  ]
 }
@@ -0,0 +1,80 @@
+# gf96 strict SW-bitexact witness chain (exact-dyadic target)
+
+Promotion of `gf96` (GoldenFloat96: S1 E36 M59, BIAS=34359738367=2^35-1) from
+`bitexact_selfconsistent` to strict SW-`bitexact` in
+`conformance/vectors/INDEX_all_formats.json`.
+
+Status tag: **[verified SW]**. This is a software chain (an analytic
+separation-bound + two structurally independent exact decode paths). It is NOT an
+on-silicon Tier-E claim. HW-decode / HW-compute remain [REQUIRES USER ACTION]
+(a 4/4 Tier-E chain on AX7203, tracked on issue #199 of the trinity-fpga repo).
+
+## Why NO FP-target (contrast with gf48)
+
+Phase-A formats (gf4..gf32) decode into IEEE binary32 (23-bit mantissa). gf48 has
+M=29 and lowers EXACTLY into binary64 (52 bits) with RNE only on the FP64-subnormal
+edge, so its proof used a fixed-width FP64 RTL bit-model + an iverilog witness.
+
+gf96 has **M=59 > 52**, so binary64 CANNOT hold the mantissa exactly and a binary64
+lowering WOULD round. The pack therefore keeps every gf96 value as an EXACT dyadic
+literal `A*2^B` (`value_encoding=dyadic`), and the conformance target is the exact
+rational value itself. Consequently the decode path has NO rounding: every
+representable gf96 code maps to an exact dyadic rational (see `SEPARATION_BOUND.md`,
+Lemma sec. 3). The iverilog-FP64 witness is not applicable, and no RTL bit-model is
+required, because there is no rounding to model.
+
+## Two independent witnesses (both pass in-sandbox)
+
+1. **Dyadic independent decoder** -- `../../gf_wide_independent_witness.py`
+   run with the pack path:
+   ```
+   python3 conformance/gf_wide_independent_witness.py \
+     conformance/vectors/gf96_conformance_v0.json
+   ```
+   Expected: `15/15 bit-exact (abs_error=0)`.
+   Internal representation: integer `(2^M+mant)` normalized to `(odd, shift)`.
+
+2. **Golden Fraction oracle** -- `gf96_decode_ref.py`
+   Exact-rational decode (fractions.Fraction significand + symbolic integer shift),
+   checked against the pack; DIFFERENT internal representation from witness 1:
+   ```
+   python3 conformance/witness/gf96/gf96_decode_ref.py \
+     conformance/vectors/gf96_conformance_v0.json
+   ```
+   Expected: `15/15 exact`.
+
+## Cross-check of the two paths (representative sweep)
+
+`cross_check_representative.py` runs BOTH decode paths over a large representative
+set (5-class + exponent boundaries + full-mantissa edges + deep-underflow/overflow
++ 200k deterministic random, seed=96) and asserts they agree bit-exactly. 2^96
+exhaustive is infeasible; this is a falsifiable representative sweep, and the
+analytic lemma covers the whole domain.
+
+```
+cd conformance/witness/gf96 && python3 cross_check_representative.py
+```
+Expected: `201512/201512 agree` (count is deterministic for seed=96).
+
+## Memory note (why no giant integers)
+
+The gf96 exponent range is +-2^35, so `2^(exp-BIAS)` must NEVER be materialized as
+an integer (2^34e9 ~ 4 GB -> OOM). Both witnesses keep the huge power of two
+symbolic (in `shift`) and only ever build small numerators (<= 2^60). Peak RSS in
+the sandbox is ~14 MB.
+
+## Files
+
+| File | Role |
+|---|---|
+| `gf96_decode_ref.py` | Golden Fraction decode oracle (witness 2). |
+| `cross_check_representative.py` | Cross-check of the two independent paths over the representative sweep. |
+| `SEPARATION_BOUND.md` | Analytic separation-bound (zero-rounding lemma + honesty boundaries). |
+
+## Provenance
+
+- Anchor identity: Vasilev (gHashTag), ORCID 0009-0008-4294-6159, admin@t27.ai.
+- Preprint: arXiv:2606.05017 (GoldenFloat). SSOT:
+  gHashTag/t27 specs/numeric/formats_catalog.t27.
+- gf48 (`conformance/witness/gf48_fp64/`) is the structural model for the pack
+  `witnesses` array used here.
@@ -0,0 +1,139 @@
+# gf96 strict SW-bitexact: analytic separation-bound
+
+Format: **GoldenFloat96** -- S1 E36 M59, BIAS = 34359738367 = 2^35 - 1
+(IEC 60559 interchange bias 2^(E-1)-1). SSOT: `specs/numeric/formats_catalog.t27`.
+
+Status tag: **[verified SW]**. This is a software argument (an analytic lemma plus
+two independent exact decode paths). It is NOT an on-silicon Tier-E claim.
+HW-decode / HW-compute remain [REQUIRES USER ACTION] (a 4/4 Tier-E chain on
+AX7203, tracked on issue #199 of the trinity-fpga repo).
+
+---
+
+## 1. Why a separation-bound (not only an oracle)
+
+gf48 (M=29 <= 52) lowered into IEEE binary64, so its bit-exact proof involved RNE
+rounding on the subnormal edge and was checked by a fixed-width RTL bit-model plus
+an iverilog run (lesson 04.07: Python arbitrary-width does NOT catch fixed-width
+bugs).
+
+gf96 has **M=59 > 52** -- the mantissa does NOT fit in binary64 (52 bits). A
+binary64 lowering WOULD round. Therefore the pack keeps every value as an EXACT
+dyadic literal `A*2^B` (`value_encoding=dyadic`), and the conformance target is the
+exact rational value itself, not an FP lowering. The question the separation-bound
+closes: **is there any place in the gf96 decode path where rounding could be
+non-deterministic or lose precision?** The answer is no, proven below without
+hardware and without an infeasible 2^96 exhaustive sweep.
+
+---
+
+## 2. Decode law (5 classes, parametric in E, M, BIAS)
+
+Bit-layout LSB-aligned: `[sign:1][exp:E][mant:M]`, total 1+E+M = 96 bits.
+EXP_MAX = 2^E - 1.
+
+| Class | Condition | Value |
+|---|---|---|
+| Inf | exp=EXP_MAX, mant=0 | (-1)^s * inf |
+| NaN | exp=EXP_MAX, mant!=0 | quiet NaN (payload irrelevant) |
+| Zero | exp=0, mant=0 | (-1)^s * 0 |
+| Subnormal | exp=0, mant!=0 | (-1)^s * (mant / 2^M) * 2^(1-BIAS) |
+| Normal | otherwise | (-1)^s * (1 + mant / 2^M) * 2^(exp-BIAS) |
+
+---
+
+## 3. Lemma (exact representability -- "zero rounding error")
+
+**Claim.** For any 96-bit code `raw`, the finite decoded gf96 value is an exact
+dyadic rational of the form `odd * 2^k` (odd is odd or 0, k in Z), and this
+representation is unique. Consequently the gf96 decode path contains NO rounding,
+and abs_error = 0 holds identically (not statistically) over the whole domain.
+
+**Proof.** Consider the finite classes.
+
+*Normal.*
+  V = (1 + mant/2^M) * 2^(exp-BIAS)
+    = (2^M + mant) * 2^(exp - BIAS - M).
+The numerator `2^M + mant` is an integer in [2^M, 2^(M+1)-1] (since 0 <= mant <=
+2^M-1). The exponent `exp - BIAS - M` is an integer. So V = integer * 2^integer ->
+dyadic.
+
+*Subnormal.*
+  V = (mant/2^M) * 2^(1-BIAS)
+    = mant * 2^(1 - BIAS - M),
+mant an integer in [1, 2^M-1], integer exponent -> dyadic.
+
+*Zero.* V = 0 = 0*2^0 -- dyadic (degenerate edge).
+
+The canonical form `odd * 2^k` is obtained by factoring all powers of two out of the
+integer numerator into the exponent; it is unique (a nonzero rational has exactly
+one representation odd*2^k with odd numerator). QED.
+
+**Corollary (separation-bound, strong form).** Let Delta be the minimum distance
+between two distinct representable gf96 values (the ULP at a given exponent =
+2^(exp-BIAS-M)). Since each value is represented EXACTLY (sec. 3), the maximum
+decode rounding error is 0 < Delta/2 for every exponent. The condition
+"separation of representable values strictly exceeds the maximum rounding error"
+holds with room to spare (the error is exactly 0). Rounding is therefore
+deterministic and cannot select a neighbouring value: the decode map raw -> value
+is injective up to signed-zero / NaN class and is independent of any rounding mode.
+
+Note: the argument does NOT materialize 2^BIAS (~2^35 bits). It operates on an
+integer numerator (<= 2^60) and a symbolic integer exponent. This is exactly what
+both witness implementations do (sec. 4), so their execution fits in sandbox memory
+(peak ~14 MB).
+
+---
+
+## 4. Two independent exact decode paths (witness set)
+
+The lemma is necessary but not sufficient: the SPECIFIC pack vectors must also match
+an independently computed value. Two structurally DIFFERENT exact decode
+implementations provide this, agreeing with each other and with the pack:
+
+1. **Dyadic independent witness** -- `conformance/gf_wide_independent_witness.py`
+   (already in-repo; parametric in (e,m,bias) from the catalog; written from
+   scratch, does NOT reuse the encoder). Internal representation: an integer
+   `(2^M+mant)` normalized to `(odd, shift)` by factoring out twos.
+   Result: **15/15 pack vectors bit-exact, abs_error=0**.
+
+2. **Golden Fraction oracle** -- `conformance/witness/gf96/gf96_decode_ref.py`
+   (new; independent implementation). DIFFERENT internal representation: the
+   significand is a genuine `fractions.Fraction` (1 + mant/2^M), while the large
+   exponent is carried as a separate symbolic integer `shift`; final
+   canonicalization via `sig.numerator / sig.denominator * 2^shift`.
+   Result: **15/15 pack vectors exact, abs_error=0**.
+
+**Cross-check of the two paths** (`cross_check_representative.py`): on the 15 pack
+vectors plus a representative set (5 classes + exponent boundaries + full-mantissa
+edges + deep-underflow/overflow + 200k deterministic random, seed=96) --
+**201512/201512 agreements**, abs_error=0. 2^96 exhaustive is infeasible; this is a
+falsifiable representative sweep, and lemma sec. 3 covers the whole domain
+analytically.
+
+---
+
+## 5. Why this is strict bitexact, not selfconsistent
+
+`bitexact_selfconsistent` = one decode law, no second independent witness. Here we
+have: (a) an analytic lemma of zero rounding error (decode with no rounding at all),
+and (b) TWO structurally different exact paths agreeing with each other and with the
+pack. This meets the strict SW-`bitexact` definition (independent decoder +
+abs_error=0 + second witness). Promotion: gf96 `bitexact_selfconsistent -> bitexact`.
+
+## 6. Honesty boundaries
+
+- This is an **SW** argument. NOT Tier-E (no CI GREEN + bitstream SHA256 + UART
+  N/N + IDCODE 0x13636093). gf96 decode-HW / compute-HW = [REQUIRES USER ACTION].
+- The iverilog-FP64 witness (as used for gf48) is **not applicable** here: M=59 >
+  52, the target type is not binary64 but the exact dyadic value; no fixed-width FP
+  datapath participates in gf96 SW conformance. An RTL bit-model is not required
+  because there is no rounding.
+- No categorical superiority claims about gf96 over any other format. The
+  GoldenFloat ladder earns its place through breadth and toolchain coherence, not
+  per-rung superiority; takum (Hunhold 2024, arXiv:2412.20273) is the standing
+  counterexample and is not suppressed.
+
+Anchor: Vasilev (gHashTag), ORCID 0009-0008-4294-6159, admin@t27.ai.
+Preprint: arXiv:2606.05017 (GoldenFloat). SSOT: gHashTag/t27
+specs/numeric/formats_catalog.t27.
@@ -0,0 +1,114 @@
+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+"""
+cross_check_representative.py -- cross-verify the TWO independent gf96 decode paths
+(dyadic integer normalizer  vs  Fraction-significand + symbolic shift) over a large
+REPRESENTATIVE code set. 2^96 exhaustive is infeasible; this is a falsifiable
+representative sweep: 5-class + exponent boundaries + full-mantissa edges +
+deep-underflow/overflow edges + deterministic random (seed=96).
+
+Both paths must agree bit-exactly (same canonical dyadic (odd, shift), or same
+special class) on every probed code. Any disagreement -> exit 1 (falsified).
+
+Author: Vasilev (gHashTag), ORCID 0009-0008-4294-6159, admin@t27.ai.
+"""
+import os
+import random
+import sys
+
+# Make both witness modules importable no matter the current working directory:
+# witness 2 (gf96_decode_ref) lives beside this file; witness 1
+# (gf_wide_independent_witness) lives two levels up in conformance/.
+_HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, _HERE)                              # gf96_decode_ref.py
+sys.path.insert(0, os.path.abspath(os.path.join(_HERE, "..", "..")))  # conformance/
+
+import gf96_decode_ref as ORACLE                      # Fraction path (witness 2)
+from gf_wide_independent_witness import make_decoder, normalize_dyadic  # dyadic path (witness 1)
+
+N, E, M, BIAS = 96, 36, 59, 34359738367
+EXP_MAX = (1 << E) - 1
+
+
+def path_dyadic(raw):
+    """Witness-1 decode -> ('SPECIAL',name) | ('ZERO',) | ('NUM',(odd,shift))."""
+    dec, _ = make_decoder(E, M, BIAS)
+    r = dec(raw)
+    if isinstance(r, str):
+        if r.startswith("ZERO"):
+            return ("NUM", (0, 0))
+        return ("SPECIAL", r)
+    return ("NUM", r)  # (odd, shift)
+
+
+def path_fraction(raw):
+    """Witness-2 decode -> ('SPECIAL',name) | ('NUM',(odd,shift))."""
+    d = ORACLE.decode_fraction(raw)
+    if d[0] == "SPECIAL":
+        return ("SPECIAL", d[1])
+    return ("NUM", ORACLE.sigshift_to_dyadic(d[1], d[2]))
+
+
+def make_code(sign, exp, mant):
+    return (sign << (E + M)) | ((exp & EXP_MAX) << M) | (mant & ((1 << M) - 1))
+
+
+def representative_codes():
+    codes = set()
+    MMAX = (1 << M) - 1
+    exps = {0, 1, 2, 3, EXP_MAX, EXP_MAX - 1, EXP_MAX - 2,
+            BIAS & EXP_MAX, (BIAS - 1) & EXP_MAX, (BIAS + 1) & EXP_MAX,
+            1 << (E - 1), (1 << (E - 1)) - 1, (1 << (E - 1)) + 1}
+    # sweep a denser band of exponents too
+    for e in range(0, 40):
+        exps.add(e)
+        exps.add(EXP_MAX - e)
+    mants = {0, 1, 2, 3, MMAX, MMAX - 1, MMAX >> 1, (MMAX >> 1) + 1,
+             1 << (M - 1), (1 << (M - 1)) - 1, 1 << (M // 2)}
+    for s in (0, 1):
+        for e in exps:
+            for m in mants:
+                codes.add(make_code(s, e, m))
+    # deterministic random
+    rng = random.Random(96)
+    for _ in range(200000):
+        codes.add(rng.getrandbits(N))
+    return codes
+
+
+def main():
+    codes = representative_codes()
+    ok = 0
+    fails = []
+    for raw in codes:
+        a = path_dyadic(raw)
+        b = path_fraction(raw)
+        # NaN: both paths must classify as NaN(+/-) with matching sign; payload irrelevant
+        if a[0] == "SPECIAL" and b[0] == "SPECIAL":
+            an, bn = a[1], b[1]
+            if an.startswith("NAN") and bn.startswith("NAN"):
+                match = (an[3:] == bn[3:])  # sign parenthetical
+            else:
+                match = (an == bn)
+        else:
+            match = (a == b)
+        if match:
+            ok += 1
+        else:
+            if len(fails) < 20:
+                fails.append((hex(raw), a, b))
+    tot = len(codes)
+    print(f"gf96 cross-check (dyadic path == Fraction path): {ok}/{tot} agree "
+          f"[e={E} m={M} bias={BIAS}]")
+    if fails:
+        print("FAILS (first 20):")
+        for h, a, b in fails:
+            print(f"  {h}: dyadic={a} fraction={b}")
+        return 1
+    print(f"VERDICT: {tot} representative codes, two independent exact paths agree, "
+          f"abs_error=0 (2^96 exhaustive infeasible; falsifiable representative sweep)")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())