diff --git a/AGENTS.md b/AGENTS.md index ada2f59c..1dd19f0c 100644 --- a/AGENTS.md +++ b/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. diff --git a/docs/PROJECT_MAP.json b/docs/PROJECT_MAP.json index cff3b31a..879a7475 100644 --- a/docs/PROJECT_MAP.json +++ b/docs/PROJECT_MAP.json @@ -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", diff --git a/docs/PROJECT_MAP.md b/docs/PROJECT_MAP.md index b566d916..185a5367 100644 --- a/docs/PROJECT_MAP.md +++ b/docs/PROJECT_MAP.md @@ -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 | — | — | — | diff --git a/formal/CoreFormalism/HachimojiLUT.lean b/formal/CoreFormalism/HachimojiLUT.lean index f4b5bf59..b09053e2 100644 --- a/formal/CoreFormalism/HachimojiLUT.lean +++ b/formal/CoreFormalism/HachimojiLUT.lean @@ -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