allaun
e0d7753165
Add docs/hachimoji_torsor_consequences.md with three concrete consequences of the PhaseCircle = ℤ/360ℤ torsor framing: 1. phaseEmbed_injective_on_canonical and BinaryLUT.h_consistent have clean closes via native_decide / decide over the 8 canonical phases. 2. HachimojiTokenEmbed.lean should use Fourier harmonics of the phase angle across all 16 S¹⁵ coordinates, making the norm constraint provable by cos_sq_add_sin_sq. 3. octagon_chord is the correct citation-query distance for python/hachimoji_citation.py; follow-on work should weight hybrid search by angular proximity on S¹. Also updates docs/GLOSSARY.md HachimojiTokenEmbed entry with the Fourier harmonics architecture and AGENTS.md with a cross-reference. Regenerate docs/PROJECT_MAP.* to track the new file. Build: N/A (documentation only)
4.9 KiB
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)admissiongate- 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 definitionsformal/CoreFormalism/HachimojiCodec.lean—classifyEquationand admission gatepython/hachimoji_citation.py— citation hybrid matcherdocs/GLOSSARY.md—phaseEmbed,BinaryLUT,octagon chord,HachimojiTokenEmbed