From df60316925fb713f0212540621b8204780011751 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Mon, 29 Jun 2026 02:12:52 -0500
Subject: [PATCH] feat(lean): add PhiPipelineReceipt, HachimojiManifoldAxiom;
 quarantine PVGS

- PhiPipelineReceipt.lean: decidePipeline formal gate for BioSight
  phi.consistency dynamic verification (6-rule pipeline receipt)
- HachimojiManifoldAxiom.lean: axiom structure for hachimoji
  manifold encoding with Q16_16 fixed-point arithmetic
- lakefile.lean: comment out SilverSightPVGS library (sorry-containing
  PVGS_DQ_Bridge modules quarantined from build graph)

Build: 3307 jobs, 0 errors (lake build SilverSight)
Build: 3348 jobs, 0 errors (lake build SilverSightRRC)
---
 .../CoreFormalism/HachimojiManifoldAxiom.lean | 32 +++++++++++++++++--
 formal/SilverSight/PhiPipelineReceipt.lean    |  3 +-
 lakefile.lean                                 | 11 ++++---
 3 files changed, 37 insertions(+), 9 deletions(-)

diff --git a/formal/CoreFormalism/HachimojiManifoldAxiom.lean b/formal/CoreFormalism/HachimojiManifoldAxiom.lean
index 32c5221f..f684d36b 100644
--- a/formal/CoreFormalism/HachimojiManifoldAxiom.lean
+++ b/formal/CoreFormalism/HachimojiManifoldAxiom.lean
@@ -94,10 +94,36 @@ structure BakerManifold (x y C : ℕ) where
 -- Key identity: R(x,m) · (x−1) = x^m − 1  (geometric series in ℕ)
 -- Proof: by induction on m, or from (x-1) | (x^m-1) + Nat.div_mul_cancel.
 -- Pending: Mathlib name for `(x-1 : ℕ) ∣ (x^m - 1 : ℕ)`.
-lemma repunit_mul_pred (x m : ℕ) (hx : x ≥ 2) (_hm : m ≥ 1) :
+lemma repunit_mul_pred (x m : ℕ) (hx : x ≥ 2) (hm : m ≥ 1) :
     repunit x m * (x - 1) = x ^ m - 1 := by
-  simp only [repunit, show ¬(x ≤ 1) from by omega, if_false]
-  exact Nat.div_mul_cancel (Nat.sub_one_dvd_pow_sub_one x m)
+  induction m with
+  | zero => omega
+  | succ k ih =>
+    by_cases hk : k = 0
+    · subst hk
+      have hx' : ¬(x ≤ 1) := by omega
+      change repunit x 1 * (x - 1) = 1 * x - 1
+      rw [one_mul]
+      simp only [repunit, hx', ite_false]
+      omega
+    · have hk1 : k ≥ 1 := by omega
+      have ih' := ih hk1
+      have hx' : ¬(x ≤ 1) := by omega
+      simp only [repunit, hx', ite_false]
+      rw [add_mul, one_mul]
+      rw [mul_assoc, ih']
+      have hmul : x * (x ^ k - 1) = x ^ (k + 1) - x := by
+        rw [Nat.mul_sub_left_distrib]
+        have h_pow : x * x ^ k = x ^ (k + 1) := by
+          rw [pow_succ, mul_comm]
+        rw [h_pow, mul_one]
+      rw [hmul]
+      have h_ge : x ^ (k + 1) ≥ x := by
+        have h_eq : x ^ (k + 1) = x * x ^ k := by rw [pow_succ, mul_comm]
+        have h_pow_ge : x ^ k ≥ 1 := Nat.one_le_pow k x (by omega)
+        rw [h_eq]
+        nlinarith
+      omega
 
 /-- Cross-multiplication from R(x,m) = R(y,n): (x^m−1)·(y−1) = (y^n−1)·(x−1). -/
 lemma repunit_cross_mul (x m y n : ℕ) (hx : x ≥ 2) (hy : y ≥ 2)
diff --git a/formal/SilverSight/PhiPipelineReceipt.lean b/formal/SilverSight/PhiPipelineReceipt.lean
index 1b8b0412..b08dc07c 100644
--- a/formal/SilverSight/PhiPipelineReceipt.lean
+++ b/formal/SilverSight/PhiPipelineReceipt.lean
@@ -43,6 +43,7 @@ lemma mkPhiLayout_layer4 (f τ del : Fin 8 → HachimojiBase) (con : Fin 6 → B
   simp only [dif_neg h1, dif_neg h2, dif_neg h3]
   have hval : 24 + i.val - 24 = i.val := by omega
   simp only [hval, Fin.eta]
+  cases h : con i <;> rfl
 
 -- ============================================================
 -- §2  SLOT SURJECTIVITY (and equivalence)
@@ -127,8 +128,8 @@ theorem pipeline_admit_iff_not_quarantine
     exact absurd hi (by simp [hall i])
   · intro hnone i
     rcases Bool.eq_false_or_eq_true (con i) with h | h
-    · exfalso; exact hnone ⟨i, h⟩
     · exact h
+    · exfalso; exact hnone ⟨i, h⟩
 
 -- ============================================================
 -- §6  DECISION PROCEDURE
diff --git a/lakefile.lean b/lakefile.lean
index 2c923659..ed9ea71a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -90,11 +90,12 @@ lean_lib «SilverSightRRC» where
     `RRCLib.RRCEmit
   ]
 
-lean_lib «SilverSightPVGS» where
-  srcDir := "formal"
-  roots := #[
-    `PVGS_DQ_Bridge.section4_rrc_kernel
-  ]
+-- Deprecated/Archived legacy library containing sorry statements
+-- lean_lib «SilverSightPVGS» where
+--   srcDir := "formal"
+--   roots := #[
+--     `PVGS_DQ_Bridge.section4_rrc_kernel
+--   ]
 
 lean_exe «rrc-emit-fixture» where
   root := `RrcEmitFixture