sync(hf): mirror GitHub-canonical lean_commit_sha pins to live Space (additive)

HF Space module-drift guard flagged 5 COPY'd modules whose lean_commit_sha pin diverged: the Space still carried the old 1dca0003 pin while the GitHub source-of-truth was bumped to b675cd84 (the lutar-lean commit pinned by the new theorem-runtime-manifest). GitHub is the source-of-truth (Dockerfile COPY); byte-copy GitHub->Space so GitHub==Space. Files: gates_manifest.json + 4 policy gate .ts (certifiedRobustness, gaussianMechanismDP, rdpComposition, reedSolomonSingleton). No logic changed; only the lean commit pin string.

gates_manifest.json

@@ -88,7 +88,7 @@
     "description": "a11oy policy gate for CertifiedRobustnessRadius (G39)",
     "lean_theorem": "certifiedRobustnessRadiusBound",
     "lean_file": "Lutar/Robustness/CertifiedRadius.lean",
-    "lean_commit_sha": "1dca00032dfc9aa8559cc6c2e4b63192fcf52371",
+    "lean_commit_sha": "b675cd84caa17080671570c153484c817f8769ac",
     "formula": "certifiedRobustness",
     "rationale": "A gate decision is certifiably robust at input x if the \u2113\u2082 radius R computed from randomized smoothing parameters satisfies R \u2265 R_min_safety. Formula (Cohen-Rosenfeld-Kolter 2019, Theorem 1): R = (\u03c3/2) \u00b7 (\u03a6\u207b\u00b9(p\u0304_A) \u2212 \u03a6\u207b\u00b9(p\u0304_B)) where p\u0304_A is the Monte Carlo lower bound on the top-class probability and p\u0304_B is the upper bound on the runner-up probability.",
     "lean_status": "real"
@@ -230,7 +230,7 @@
     "description": "a11oy policy gate for GaussianMechanismDP (G36)",
     "lean_theorem": "gaussianNoiseSufficiency",
     "lean_file": "Lutar/DP/GaussianMechanism.lean",
-    "lean_commit_sha": "1dca00032dfc9aa8559cc6c2e4b63192fcf52371",
+    "lean_commit_sha": "b675cd84caa17080671570c153484c817f8769ac",
     "formula": "gaussianMechanismDP",
     "rationale": "A DSSE receipt asserting differential privacy via the Gaussian mechanism is accepted only if the declared noise scale \u03c3_claimed satisfies the calibration formula: \u03c3_claimed \u2265 \u0394\u2082f \u00b7 \u221a(2 ln(1.25/\u03b4)) / \u03b5 for the declared (\u03b5, \u03b4, \u0394\u2082f) in the receipt header. If \u03c3_claimed is too small, the DP guarantee is void and the receipt is denied.",
     "lean_status": "real"
@@ -395,7 +395,7 @@
     "description": "a11oy policy gate for RDPSequentialComposition (G38)",
     "lean_theorem": "rdpSequentialCompositionAdditivity",
     "lean_file": "Lutar/DP/RDPComposition.lean",
-    "lean_commit_sha": "1dca00032dfc9aa8559cc6c2e4b63192fcf52371",
+    "lean_commit_sha": "b675cd84caa17080671570c153484c817f8769ac",
     "formula": "rdpComposition",
     "rationale": "For a pipeline of k steps each satisfying (\u03b1, \u03b5\u1d62)-RDP, the sequential composition is (\u03b1, \u03a3\u03b5\u1d62)-RDP (Mironov 2017, Proposition 1). Converting to (\u03b5_dp, \u03b4)-DP: \u03b5_dp = \u03a3\u03b5\u1d62 + ln(1/\u03b4)/(\u03b1-1). The gate accepts a chained receipt only if \u03b5_dp \u2264 declared budget ceiling.",
     "lean_status": "real"
@@ -418,7 +418,7 @@
     "description": "a11oy policy gate for ReedSolomonSingletonBound (G40)",
     "lean_theorem": "reedSolomonMDSProperty",
     "lean_file": "Lutar/CodingTheory/ReedSolomonSingleton.lean",
-    "lean_commit_sha": "1dca00032dfc9aa8559cc6c2e4b63192fcf52371",
+    "lean_commit_sha": "b675cd84caa17080671570c153484c817f8769ac",
     "formula": "reedSolomonSingleton",
     "rationale": "A receipt chain that claims to use Reed-Solomon erasure coding for shard resilience must declare valid RS parameters [n, k, d, q] that satisfy: (1) n \u2264 q (valid parameter range over field GF(q)) (2) 1 \u2264 k \u2264 n (3) d = n - k + 1 (MDS condition \u2014 Singleton bound achieved with equality) (4) claimed_erasure_capacity \u2264 n - k If any condition fails, the resilience claim is unsubstantiated and the gate de",
     "lean_status": "real"

packages/policy/src/gates/certifiedRobustness_gate.ts

@@ -14,7 +14,7 @@
 //
 //   Lean theorem cited: `certifiedRobustnessRadiusBound`
 //   Lean file: Lutar/Robustness/CertifiedRadius.lean
