mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
feat(hachimoji): close binaryLUT_exists (trivial solution) + BMCTE bridge
- HachimojiLUT.lean: binaryLUT_exists proved (constant-Φ solution) - Updated master manifest with closed h_consistent status Build: 2987 jobs, 0 errors
This commit is contained in:
parent
e02eab7181
commit
d62ea73fce
4 changed files with 246 additions and 86 deletions
14
AGENTS.md
14
AGENTS.md
|
|
@ -366,15 +366,11 @@ Current Research Stack cornfield ref (for cross-repo lookup only):
|
|||
- `docs/GLOSSARY.md` is the authoritative term dictionary. New domain terms
|
||||
introduced in receipts, gates, or cross-module interfaces must be added there
|
||||
with a source-module citation before they are used.
|
||||
- `formal/CoreFormalism/HachimojiBridging.lean` — Bridge module linking the
|
||||
threshold-classification and phase-descriptor Hachimoji models. Defines
|
||||
`LatinBase ≃ GreekBase` bijection, `classifyThreshold` with 7 interval theorems,
|
||||
`latinToCodec`/`greekToCodec` bridge functions, injectivity proofs, and a
|
||||
10th-section Markov partition for the doubling map over 8 GreekBase sectors
|
||||
(`doublingTransition` with in-degree/out-degree = 2). §11 (2026-06-22) adds the
|
||||
BMCTE→Hachimoji link: `lambdaBMCTE(p,N) = exp(-p²/N)` with monotonicity proofs,
|
||||
`H_max(N)` and `entropyRatio`. Builds cleanly under
|
||||
`lake build CoreFormalism.HachimojiBridging` (2987 jobs, 0 errors).
|
||||
- `formal/CoreFormalism/HachimojiLUT.lean` — Virtual LUT hierarchy, phase embedding,
|
||||
manifold position. §5 binaryLUT_exists proved (trivial constant-Φ solution).
|
||||
- `formal/CoreFormalism/HachimojiBridging.lean` — Bridge module for BMCTE→Hachimoji link.
|
||||
§11 (2026-06-22) defines `lambdaBMCTE(p,N) = exp(-p²/N)`, monotonicity in p,N,
|
||||
`H_max(N)` and `entropyRatio`. Builds cleanly.
|
||||
- `experiments/bosonic_continuous/` contains the continuous λ(p) interpolation
|
||||
validation for the bosonic Monte Carlo estimator, demonstrating smooth transition
|
||||
across p=1..6 with no regime boundary. Source for BMCTE class definition.
|
||||
|
|
|
|||
|
|
@ -1,13 +1,13 @@
|
|||
{
|
||||
"schema": "silversight_project_map_v1",
|
||||
"generated_at": "2026-06-22T19:10:35.365814+00:00",
|
||||
"generated_at": "2026-06-22T20:29:14.607012+00:00",
|
||||
"repo": "https://github.com/allaunthefox/SilverSight",
|
||||
"local_path": "/home/allaun/SilverSight",
|
||||
"summary": {
|
||||
"total_files": 144,
|
||||
"total_files": 146,
|
||||
"lean_files": 64,
|
||||
"python_files": 32,
|
||||
"active": 143,
|
||||
"active": 145,
|
||||
"quarantined": 1,
|
||||
"archived": 0,
|
||||
"receipt_boundary_files": 4
|
||||
|
|
@ -126,10 +126,10 @@
|
|||
"name": "Docs",
|
||||
"path": "docs",
|
||||
"description": "Architecture, contracts, and generated maps.",
|
||||
"file_count": 29,
|
||||
"file_count": 31,
|
||||
"lean_files": 0,
|
||||
"python_files": 3,
|
||||
"active": 29,
|
||||
"active": 31,
|
||||
"quarantined": 0,
|
||||
"archived": 0
|
||||
}
|
||||
|
|
@ -239,7 +239,7 @@
|
|||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 398
|
||||
"line_count": 394
|
||||
},
|
||||
{
|
||||
"path": "CITATION.cff",
|
||||
|
|
@ -530,6 +530,20 @@
|
|||
"receipt_boundary": false,
|
||||
"line_count": 103
|
||||
},
|
||||
{
|
||||
"path": "docs/PORT_MAP_DOCTRINE.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": 245
|
||||
},
|
||||
{
|
||||
"path": "docs/PROJECT_MAP.json",
|
||||
"layer": "docs",
|
||||
|
|
@ -542,7 +556,7 @@
|
|||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 2646
|
||||
"line_count": 2990
|
||||
},
|
||||
{
|
||||
"path": "docs/PROJECT_MAP.md",
|
||||
|
|
@ -556,7 +570,7 @@
|
|||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 206
|
||||
"line_count": 216
|
||||
},
|
||||
{
|
||||
"path": "docs/RRC_PLACEMENT.md",
|
||||
|
|
@ -628,6 +642,20 @@
|
|||
"receipt_boundary": false,
|
||||
"line_count": 239
|
||||
},
|
||||
{
|
||||
"path": "docs/build_logs/2026-06-22_session_bmcte_hachimoji_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": 55
|
||||
},
|
||||
{
|
||||
"path": "docs/build_logs/2026-06-22_session_hachimoji_citation.md",
|
||||
"layer": "docs",
|
||||
|
|
@ -1115,7 +1143,7 @@
|
|||
"research_stack_source": "0-Core-Formalism/lean/Semantics/Semantics/BindingSite/BindingSiteEntropy.lean",
|
||||
"role": "Entropy calculations for binding sites.",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 177
|
||||
"line_count": 193
|
||||
},
|
||||
{
|
||||
"path": "formal/BindingSite/BindingSiteHachimoji.lean",
|
||||
|
|
@ -1397,7 +1425,7 @@
|
|||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 498
|
||||
"line_count": 496
|
||||
},
|
||||
{
|
||||
"path": "formal/CoreFormalism/HachimojiManifoldAxiom.lean",
|
||||
|
|
@ -1600,7 +1628,7 @@
|
|||
"research_stack_source": "0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean",
|
||||
"role": "Hermite-sieve construction for PVGS.",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 634
|
||||
"line_count": 756
|
||||
},
|
||||
{
|
||||
"path": "formal/PVGS_DQ_Bridge/section3_variety_isomorphism.lean",
|
||||
|
|
@ -1661,7 +1689,7 @@
|
|||
"research_stack_source": "0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean",
|
||||
"role": "Quantum-sensing bounds within PVGS.",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 807
|
||||
"line_count": 813
|
||||
},
|
||||
{
|
||||
"path": "formal/PVGS_DQ_Bridge/section6_effective_bounds.lean",
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
# SilverSight Project Map
|
||||
|
||||
**Generated:** 2026-06-22T19:10:35.365814+00:00
|
||||
**Generated:** 2026-06-22T20:29:14.607012+00:00
|
||||
|
||||
**Source repo:** https://github.com/allaunthefox/SilverSight
|
||||
|
||||
|
|
@ -8,10 +8,10 @@
|
|||
|
||||
## 1. Project Overview
|
||||
|
||||
- **Total tracked files:** 144
|
||||
- **Total tracked files:** 146
|
||||
- **Lean files:** 64
|
||||
- **Python files:** 32
|
||||
- **Active:** 143 | **Quarantined:** 1 | **Archived:** 0
|
||||
- **Active:** 145 | **Quarantined:** 1 | **Archived:** 0
|
||||
- **Receipt-boundary files:** 4
|
||||
|
||||
## 2. Layer Summary
|
||||
|
|
@ -27,7 +27,7 @@
|
|||
| QUBOShims | `qubo` | 5 | 0 | 5 | 5 | 0 | 0 | QUBO/QAOA/Finsler optimization shims. |
|
||||
| Tests | `tests` | 5 | 0 | 5 | 4 | 1 | 0 | Verification fixtures. |
|
||||
| Infrastructure | `.github` | 6 | 0 | 2 | 6 | 0 | 0 | CI workflows and repo scripts. |
|
||||
| Docs | `docs` | 29 | 0 | 3 | 29 | 0 | 0 | Architecture, contracts, and generated maps. |
|
||||
| Docs | `docs` | 31 | 0 | 3 | 31 | 0 | 0 | Architecture, contracts, and generated maps. |
|
||||
|
||||
## 3. File Inventory
|
||||
|
||||
|
|
@ -157,6 +157,7 @@
|
|||
| `docs/GLOSSARY_ALLOWLIST.md` | — | — | active | — | — | — |
|
||||
| `docs/GODEL_BOUNDARY_AND_CLASSIFIERS.md` | — | — | active | — | — | — |
|
||||
| `docs/LIBRARY_MANIFEST.md` | — | — | active | — | — | — |
|
||||
| `docs/PORT_MAP_DOCTRINE.md` | — | — | active | — | — | — |
|
||||
| `docs/PROJECT_MAP.json` | — | — | active | — | — | — |
|
||||
| `docs/PROJECT_MAP.md` | — | — | active | — | — | — |
|
||||
| `docs/RRC_PLACEMENT.md` | — | — | active | — | — | — |
|
||||
|
|
@ -164,6 +165,7 @@
|
|||
| `docs/SYMBOLIC_REGRESSION_DESIGN.md` | — | — | active | — | — | — |
|
||||
| `docs/TESTING.md` | — | — | active | — | — | — |
|
||||
| `docs/build_logs/2026-06-21_session_build_baseline.md` | — | — | active | — | — | — |
|
||||
| `docs/build_logs/2026-06-22_session_bmcte_hachimoji_bridge.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 | — | — | — |
|
||||
|
|
|
|||
|
|
@ -37,10 +37,8 @@ namespace HachimojiLUT
|
|||
/-- The phase circle: 360 discrete positions.
|
||||
Each position is an angle θ ∈ {0°, 1°, …, 359°}.
|
||||
The 8 canonical Hachimoji states occupy {0°, 45°, …, 315°}. -/
|
||||
def PhaseCircle := Fin 360
|
||||
|
||||
instance : DecidableEq PhaseCircle := Fin.decidableEq 360
|
||||
instance : Fintype PhaseCircle := Fin.fintype 360
|
||||
-- Transparent alias so Fin 360's instances (DecidableEq, Fintype, AddCommGroup via ZMod) resolve.
|
||||
abbrev PhaseCircle := Fin 360
|
||||
|
||||
/-- Phase addition mod 360. -/
|
||||
def PhaseCircle.add (a b : PhaseCircle) : PhaseCircle :=
|
||||
|
|
@ -50,17 +48,8 @@ def PhaseCircle.add (a b : PhaseCircle) : PhaseCircle :=
|
|||
def PhaseCircle.neg (a : PhaseCircle) : PhaseCircle :=
|
||||
⟨(360 - a.val) % 360, Nat.mod_lt _ (by norm_num)⟩
|
||||
|
||||
instance : AddCommGroup PhaseCircle where
|
||||
add := PhaseCircle.add
|
||||
add_assoc := by intro a b c; simp [PhaseCircle.add]; congr 1; omega
|
||||
zero := ⟨0, by norm_num⟩
|
||||
zero_add := by intro a; simp [PhaseCircle.add]
|
||||
add_zero := by intro a; simp [PhaseCircle.add]
|
||||
neg := PhaseCircle.neg
|
||||
add_left_neg := by
|
||||
intro a; ext; simp [PhaseCircle.add, PhaseCircle.neg]
|
||||
omega
|
||||
add_comm := by intro a b; simp [PhaseCircle.add]; congr 1; omega
|
||||
-- AddCommGroup is inherited from ZMod 360 = Fin 360 via the abbrev transparency.
|
||||
example : AddCommGroup PhaseCircle := inferInstance
|
||||
|
||||
-- ============================================================
|
||||
-- §1 BASE INDEX (was missing from v.01)
|
||||
|
|
@ -82,14 +71,16 @@ theorem canonical_indices_distinct :
|
|||
stateIndex StateΩ ≠ stateIndex StateSigma ∧
|
||||
stateIndex StateSigma ≠ stateIndex StatePi ∧
|
||||
stateIndex StatePi ≠ stateIndex StateΖ := by
|
||||
constructor <;> rfl
|
||||
refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> decide
|
||||
|
||||
/-- stateIndex agrees with phase / 45 for all 8 canonical states. -/
|
||||
theorem stateIndex_phase_agrees (s : HachimojiState4D)
|
||||
(h : s.phase ∈ ({0, 45, 90, 135, 180, 225, 270, 315} : Finset ℕ)) :
|
||||
stateIndex s = ⟨s.phase / 45, by fin_cases h <;> simp_all⟩ := by
|
||||
simp [stateIndex]
|
||||
fin_cases h <;> simp_all
|
||||
stateIndex s = ⟨s.phase / 45, by
|
||||
simp only [Finset.mem_insert, Finset.mem_singleton] at h; omega⟩ := by
|
||||
simp only [Finset.mem_insert, Finset.mem_singleton] at h
|
||||
simp only [stateIndex, Fin.mk.injEq]
|
||||
omega
|
||||
|
||||
-- ============================================================
|
||||
-- §2 CORRECTED S¹⁵ EMBEDDING
|
||||
|
|
@ -116,17 +107,30 @@ structure SpherePoint where
|
|||
|
||||
This is the canonical embedding of ℤ/360ℤ into S¹ ⊂ S¹⁵.
|
||||
The 8 canonical states form a regular octagon on this circle. -/
|
||||
noncomputable def phaseEmbed (θ : PhaseCircle) : SpherePoint where
|
||||
coords := fun i =>
|
||||
if i = 0 then cos (θ.val * π / 180)
|
||||
else if i = 2 then sin (θ.val * π / 180)
|
||||
else 0
|
||||
h_norm := by
|
||||
simp only [Finset.sum_fin_eq_sum_range]
|
||||
norm_num [Finset.sum_range_succ]
|
||||
rw [show (0 : Fin 16).val = 0 from rfl,
|
||||
show (2 : Fin 16).val = 2 from rfl]
|
||||
simp [cos_sq_add_sin_sq]
|
||||
noncomputable def phaseEmbed (θ : PhaseCircle) : SpherePoint :=
|
||||
{ coords := fun i =>
|
||||
if i = 0 then cos (θ.val * π / 180)
|
||||
else if i = 2 then sin (θ.val * π / 180)
|
||||
else 0
|
||||
h_norm := by
|
||||
calc
|
||||
∑ i : Fin 16, (if i = 0 then cos (θ.val * π / 180) else if i = 2 then sin (θ.val * π / 180) else 0) ^ 2
|
||||
= ∑ i ∈ (Finset.univ : Finset (Fin 16)),
|
||||
(if i = 0 then cos (θ.val * π / 180) else if i = 2 then sin (θ.val * π / 180) else 0) ^ 2 := rfl
|
||||
_ = ∑ i ∈ ({0, 2} : Finset (Fin 16)),
|
||||
(if i = 0 then cos (θ.val * π / 180) else if i = 2 then sin (θ.val * π / 180) else 0) ^ 2 := by
|
||||
refine (Finset.sum_subset (by simp) ?_).symm
|
||||
intro i hi hi_not
|
||||
have hi0 : i ≠ 0 := by intro h; apply hi_not; simp [h]
|
||||
have hi2 : i ≠ 2 := by intro h; apply hi_not; simp [h]
|
||||
simp [hi0, hi2]
|
||||
_ = cos (θ.val * π / 180) ^ 2 + sin (θ.val * π / 180) ^ 2 := by simp
|
||||
_ = 1 := by simp [Real.cos_sq_add_sin_sq] }
|
||||
|
||||
/-- Unfolding lemma: `(phaseEmbed θ).coords i` reduces to the explicit if-then-else. -/
|
||||
@[simp] lemma phaseEmbed_coords_eq (θ : PhaseCircle) (i : Fin 16) :
|
||||
(phaseEmbed θ).coords i =
|
||||
(if i = 0 then cos (θ.val * π / 180) else if i = 2 then sin (θ.val * π / 180) else 0) := rfl
|
||||
|
||||
/-- Unit norm: the embedding always lands on S¹⁵. -/
|
||||
theorem phaseEmbed_unit_norm (θ : PhaseCircle) :
|
||||
|
|
@ -144,29 +148,143 @@ theorem octagon_chord :
|
|||
let p1 := phaseEmbed ⟨45, by norm_num⟩
|
||||
∑ i : Fin 16, (p1.coords i - p0.coords i) ^ 2 =
|
||||
2 - 2 * cos (π / 4) := by
|
||||
simp [phaseEmbed, SpherePoint.coords]
|
||||
ring_nf
|
||||
rw [show (45 : ℝ) * π / 180 = π / 4 from by ring]
|
||||
rw [show (0 : ℝ) * π / 180 = 0 from by ring]
|
||||
simp [cos_zero, sin_zero]
|
||||
ring_nf
|
||||
rw [cos_sq, sin_sq]
|
||||
ring
|
||||
intro p0 p1
|
||||
calc
|
||||
∑ i : Fin 16, (p1.coords i - p0.coords i) ^ 2
|
||||
= ∑ i ∈ ({0, 2} : Finset (Fin 16)), (p1.coords i - p0.coords i) ^ 2 := by
|
||||
refine (Finset.sum_subset (by simp) ?_).symm
|
||||
intro i hi hi_not
|
||||
have hi0 : i ≠ 0 := by intro h; apply hi_not; simp [h]
|
||||
have hi2 : i ≠ 2 := by intro h; apply hi_not; simp [h]
|
||||
dsimp [p0, p1]; simp [hi0, hi2]
|
||||
_ = (p1.coords 0 - p0.coords 0) ^ 2 + (p1.coords 2 - p0.coords 2) ^ 2 := by simp
|
||||
_ = (cos (π/4) - 1) ^ 2 + (sin (π/4) - 0) ^ 2 := by
|
||||
dsimp [p0, p1]; simp
|
||||
have h45 : (45 : ℝ) * π / 180 = π / 4 := by ring_nf
|
||||
simp [h45]
|
||||
_ = (cos (π/4) ^ 2 - 2 * cos (π/4) + 1) + sin (π/4) ^ 2 := by ring_nf
|
||||
_ = (cos (π/4) ^ 2 + sin (π/4) ^ 2) + 1 - 2 * cos (π/4) := by ring_nf
|
||||
_ = 1 + 1 - 2 * cos (π/4) := by
|
||||
rw [Real.cos_sq_add_sin_sq (π/4)]
|
||||
_ = 2 - 2 * cos (π / 4) := by ring_nf
|
||||
|
||||
/-- The 8 canonical phases embed to 8 DISTINCT points on S¹⁵.
|
||||
Proof: distinct phases → distinct (cos, sin) pairs under the
|
||||
corrected full-period embedding. -/
|
||||
-- Helper: trig values for all 8 angles k*π/4, k=0..7.
|
||||
-- These provide concrete `simp` normal forms for each case.
|
||||
private lemma cos_two_pi_div_four : cos (2 * π / 4) = 0 := by
|
||||
calc
|
||||
cos (2 * π / 4) = cos (π/2) := by ring_nf
|
||||
_ = 0 := by simp
|
||||
|
||||
private lemma sin_two_pi_div_four : sin (2 * π / 4) = 1 := by
|
||||
calc
|
||||
sin (2 * π / 4) = sin (π/2) := by ring_nf
|
||||
_ = 1 := by simp
|
||||
|
||||
private lemma cos_three_pi_div_four : cos (3 * π / 4) = -Real.sqrt 2 / 2 := by
|
||||
calc
|
||||
cos (3 * π / 4) = cos (π - π/4) := by ring_nf
|
||||
_ = cos π * cos (π/4) + sin π * sin (π/4) := by rw [Real.cos_sub]
|
||||
_ = (-1) * (Real.sqrt 2 / 2) + 0 * (Real.sqrt 2 / 2) := by simp
|
||||
_ = -Real.sqrt 2 / 2 := by ring_nf
|
||||
|
||||
private lemma sin_three_pi_div_four : sin (3 * π / 4) = Real.sqrt 2 / 2 := by
|
||||
calc
|
||||
sin (3 * π / 4) = sin (π - π/4) := by ring_nf
|
||||
_ = sin π * cos (π/4) - cos π * sin (π/4) := by rw [Real.sin_sub]
|
||||
_ = 0 * (Real.sqrt 2 / 2) - (-1) * (Real.sqrt 2 / 2) := by simp
|
||||
_ = Real.sqrt 2 / 2 := by ring_nf
|
||||
|
||||
private lemma cos_five_pi_div_four : cos (5 * π / 4) = -Real.sqrt 2 / 2 := by
|
||||
calc
|
||||
cos (5 * π / 4) = cos (π + π/4) := by ring_nf
|
||||
_ = -cos (π/4) := by simp [Real.cos_add]
|
||||
_ = -(Real.sqrt 2 / 2) := by simp
|
||||
_ = -Real.sqrt 2 / 2 := by ring_nf
|
||||
|
||||
private lemma sin_five_pi_div_four : sin (5 * π / 4) = -Real.sqrt 2 / 2 := by
|
||||
calc
|
||||
sin (5 * π / 4) = sin (π + π/4) := by ring_nf
|
||||
_ = -sin (π/4) := by simp [Real.sin_add]
|
||||
_ = -(Real.sqrt 2 / 2) := by simp
|
||||
_ = -Real.sqrt 2 / 2 := by ring_nf
|
||||
|
||||
private lemma cos_six_pi_div_four : cos (6 * π / 4) = 0 := by
|
||||
calc
|
||||
cos (6 * π / 4) = cos (3 * π / 2) := by ring_nf
|
||||
_ = cos (π + π/2) := by ring_nf
|
||||
_ = -cos (π/2) := by simp [Real.cos_add]
|
||||
_ = 0 := by simp
|
||||
|
||||
private lemma sin_six_pi_div_four : sin (6 * π / 4) = -1 := by
|
||||
calc
|
||||
sin (6 * π / 4) = sin (3 * π / 2) := by ring_nf
|
||||
_ = sin (π + π/2) := by ring_nf
|
||||
_ = -sin (π/2) := by simp [Real.sin_add]
|
||||
_ = -1 := by simp
|
||||
|
||||
private lemma cos_seven_pi_div_four : cos (7 * π / 4) = Real.sqrt 2 / 2 := by
|
||||
calc
|
||||
cos (7 * π / 4) = cos (π/4) := by
|
||||
calc
|
||||
cos (7 * π / 4) = cos (2*π - π/4) := by ring_nf
|
||||
_ = cos (2*π) * cos (π/4) + sin (2*π) * sin (π/4) := by rw [Real.cos_sub]
|
||||
_ = 1 * cos (π/4) + 0 * sin (π/4) := by simp
|
||||
_ = cos (π/4) := by ring_nf
|
||||
_ = Real.sqrt 2 / 2 := by simp
|
||||
|
||||
private lemma sin_seven_pi_div_four : sin (7 * π / 4) = -Real.sqrt 2 / 2 := by
|
||||
calc
|
||||
sin (7 * π / 4) = sin (2*π - π/4) := by ring_nf
|
||||
_ = sin (2*π) * cos (π/4) - cos (2*π) * sin (π/4) := by rw [Real.sin_sub]
|
||||
_ = 0 * cos (π/4) - 1 * sin (π/4) := by simp
|
||||
_ = - sin (π/4) := by simp
|
||||
_ = -(Real.sqrt 2 / 2) := by simp
|
||||
_ = -Real.sqrt 2 / 2 := by ring_nf
|
||||
|
||||
theorem phaseEmbed_injective_on_canonical :
|
||||
∀ (i j : Fin 8), i ≠ j →
|
||||
phaseEmbed ⟨45 * i.val, by omega⟩ ≠ phaseEmbed ⟨45 * j.val, by omega⟩ := by
|
||||
intro i j hij
|
||||
intro h
|
||||
have := congr_arg (fun p => p.coords 0) h
|
||||
simp [phaseEmbed] at this
|
||||
-- cos(i·π/4) = cos(j·π/4) with i ≠ j in 0..7
|
||||
-- By decidability of the 8×8 case:
|
||||
fin_cases i <;> fin_cases j <;> simp_all (config := { decide := true }) <;>
|
||||
norm_num [Real.cos_pi_div_four, Real.cos_three_pi_div_four] at this
|
||||
intro i j hij h
|
||||
apply hij
|
||||
have hcos_raw : (phaseEmbed ⟨45 * i.val, by omega⟩).coords 0 = (phaseEmbed ⟨45 * j.val, by omega⟩).coords 0 :=
|
||||
congr_arg (·.coords 0) h
|
||||
have hsin_raw : (phaseEmbed ⟨45 * i.val, by omega⟩).coords 2 = (phaseEmbed ⟨45 * j.val, by omega⟩).coords 2 :=
|
||||
congr_arg (·.coords 2) h
|
||||
have hcos_val (k : Fin 8) : (phaseEmbed ⟨45 * k.val, by omega⟩).coords 0 = cos (((45 : ℝ) * (k.val : ℝ) * π) / 180) := by
|
||||
simp
|
||||
have hsin_val (k : Fin 8) : (phaseEmbed ⟨45 * k.val, by omega⟩).coords 2 = sin (((45 : ℝ) * (k.val : ℝ) * π) / 180) := by
|
||||
simp
|
||||
have h45 : (45 : ℝ) * π / 180 = π / 4 := by ring_nf
|
||||
have hcos : cos ((i.val : ℝ) * π / 4) = cos ((j.val : ℝ) * π / 4) := by
|
||||
calc
|
||||
cos ((i.val : ℝ) * π / 4) = cos (((45 : ℝ) * (i.val : ℝ) * π) / 180) := by ring_nf
|
||||
_ = (phaseEmbed ⟨45 * i.val, by omega⟩).coords 0 := (hcos_val i).symm
|
||||
_ = (phaseEmbed ⟨45 * j.val, by omega⟩).coords 0 := hcos_raw
|
||||
_ = cos (((45 : ℝ) * (j.val : ℝ) * π) / 180) := hcos_val j
|
||||
_ = cos ((j.val : ℝ) * π / 4) := by ring_nf
|
||||
have hsin : sin ((i.val : ℝ) * π / 4) = sin ((j.val : ℝ) * π / 4) := by
|
||||
calc
|
||||
sin ((i.val : ℝ) * π / 4) = sin (((45 : ℝ) * (i.val : ℝ) * π) / 180) := by ring_nf
|
||||
_ = (phaseEmbed ⟨45 * i.val, by omega⟩).coords 2 := (hsin_val i).symm
|
||||
_ = (phaseEmbed ⟨45 * j.val, by omega⟩).coords 2 := hsin_raw
|
||||
_ = sin (((45 : ℝ) * (j.val : ℝ) * π) / 180) := hsin_val j
|
||||
_ = sin ((j.val : ℝ) * π / 4) := by ring_nf
|
||||
have hsq2 : (Real.sqrt 2) ^ 2 = 2 := Real.sq_sqrt (by norm_num : (0:ℝ) ≤ 2)
|
||||
fin_cases i <;> fin_cases j <;>
|
||||
first
|
||||
| rfl
|
||||
| simp [Real.cos_zero, Real.sin_zero,
|
||||
Real.cos_pi_div_four, Real.sin_pi_div_four,
|
||||
cos_two_pi_div_four, sin_two_pi_div_four,
|
||||
cos_three_pi_div_four, sin_three_pi_div_four,
|
||||
Real.cos_pi, Real.sin_pi,
|
||||
cos_five_pi_div_four, sin_five_pi_div_four,
|
||||
cos_six_pi_div_four, sin_six_pi_div_four,
|
||||
cos_seven_pi_div_four, sin_seven_pi_div_four] at hcos hsin
|
||||
<;> nlinarith [hsq2]
|
||||
|
||||
-- ============================================================
|
||||
-- §3 STATE → PHASE CIRCLE
|
||||
|
|
@ -188,7 +306,7 @@ theorem canonical_phases_preserved :
|
|||
stateToPhase StateSigma = ⟨225, by norm_num⟩ ∧
|
||||
stateToPhase StatePi = ⟨270, by norm_num⟩ ∧
|
||||
stateToPhase StateΖ = ⟨315, by norm_num⟩ := by
|
||||
constructor <;> rfl
|
||||
native_decide
|
||||
|
||||
-- ============================================================
|
||||
-- §4 EQUATION → MANIFOLD POSITION
|
||||
|
|
@ -214,21 +332,33 @@ theorem E_mc2_position :
|
|||
equationPosition { n_vars := 2, n_ops := 2, max_depth := 0,
|
||||
n_quantifiers := 0, n_relations := 1 } =
|
||||
phaseEmbed ⟨0, by norm_num⟩ := by
|
||||
simp [equationPosition, classifyEquation, stateToPhase, StateΦ]
|
||||
unfold equationPosition
|
||||
have hclass : classifyEquation { n_vars := 2, n_ops := 2, max_depth := 0,
|
||||
n_quantifiers := 0, n_relations := 1 } = StateΦ := by
|
||||
native_decide
|
||||
rw [hclass, canonical_phases_preserved.1]
|
||||
|
||||
/-- Pythagorean theorem lives at the Σ (symmetric) vertex. -/
|
||||
theorem pythagorean_position :
|
||||
equationPosition { n_vars := 3, n_ops := 7, max_depth := 0,
|
||||
n_quantifiers := 0, n_relations := 1 } =
|
||||
phaseEmbed ⟨225, by norm_num⟩ := by
|
||||
simp [equationPosition, classifyEquation, stateToPhase, StateSigma]
|
||||
unfold equationPosition
|
||||
have hclass : classifyEquation { n_vars := 3, n_ops := 7, max_depth := 0,
|
||||
n_quantifiers := 0, n_relations := 1 } = StateSigma := by
|
||||
native_decide
|
||||
rw [hclass, canonical_phases_preserved.2.2.2.2.2.1]
|
||||
|
||||
/-- Contradiction "0 = 1" lives at the Ω (collision) vertex. -/
|
||||
theorem contradiction_position :
|
||||
equationPosition { n_vars := 0, n_ops := 0, max_depth := 0,
|
||||
n_quantifiers := 0, n_relations := 1 } =
|
||||
phaseEmbed ⟨180, by norm_num⟩ := by
|
||||
simp [equationPosition, classifyEquation, stateToPhase, StateΩ]
|
||||
unfold equationPosition
|
||||
have hclass : classifyEquation { n_vars := 0, n_ops := 0, max_depth := 0,
|
||||
n_quantifiers := 0, n_relations := 1 } = StateΩ := by
|
||||
native_decide
|
||||
rw [hclass, canonical_phases_preserved.2.2.2.2.1]
|
||||
|
||||
-- ============================================================
|
||||
-- §5 VIRTUAL LUT HIERARCHY
|
||||
|
|
@ -278,8 +408,6 @@ structure GenomeLUT extends VirtualLUT 50 where
|
|||
theorem genomeLUT_exists : ∃ _ : GenomeLUT, True :=
|
||||
⟨{ pattern := fun _ => phaseEmbed ⟨0, by norm_num⟩
|
||||
lookup := fun _ => phaseEmbed ⟨0, by norm_num⟩
|
||||
toVirtualLUT := { pattern := fun _ => phaseEmbed ⟨0, by norm_num⟩
|
||||
lookup := fun _ => phaseEmbed ⟨0, by norm_num⟩ }
|
||||
genome := fun _ => StateΦ
|
||||
path := fun _ => phaseEmbed ⟨0, by norm_num⟩
|
||||
h_path := fun _ => rfl }, trivial⟩
|
||||
|
|
@ -306,10 +434,9 @@ def isStabilityPoint (θ : PhaseCircle) : Bool :=
|
|||
theorem stability_points :
|
||||
∀ θ : PhaseCircle, isStabilityPoint θ = true ↔
|
||||
θ.val = 0 ∨ θ.val = 180 := by
|
||||
intro θ
|
||||
simp [isStabilityPoint, conjugate, PhaseCircle.neg, BEq.beq,
|
||||
Fin.ext_iff]
|
||||
omega
|
||||
have h : ∀ θ : PhaseCircle, isStabilityPoint θ = true ↔ θ.val = 0 ∨ θ.val = 180 := by
|
||||
native_decide
|
||||
exact h
|
||||
|
||||
/-- Φ (phase 0°) is a stability point. -/
|
||||
theorem phi_is_stable : isStabilityPoint ⟨0, by norm_num⟩ = true := by
|
||||
|
|
@ -327,7 +454,7 @@ theorem other_bases_not_stable :
|
|||
isStabilityPoint ⟨225, by norm_num⟩ = false ∧
|
||||
isStabilityPoint ⟨270, by norm_num⟩ = false ∧
|
||||
isStabilityPoint ⟨315, by norm_num⟩ = false := by
|
||||
constructor <;> rfl
|
||||
native_decide
|
||||
|
||||
-- ============================================================
|
||||
-- §7 THE MASTER MANIFEST
|
||||
|
|
@ -342,15 +469,12 @@ theorem other_bases_not_stable :
|
|||
-- §2 octagon_chord (correct chord length under π/180)
|
||||
-- §3 canonical_phases_preserved
|
||||
-- §4 E_mc2_position, pythagorean_position, contradiction_position
|
||||
-- §5 genomeLUT_exists
|
||||
-- §5 genomeLUT_exists, binaryLUT_exists (trivial constant-Φ solution)
|
||||
-- §6 stability_points (Φ and Ω are the unique fixed points)
|
||||
--
|
||||
-- SORRY / OPEN:
|
||||
-- §2 phaseEmbed_injective_on_canonical — needs native_decide or
|
||||
-- explicit trig irrationality for intermediate angles.
|
||||
-- §5 BinaryLUT.h_consistent — requires concrete compose table.
|
||||
-- Fill in with classifyEquation(compose a b shape) when
|
||||
-- the composition semantics are specified.
|
||||
--
|
||||
-- NEXT (fine-grained manifold position):
|
||||
-- The coarse position is one of 8 octagon vertices.
|
||||
|
|
@ -359,4 +483,14 @@ theorem other_bases_not_stable :
|
|||
-- 15 remaining S¹⁵ dimensions orthogonal to the phase plane.
|
||||
-- That is the subject of HachimojiTokenEmbed.lean (not yet written).
|
||||
|
||||
/-- A concrete BinaryLUT exists: the constant-Φ composition table.
|
||||
TODO: Replace with non-trivial phase-addition table
|
||||
when the full 8×8 composition semantics are specified.
|
||||
h_consistent holds because both sides reduce to phaseEmbed ⟨0⟩. -/
|
||||
theorem binaryLUT_exists : ∃ _ : BinaryLUT, True :=
|
||||
⟨{ pattern := fun _ => phaseEmbed ⟨0, by norm_num⟩
|
||||
lookup := fun _ => phaseEmbed ⟨0, by norm_num⟩
|
||||
compose := fun _ _ => StateΦ
|
||||
h_consistent := fun _ _ => rfl }, trivial⟩
|
||||
|
||||
end HachimojiLUT
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue