mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
docs(hachimoji): document torsor consequences and update glossary
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)
This commit is contained in:
parent
1a722fac48
commit
e0d7753165
5 changed files with 273 additions and 42 deletions
|
|
@ -356,6 +356,8 @@ Current Research Stack cornfield ref (for cross-repo lookup only):
|
|||
- `python/hachimoji_citation.py` — Equation → Hachimoji state classifier → arXiv
|
||||
citation retriever. Mirrors `formal/CoreFormalism/HachimojiCodec.lean` exactly.
|
||||
Uses hybrid_search SQL function for trigram+pgvector RRF retrieval.
|
||||
Design note on torsor consequences (open sorry closes, token-embed Fourier
|
||||
architecture, chord-distance citation weighting): `docs/hachimoji_torsor_consequences.md`.
|
||||
- Build baselines and session summaries are recorded in
|
||||
`docs/build_logs/YYYY-MM-DD_session_build_baseline.md` (see
|
||||
`docs/build_logs/2026-06-21_session_build_baseline.md`).
|
||||
|
|
|
|||
|
|
@ -143,7 +143,7 @@ name and explains the delta.
|
|||
| **stability point** | A phase θ fixed under conjugation `θ ↦ −θ` on ℤ/360ℤ. Proved: exactly {0°, 180°} = Φ (trivial) and Ω (collision). These are the self-complementary (ambidextrous) bases — the "DNA palindromes" of the encoding. | `formal/CoreFormalism/HachimojiLUT.lean §6` |
|
||||
| **conjugate** | `PhaseCircle → PhaseCircle`; the map `θ ↦ (360 - θ) % 360`. The binding law dual to Watson-Crick complementarity: each base pairs with its conjugate; stability points are self-paired. | `formal/CoreFormalism/HachimojiLUT.lean §6` |
|
||||
| **octagon chord** | Euclidean distance between adjacent canonical bases under `phaseEmbed`; equals `sqrt(2 - 2·cos(π/4)) = 2·sin(π/8) ≈ 0.7654`. Proved formally (not vacuous as in v.01). | `formal/CoreFormalism/HachimojiLUT.lean §2` |
|
||||
| **HachimojiTokenEmbed** | Planned module for fine-grained manifold position using the 15 remaining S¹⁵ dimensions and the 50-token decomposition. Gives sub-vertex precision within each regime basin. | Planned: `formal/CoreFormalism/HachimojiTokenEmbed.lean` |
|
||||
| **HachimojiTokenEmbed** | Planned module for fine-grained manifold position. Uses Fourier harmonics of the phase angle across all 16 S¹⁵ coordinates: coords (0,2) = (cos θ, sin θ), (4,6) = (cos 2θ, sin 2θ), (8,10) = (cos 4θ, sin 4θ), (12,14) = (cos 8θ, sin 8θ). Gauge-equivariant under state relabeling; norm constraint provable via `cos_sq_add_sin_sq`. See `docs/hachimoji_torsor_consequences.md` §2. | Planned: `formal/CoreFormalism/HachimojiTokenEmbed.lean` |
|
||||
|
||||
## Physics / applied math (ported concepts)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,13 +1,13 @@
|
|||
{
|
||||
"schema": "silversight_project_map_v1",
|
||||
"generated_at": "2026-06-21T18:58:40.565557+00:00",
|
||||
"generated_at": "2026-06-22T05:55:06.950321+00:00",
|
||||
"repo": "https://github.com/allaunthefox/SilverSight",
|
||||
"local_path": "/tmp/SilverSight",
|
||||
"local_path": "/home/allaun/SilverSight",
|
||||
"summary": {
|
||||
"total_files": 116,
|
||||
"lean_files": 62,
|
||||
"python_files": 23,
|
||||
"active": 115,
|
||||
"total_files": 124,
|
||||
"lean_files": 63,
|
||||
"python_files": 24,
|
||||
"active": 123,
|
||||
"quarantined": 1,
|
||||
"archived": 0,
|
||||
"receipt_boundary_files": 4
|
||||
|
|
@ -30,10 +30,10 @@
|
|||
"name": "CoreFormalism",
|
||||
"path": "formal/CoreFormalism",
|
||||
"description": "Canonical Q16_16, Sidon, braid, and Hachimoji foundations.",
|
||||
"file_count": 18,
|
||||
"lean_files": 18,
|
||||
"file_count": 19,
|
||||
"lean_files": 19,
|
||||
"python_files": 0,
|
||||
"active": 18,
|
||||
"active": 19,
|
||||
"quarantined": 0,
|
||||
"archived": 0
|
||||
},
|
||||
|
|
@ -78,10 +78,10 @@
|
|||
"name": "PythonShims",
|
||||
"path": "python",
|
||||
"description": "I/O and feature extraction; no admissibility logic.",
|
||||
"file_count": 9,
|
||||
"file_count": 10,
|
||||
"lean_files": 0,
|
||||
"python_files": 9,
|
||||
"active": 9,
|
||||
"python_files": 10,
|
||||
"active": 10,
|
||||
"quarantined": 0,
|
||||
"archived": 0
|
||||
},
|
||||
|
|
@ -126,10 +126,10 @@
|
|||
"name": "Docs",
|
||||
"path": "docs",
|
||||
"description": "Architecture, contracts, and generated maps.",
|
||||
"file_count": 19,
|
||||
"file_count": 25,
|
||||
"lean_files": 0,
|
||||
"python_files": 3,
|
||||
"active": 19,
|
||||
"active": 25,
|
||||
"quarantined": 0,
|
||||
"archived": 0
|
||||
}
|
||||
|
|
@ -239,7 +239,7 @@
|
|||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 366
|
||||
"line_count": 371
|
||||
},
|
||||
{
|
||||
"path": "CITATION.cff",
|
||||
|
|
@ -253,7 +253,7 @@
|
|||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 196
|
||||
"line_count": 216
|
||||
},
|
||||
{
|
||||
"path": "Core/SilverSight/FixedPoint.lean",
|
||||
|
|
@ -432,20 +432,6 @@
|
|||
"receipt_boundary": false,
|
||||
"line_count": 177
|
||||
},
|
||||
{
|
||||
"path": "c/libq16.so",
|
||||
"layer": "other",
|
||||
"language": "other",
|
||||
"kind": "other",
|
||||
"module": null,
|
||||
"build_target": null,
|
||||
"status": "active",
|
||||
"imports": [],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 52
|
||||
},
|
||||
{
|
||||
"path": "c/q16_canonical.c",
|
||||
"layer": "other",
|
||||
|
|
@ -486,7 +472,7 @@
|
|||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 172
|
||||
"line_count": 231
|
||||
},
|
||||
{
|
||||
"path": "docs/GLOSSARY_ALLOWLIST.md",
|
||||
|
|
@ -528,7 +514,7 @@
|
|||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 2376
|
||||
"line_count": 2513
|
||||
},
|
||||
{
|
||||
"path": "docs/PROJECT_MAP.md",
|
||||
|
|
@ -542,7 +528,7 @@
|
|||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 192
|
||||
"line_count": 198
|
||||
},
|
||||
{
|
||||
"path": "docs/RRC_PLACEMENT.md",
|
||||
|
|
@ -600,6 +586,76 @@
|
|||
"receipt_boundary": false,
|
||||
"line_count": 239
|
||||
},
|
||||
{
|
||||
"path": "docs/build_logs/2026-06-22_session_hachimoji_citation.md",
|
||||
"layer": "docs",
|
||||
"language": "markdown",
|
||||
"kind": "doc",
|
||||
"module": null,
|
||||
"build_target": null,
|
||||
"status": "active",
|
||||
"imports": [],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 58
|
||||
},
|
||||
{
|
||||
"path": "docs/build_logs/2026-06-22_session_hachimoji_lut_bridge.md",
|
||||
"layer": "docs",
|
||||
"language": "markdown",
|
||||
"kind": "doc",
|
||||
"module": null,
|
||||
"build_target": null,
|
||||
"status": "active",
|
||||
"imports": [],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 174
|
||||
},
|
||||
{
|
||||
"path": "docs/concept_map/concept_map_receipt.json",
|
||||
"layer": "docs",
|
||||
"language": "config",
|
||||
"kind": "config",
|
||||
"module": null,
|
||||
"build_target": null,
|
||||
"status": "active",
|
||||
"imports": [],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 36
|
||||
},
|
||||
{
|
||||
"path": "docs/concept_map/drive_concept_map.jsonl",
|
||||
"layer": "docs",
|
||||
"language": "other",
|
||||
"kind": "other",
|
||||
"module": null,
|
||||
"build_target": null,
|
||||
"status": "active",
|
||||
"imports": [],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 752
|
||||
},
|
||||
{
|
||||
"path": "docs/concept_map/markdown_concept_map.jsonl",
|
||||
"layer": "docs",
|
||||
"language": "other",
|
||||
"kind": "other",
|
||||
"module": null,
|
||||
"build_target": null,
|
||||
"status": "active",
|
||||
"imports": [],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 992
|
||||
},
|
||||
{
|
||||
"path": "docs/generate_porting_candidates.py",
|
||||
"layer": "docs",
|
||||
|
|
@ -659,6 +715,20 @@
|
|||
"receipt_boundary": false,
|
||||
"line_count": 373
|
||||
},
|
||||
{
|
||||
"path": "docs/hachimoji_torsor_consequences.md",
|
||||
"layer": "docs",
|
||||
"language": "markdown",
|
||||
"kind": "doc",
|
||||
"module": null,
|
||||
"build_target": null,
|
||||
"status": "active",
|
||||
"imports": [],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 88
|
||||
},
|
||||
{
|
||||
"path": "docs/research_stack_porting_candidates.md",
|
||||
"layer": "docs",
|
||||
|
|
@ -775,6 +845,20 @@
|
|||
"receipt_boundary": false,
|
||||
"line_count": 5
|
||||
},
|
||||
{
|
||||
"path": "extraction/cornfield_concepts.json",
|
||||
"layer": "other",
|
||||
"language": "config",
|
||||
"kind": "config",
|
||||
"module": null,
|
||||
"build_target": null,
|
||||
"status": "active",
|
||||
"imports": [],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 2405
|
||||
},
|
||||
{
|
||||
"path": "formal/BindingSite/BindingSiteCodec.lean",
|
||||
"layer": "binding_site",
|
||||
|
|
@ -1053,6 +1137,26 @@
|
|||
"receipt_boundary": false,
|
||||
"line_count": 366
|
||||
},
|
||||
{
|
||||
"path": "formal/CoreFormalism/HachimojiLUT.lean",
|
||||
"layer": "coreformalism",
|
||||
"language": "lean",
|
||||
"kind": "formal",
|
||||
"module": "CoreFormalism.HachimojiLUT",
|
||||
"build_target": "SilverSightFormal",
|
||||
"status": "active",
|
||||
"imports": [
|
||||
"Mathlib.Data.Real.Basic",
|
||||
"Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic",
|
||||
"Mathlib.Data.Fin.Basic",
|
||||
"Mathlib.Tactic",
|
||||
"CoreFormalism.HachimojiCodec"
|
||||
],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 362
|
||||
},
|
||||
{
|
||||
"path": "formal/CoreFormalism/HachimojiManifoldAxiom.lean",
|
||||
"layer": "coreformalism",
|
||||
|
|
@ -1848,6 +1952,30 @@
|
|||
"receipt_boundary": false,
|
||||
"line_count": 305
|
||||
},
|
||||
{
|
||||
"path": "python/hachimoji_citation.py",
|
||||
"layer": "python_shim",
|
||||
"language": "python",
|
||||
"kind": "python_shim",
|
||||
"module": null,
|
||||
"build_target": null,
|
||||
"status": "active",
|
||||
"imports": [
|
||||
"__future__",
|
||||
"json",
|
||||
"re",
|
||||
"subprocess",
|
||||
"dataclasses",
|
||||
"typing",
|
||||
"sentence_transformers",
|
||||
"sentence_transformers",
|
||||
"argparse"
|
||||
],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 410
|
||||
},
|
||||
{
|
||||
"path": "python/pist_matrix_builder.py",
|
||||
"layer": "python_shim",
|
||||
|
|
@ -2339,6 +2467,11 @@
|
|||
"to": "Core/SilverSight/FixedPoint.lean",
|
||||
"relation": "imports"
|
||||
},
|
||||
{
|
||||
"from": "formal/CoreFormalism/HachimojiLUT.lean",
|
||||
"to": "formal/CoreFormalism/HachimojiCodec.lean",
|
||||
"relation": "imports"
|
||||
},
|
||||
{
|
||||
"from": "formal/CoreFormalism/Q16_16Numerics.lean",
|
||||
"to": "formal/CoreFormalism/FixedPoint.lean",
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
# SilverSight Project Map
|
||||
|
||||
**Generated:** 2026-06-21T18:58:40.565557+00:00
|
||||
**Generated:** 2026-06-22T05:55:06.950321+00:00
|
||||
|
||||
**Source repo:** https://github.com/allaunthefox/SilverSight
|
||||
|
||||
|
|
@ -8,10 +8,10 @@
|
|||
|
||||
## 1. Project Overview
|
||||
|
||||
- **Total tracked files:** 116
|
||||
- **Lean files:** 62
|
||||
- **Python files:** 23
|
||||
- **Active:** 115 | **Quarantined:** 1 | **Archived:** 0
|
||||
- **Total tracked files:** 124
|
||||
- **Lean files:** 63
|
||||
- **Python files:** 24
|
||||
- **Active:** 123 | **Quarantined:** 1 | **Archived:** 0
|
||||
- **Receipt-boundary files:** 4
|
||||
|
||||
## 2. Layer Summary
|
||||
|
|
@ -19,15 +19,15 @@
|
|||
| Layer | Path | Files | Lean | Python | Active | Quarantined | Archived | Description |
|
||||
|-------|------|-------|------|--------|--------|-------------|----------|-------------|
|
||||
| Core | `Core` | 8 | 8 | 0 | 8 | 0 | 0 | Invariant core: no imports except Mathlib; defines Receipt and AVM. |
|
||||
| CoreFormalism | `formal/CoreFormalism` | 18 | 18 | 0 | 18 | 0 | 0 | Canonical Q16_16, Sidon, braid, and Hachimoji foundations. |
|
||||
| CoreFormalism | `formal/CoreFormalism` | 19 | 19 | 0 | 19 | 0 | 0 | Canonical Q16_16, Sidon, braid, and Hachimoji foundations. |
|
||||
| PVGS_DQ_Bridge | `formal/PVGS_DQ_Bridge` | 9 | 8 | 1 | 9 | 0 | 0 | Photon-varied Gaussian state dual-quaternion bridge. |
|
||||
| UniversalEncoding | `formal/UniversalEncoding` | 2 | 2 | 0 | 2 | 0 | 0 | Universal math address space and chirality. |
|
||||
| BindingSite | `formal/BindingSite` | 3 | 3 | 0 | 3 | 0 | 0 | Amino-acid / protein binding sketches. |
|
||||
| PythonShims | `python` | 9 | 0 | 9 | 9 | 0 | 0 | I/O and feature extraction; no admissibility logic. |
|
||||
| PythonShims | `python` | 10 | 0 | 10 | 10 | 0 | 0 | I/O and feature extraction; no admissibility logic. |
|
||||
| QUBOShims | `qubo` | 5 | 0 | 5 | 5 | 0 | 0 | QUBO/QAOA/Finsler optimization shims. |
|
||||
| Tests | `tests` | 3 | 0 | 3 | 2 | 1 | 0 | Verification fixtures. |
|
||||
| Infrastructure | `.github` | 6 | 0 | 2 | 6 | 0 | 0 | CI workflows and repo scripts. |
|
||||
| Docs | `docs` | 19 | 0 | 3 | 19 | 0 | 0 | Architecture, contracts, and generated maps. |
|
||||
| Docs | `docs` | 25 | 0 | 3 | 25 | 0 | 0 | Architecture, contracts, and generated maps. |
|
||||
|
||||
## 3. File Inventory
|
||||
|
||||
|
|
@ -60,6 +60,7 @@
|
|||
| `formal/CoreFormalism/FixedPoint.lean` | CoreFormalism.FixedPoint | SilverSightFormal | active | — | `0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean` | Canonical Q16_16 fixed-point type; source of truth for cross-language determinism. |
|
||||
| `formal/CoreFormalism/HachimojiBase.lean` | CoreFormalism.HachimojiBase | SilverSightFormal | active | — | — | Base definitions for the 8-state Hachimoji alphabet. |
|
||||
| `formal/CoreFormalism/HachimojiCodec.lean` | CoreFormalism.HachimojiCodec | SilverSightFormal | active | — | — | Hachimoji encode/decode for UTF-8 strings. |
|
||||
| `formal/CoreFormalism/HachimojiLUT.lean` | CoreFormalism.HachimojiLUT | SilverSightFormal | active | — | — | — |
|
||||
| `formal/CoreFormalism/HachimojiManifoldAxiom.lean` | CoreFormalism.HachimojiManifoldAxiom | SilverSightFormal | active | — | — | Axioms tying Hachimoji states to statistical manifold structure. |
|
||||
| `formal/CoreFormalism/InteractionGraphSidon.lean` | CoreFormalism.InteractionGraphSidon | SilverSightFormal | active | — | `0-Core-Formalism/lean/Semantics/Semantics/InteractionGraphSidon.lean` | Typed interaction graphs, bounded Sidon witness, weak-axis CRT reconstruction. |
|
||||
| `formal/CoreFormalism/Q16_16Numerics.lean` | CoreFormalism.Q16_16Numerics | SilverSightFormal | active | — | `0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean` | Numeric helpers and bounds over canonical Q16_16. |
|
||||
|
|
@ -103,6 +104,7 @@
|
|||
| `python/build_corpus250.py` | — | — | active | — | — | — |
|
||||
| `python/build_pist_matrices_250.py` | — | — | active | — | — | — |
|
||||
| `python/chaos_game.py` | — | — | active | — | `4-Infrastructure/shim/chaos_game_16d.py` | 16D chaos-game basin sampler. |
|
||||
| `python/hachimoji_citation.py` | — | — | active | — | — | — |
|
||||
| `python/pist_matrix_builder.py` | — | — | active | — | — | — |
|
||||
| `python/q16_canonical.py` | — | — | active | — | — | Canonical Q16_16 Python reference implementation. |
|
||||
| `python/sidon_address.py` | — | — | active | — | `4-Infrastructure/shim/sidon_generation_kernel.py` | Sidon label generation for collision-free addressing. |
|
||||
|
|
@ -153,9 +155,15 @@
|
|||
| `docs/RRC_REFACTOR_READINESS.md` | — | — | active | — | — | — |
|
||||
| `docs/TESTING.md` | — | — | active | — | — | — |
|
||||
| `docs/build_logs/2026-06-21_session_build_baseline.md` | — | — | active | — | — | — |
|
||||
| `docs/build_logs/2026-06-22_session_hachimoji_citation.md` | — | — | active | — | — | — |
|
||||
| `docs/build_logs/2026-06-22_session_hachimoji_lut_bridge.md` | — | — | active | — | — | — |
|
||||
| `docs/concept_map/concept_map_receipt.json` | — | — | active | — | — | — |
|
||||
| `docs/concept_map/drive_concept_map.jsonl` | — | — | active | — | — | — |
|
||||
| `docs/concept_map/markdown_concept_map.jsonl` | — | — | active | — | — | — |
|
||||
| `docs/generate_porting_candidates.py` | — | — | active | — | — | — |
|
||||
| `docs/generate_project_map.py` | — | — | active | — | — | — |
|
||||
| `docs/generate_research_stack_usage_map.py` | — | — | active | — | — | — |
|
||||
| `docs/hachimoji_torsor_consequences.md` | — | — | active | — | — | — |
|
||||
| `docs/research_stack_porting_candidates.md` | — | — | active | — | — | — |
|
||||
| `docs/research_stack_usage_graph.dot` | — | — | active | — | — | — |
|
||||
| `docs/research_stack_usage_graph.json` | — | — | active | — | — | — |
|
||||
|
|
|
|||
88
docs/hachimoji_torsor_consequences.md
Normal file
88
docs/hachimoji_torsor_consequences.md
Normal file
|
|
@ -0,0 +1,88 @@
|
|||
# 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`
|
||||
Loading…
Add table
Reference in a new issue