diff --git a/docs/hachimoji_torsor_consequences.md b/docs/hachimoji_torsor_consequences.md
deleted file mode 100644
index 921bd97b..00000000
--- a/docs/hachimoji_torsor_consequences.md
+++ /dev/null
@@ -1,88 +0,0 @@
-# Hachimoji Torsor Consequences
-
-**Date:** 2026-06-22
-**Scope:** `formal/CoreFormalism/HachimojiLUT.lean`, planned `formal/CoreFormalism/HachimojiTokenEmbed.lean`, `python/hachimoji_citation.py`
-**Claim boundary:** design-note; proves are pending implementation
-
-The `PhaseCircle = ℤ/360ℤ` torsor framing of the 8 Hachimoji states (45° steps on the unit circle) has three concrete, actionable consequences for the current codebase. None of them change the classifier, the admission gate, or the pipeline order — those remain gauge-invariant by construction.
-
----
-
-## 1. The two open sorrys have clean closes
-
-### `phaseEmbed_injective_on_canonical`
-
-`formal/CoreFormalism/HachimojiLUT.lean:159`
-
-The theorem asks: are the 8 canonical `phaseEmbed` outputs distinct? Under the corrected embedding `θ ↦ (cos(θ·π/180), sin(θ·π/180))` on S¹ ⊂ S¹⁵, this is just distinctness of the 8th roots of unity on the unit circle. All coordinates are explicit rationals once the trig evaluates, so the 8×8 case is decidable by `native_decide`.
-
-Why it is true structurally: the 8 canonical states are the unique trivialization of the ℤ/360ℤ torsor at 45° steps. A torsor has no preferred origin, but once the octagon is pinned down the 8 vertices cannot collide without collapsing the whole framing.
-
-**Recommended close:** `fin_cases` on `i` and `j`, then `norm_num [Real.cos_pi_div_four, Real.cos_three_pi_div_four]` or `native_decide`.
-
-### `BinaryLUT.h_consistent`
-
-`formal/CoreFormalism/HachimojiLUT.lean:254`
-
-The consistency rule says the virtual LUT lookup on two embedded states must equal the embedding of their composed state. The torsor structure gives the composition table for free: composing two Hachimoji states is addition mod 8 in the induced ℤ/8ℤ (Φ+Λ=Λ, Λ+Λ=Ρ, etc.). Concretely, the 8×8 table is closed under this group operation, which `decide` can verify once the table is written out.
-
-**Recommended close:** define `compose` as phase addition modulo 360°, expand the 64-entry table, and let `decide` check equality of the two `SpherePoint` embeddings.
-
----
-
-## 2. `HachimojiTokenEmbed.lean` has a natural architecture
-
-Planned module: `formal/CoreFormalism/HachimojiTokenEmbed.lean`
-
-The 16 S¹⁵ coordinates should be Fourier harmonics of the phase angle, not arbitrary point coordinates. With the torsor framing, the gauge-equivariant choice is:
-
-| Coordinate pair | Harmonic | Formula |
-|---|---|---|
-| coords 0, 2  | fundamental | `(cos θ, sin θ)` |
-| coords 4, 6  | 2nd harmonic | `(cos 2θ, sin 2θ)` |
-| coords 8, 10 | 3rd harmonic | `(cos 4θ, sin 4θ)` |
-| coords 12, 14| 4th harmonic | `(cos 8θ, sin 8θ)` |
-
-This fills all 16 coordinates gauge-equivariantly: any relabeling of the 8 Hachimoji states rotates the harmonics coherently. It gives sub-vertex precision within each regime basin because the higher harmonics resolve structure inside the octagon sector. And it makes the norm constraint provable by `simp [cos_sq_add_sin_sq]` rather than by `sorry`, because each harmonic contributes `cos²(kθ) + sin²(kθ) = 1` and the sum telescopes to the correct normalization.
-
-The 50-token decomposition from `GenomeLUT` then assigns one phase θ per token, and the token-level embedding is the harmonic vector above.
-
----
-
-## 3. `octagon_chord` is the right distance for `hachimoji_citation.py`
-
-`python/hachimoji_citation.py:37`
-
-The citation query currently builds a flat string from `STATE_QUERIES`, a dictionary of state-meaning keywords. The torsor insight says the invariant when comparing two equations is their chord distance on S¹, not their absolute phase label.
-
-Concretely:
-- An equation at Φ (0°) and one at Ζ (315°) are 45° apart on the circle.
-- Φ (0°) and Κ (135°) are 135° apart.
-- Under the chord metric, Φ–Ζ is closer than Φ–Κ, which the current keyword lookup cannot express.
-
-The chord formula is already proved in `HachimojiLUT.lean` (`octagon_chord`, line 142):
-
-```
-|e^{iπ/4} − 1|² = 2 − 2·cos(π/4)
-```
-
-**Follow-on improvement:** weight the hybrid-search query in `hachimoji_citation.py` by angular proximity to adjacent states. For a target state at phase θ, boost terms for states within ±45° and suppress states near the opposite side of the octagon. The formal chord distance gives the exact weighting function.
-
----
-
-## What does not change
-
-- `classifyEquation` (`formal/CoreFormalism/HachimojiCodec.lean:246`)
-- `admission` gate
-- Pipeline order
-
-ADMIT / QUARANTINE depends on which of the 8 regime basins an equation lands in, not on the absolute phase label assigned to that basin. The torsor is a coordinate convenience; the basin partition is gauge-invariant.
-
----
-
-## Cross-references
-
-- `formal/CoreFormalism/HachimojiLUT.lean` — embedding, chord, and virtual LUT definitions
-- `formal/CoreFormalism/HachimojiCodec.lean` — `classifyEquation` and admission gate
-- `python/hachimoji_citation.py` — citation hybrid matcher
-- `docs/GLOSSARY.md` — `phaseEmbed`, `BinaryLUT`, `octagon chord`, `HachimojiTokenEmbed`