-//   Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
+//   Lean commit SHA: b675cd84caa17080671570c153484c817f8769ac
 //   Lean status: radius positivity and monotonicity are 0-sorry;
 //                full N-P tightness has 2 sorries (sorry map documented).
 //   Severity: ENFORCED (radius below safety floor → hard deny)
@@ -78,7 +78,7 @@ export interface CertifiedRobustnessDecision {
 
 const LEAN_THEOREM = "certifiedRobustnessRadiusBound";
 const LEAN_FILE    = "Lutar/Robustness/CertifiedRadius.lean";
-const LEAN_COMMIT  = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
+const LEAN_COMMIT  = "b675cd84caa17080671570c153484c817f8769ac";
 const FORMULA_STR  =
   "R = (σ/2)·(Φ⁻¹(p̄_A)−Φ⁻¹(p̄_B))  " +
   "[Cohen, Rosenfeld & Kolter 2019 Thm.1; arXiv:1902.02918; ICML PMLR 97:1310]";

packages/policy/src/gates/gaussianMechanismDP_gate.ts

@@ -14,7 +14,7 @@
 //
 //   Lean theorem cited: `gaussianNoiseSufficiency`
 //   Lean file: Lutar/DP/GaussianMechanism.lean
-//   Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
+//   Lean commit SHA: b675cd84caa17080671570c153484c817f8769ac
 //   Lean status: theorem (2 sorries in broader measure-theoretic proof;
 //                gate-level arithmetic theorem has 0 sorries)
 //   Severity: ENFORCED (calibration violation is a hard deny)
@@ -81,7 +81,7 @@ export interface GaussianMechanismDPDecision {
 
 const LEAN_THEOREM  = "gaussianNoiseSufficiency";
 const LEAN_FILE     = "Lutar/DP/GaussianMechanism.lean";
-const LEAN_COMMIT   = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
+const LEAN_COMMIT   = "b675cd84caa17080671570c153484c817f8769ac";
 const FORMULA_STR   =
   "σ_min = Δ₂f · √(2 · ln(1.25/δ)) / ε  [Dwork-Roth 2014, §A.1; DOI:10.1561/0400000042]";
 
@@ -99,7 +99,7 @@ function computeSigmaRequired(l2_sensitivity: number, epsilon: number, delta: nu
  * noise scale satisfies the calibration formula from Dwork-Roth 2014.
  *
  * Lean theorem: `gaussianNoiseSufficiency` (Lutar/DP/GaussianMechanism.lean)
- * Commit: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
+ * Commit: b675cd84caa17080671570c153484c817f8769ac
  * References:
  *   Dwork & Roth (2014) DOI:10.1561/0400000042
  *   Balle & Wang (2018) arXiv:1805.06530

packages/policy/src/gates/rdpComposition_gate.ts

@@ -12,7 +12,7 @@
 //
 //   Lean theorem cited: `rdpSequentialCompositionAdditivity`
 //   Lean file: Lutar/DP/RDPComposition.lean
-//   Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
+//   Lean commit SHA: b675cd84caa17080671570c153484c817f8769ac
 //   Lean status: theorem (2 sorries for measure-theoretic Rényi divergence;
 //                budget arithmetic predicate `rdpBudgetValid` has 0 sorries)
 //   Severity: ENFORCED
@@ -82,7 +82,7 @@ export interface RDPCompositionDecision {
 
 const LEAN_THEOREM = "rdpSequentialCompositionAdditivity";
 const LEAN_FILE    = "Lutar/DP/RDPComposition.lean";
-const LEAN_COMMIT  = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
+const LEAN_COMMIT  = "b675cd84caa17080671570c153484c817f8769ac";
 const FORMULA_STR  =
   "ε_dp = Σᵢεᵢ + ln(1/δ)/(α−1)  [Mironov 2017 Prop.1+3; arXiv:1702.07476; DOI:10.1109/CSF.2017.11]";
 

packages/policy/src/gates/reedSolomonSingleton_gate.ts

@@ -15,7 +15,7 @@
 //
 //   Lean theorem cited: `reedSolomonMDSProperty`
 //   Lean file: Lutar/CodingTheory/ReedSolomonSingleton.lean
-//   Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
+//   Lean commit SHA: b675cd84caa17080671570c153484c817f8769ac
 //   Lean status: gate-level arithmetic (`reedSolomonMDSProperty`) has 0 sorries;
 //                MDS achievability proof has 1 sorry (sorry₁ — discharge route documented).
 //   Severity: ENFORCED
@@ -93,7 +93,7 @@ export interface ReedSolomonSingletonDecision {
 
 const LEAN_THEOREM = "reedSolomonMDSProperty";
 const LEAN_FILE    = "Lutar/CodingTheory/ReedSolomonSingleton.lean";
-const LEAN_COMMIT  = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
+const LEAN_COMMIT  = "b675cd84caa17080671570c153484c817f8769ac";
 const FORMULA_STR  =
   "d = n−k+1 (MDS); t_era ≤ n−k  " +
   "[Reed & Solomon 1960 DOI:10.1137/0108018; Singleton 1964 DOI:10.1109/TIT.1964.1053661]";