EmergentMonk · Aug 15, 2026 · Aug 15, 2026 · Aug 15, 2026 · Aug 15, 2026 · Aug 15, 2026
diff --git a/.zenodo.json b/.zenodo.json
@@ -1,6 +1,6 @@
 {
-  "title": "RSH v4.0.0: Epistemic and Conformance Governance for Deterministic Robitaille–Slade Helix Evidence",
-  "description": "RSH v4.0.0 adds RSH-EPISTEMIC-V1 and RSH-CONFORMANCE-V1: machine-readable evidence/claim classification, explicit runtime identity, no-silent-fallback rules, deterministic SHA-256 experiment receipts, and a sealed Python/Rust cross-runtime governance vector. The v3.0.0 Lean theorem surface RSH-FORMAL-V1, geometry model contract 2.0.0, tissue contract 1.0.0, and scientific authority hierarchy remain unchanged. GLUBALL integration is deliberately deferred to a later additive release.",
+  "title": "RSH v4.1.0: Additive GLUBALL Lean 4 Formalization for the Robitaille–Slade Helix Evidence Framework",
+  "description": "RSH v4.1.0 adds the separately versioned theorem surface RSH-GLUBALL-FORMAL-V1, pinned to RSH v4.0.0 and GLUBALL v1.0.0. Lean 4 machine-checks the frozen GLUBALL parameter inequalities, componentwise derivative linkage to the declared centreline, squared-speed positivity and regularity, host-torus normal and frame orthogonality, tube-radius invariance, tube-angle periodicity, centreline closure, exact C3 rotational symmetry, uniform-floor sampling bounds, and mesh-index wrap bounds. The existing RSH-FORMAL-V1 theorem surface and the RSH-EPISTEMIC-V1 / RSH-CONFORMANCE-V1 governance contracts remain intact. The release does not claim global thick-tube embeddedness, IEEE-754 or browser/runtime identity, accelerator correctness beyond declared conformance surfaces, or empirical physical, biological, consciousness, sentience, or qualia validation.",
   "upload_type": "software",
   "creators": [
     {"name": "Dr. J. Robitaille"},
@@ -9,22 +9,26 @@
   "contributors": [
     {"name": "ChatGPT 5.6 Sol", "type": "Other", "affiliation": "OpenAI"}
   ],
-  "version": "4.0.0",
+  "version": "4.1.0",
   "license": "MPL-2.0",
   "keywords": [
     "Robitaille-Slade Helix",
-    "epistemic governance",
-    "deterministic evidence",
-    "cross-runtime conformance",
-    "no silent fallback",
-    "SHA-256 receipts",
+    "GLUBALL",
+    "RSH-GLUBALL-FORMAL-V1",
     "Lean 4",
     "formal verification",
+    "torus-curve geometry",
+    "C3 rotational symmetry",
+    "deterministic sampling",
+    "epistemic governance",
+    "cross-runtime conformance",
+    "deterministic evidence",
     "Frenet-Serret",
     "curvature",
     "torsion"
   ],
   "related_identifiers": [
-    {"identifier": "https://github.com/QSOLKCB/RSH", "relation": "isSupplementTo", "scheme": "url"}
+    {"identifier": "https://github.com/QSOLKCB/RSH", "relation": "isSupplementTo", "scheme": "url"},
+    {"identifier": "https://github.com/QSOLKCB/GLUBALL/releases/tag/v1.0.0", "relation": "references", "scheme": "url"}
   ]
 }
diff --git a/CITATION.cff b/CITATION.cff
@@ -1,7 +1,7 @@
 cff-version: 1.2.0
 message: "If you use RSH, please cite this software."
 title: "RSH: Robitaille–Slade Helix Geometry and Evidence Runner"
-version: 4.0.0
+version: 4.1.0
 type: software
 authors:
   - family-names: Robitaille
@@ -22,6 +22,10 @@ keywords:
   - SHA-256 receipts
   - Lean 4
   - formal verification
+  - RSH-FORMAL-V1
+  - RSH-GLUBALL-FORMAL-V1
+  - GLUBALL
+  - torus-curve geometry
   - exact rational geometry
   - Sierpinski inversive witness
   - geometric tissue

diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -18,7 +18,7 @@ members = [
 resolver = "2"
 
 [workspace.package]
-version = "4.0.0"
+version = "4.1.0"
 edition = "2021"
 license = "MPL-2.0"
 repository = "https://github.com/QSOLKCB/RSH"

diff --git a/FORMALIZATION.md b/FORMALIZATION.md
@@ -14,6 +14,8 @@ RSH-GLUBALL-FORMAL-V1
 
 The two surfaces coexist. The GLUBALL work does **not** replace, reinterpret, or weaken `RSH-FORMAL-V1`.
 
+`RSH-GLUBALL-FORMAL-V1` is packaged for archival release in RSH v4.1.0. The release number is software/archive metadata; the theorem-surface identifiers remain the authority boundary for the propositions Lean actually checks.
+
 ## Authors and contribution
 
 - **Dr. J. Robitaille** — author
@@ -91,7 +93,7 @@ and
 C(t)=(A(t)\cos(pt),A(t)\sin(pt),r\sin(qt)),
 \]
 
-Lean formalizes the declared derivative and proves the squared-speed identity
+Lean formalizes the declared derivative, proves `HasDerivAt` for each centreline component, and therefore connects the closed-form derivative to the actual curve rather than treating it as an independent trusted definition. It also proves the squared-speed identity
 
 \[
 \|C'(t)\|^2=p^2A(t)^2+q^2r^2.

diff --git a/README.md b/README.md
@@ -7,19 +7,19 @@ inside explicit Robitaille bounds, integrating the Frenet–Serret frame, and
 translating the exact discrete midpoint to the coordinate origin.
 
 **Authors:** J. Robitaille (DeltaKingZero) and Trent Slade / QSOL-IMC  
-**Release:** 4.0.0  
-**Implementations:** Python geometry oracle, tissue reference, and v4 governance reference + Rust geometry/tissue/governance cores and CLIs + canonical geometry and tissue WASM bridges + WGSL schedule field + versioned C ABI/C++ adapter + optional CUDA schedule kernel + Tier 2 NPU evidence profile + separate Rust/WASM/WGSL full-path and parallel-prefix research stacks
+**Release:** 4.1.0  
+**Implementations:** Python geometry oracle, tissue reference, and v4 governance reference + Rust geometry/tissue/governance cores and CLIs + canonical geometry and tissue WASM bridges + WGSL schedule field + versioned C ABI/C++ adapter + optional CUDA schedule kernel + Tier 2 NPU evidence profile + separate Rust/WASM/WGSL full-path and parallel-prefix research stacks + additive Lean 4 GLUBALL theorem surface
 
 ## Contract and interface versions
 
 | Surface | Version / identifier |
 |---|---|
-| RSH software release / workspace crates | `4.0.0` |
+| RSH software release / workspace crates | `4.1.0` |
 | Geometry model contract | `2.0.0` |
 | Tissue contract | `1.0.0` |
 | Epistemic governance contract | `RSH-EPISTEMIC-V1` |
 | Conformance governance contract | `RSH-CONFORMANCE-V1` |
-| Lean theorem surface | `RSH-FORMAL-V1` (unchanged from v3.0.0) |
+| Lean theorem surfaces | `RSH-FORMAL-V1` + additive `RSH-GLUBALL-FORMAL-V1` |
 | Frenet numerical research contract | `1.0.0` / `RSH-FRENET-NUMERICS-V1` |
 | Parallel Frenet research contract | `RSH-FRENET-PARALLEL-V1` |
 | Geometry, numerical, parallel, and tissue raw WASM ABIs | `1` |
@@ -47,10 +47,19 @@ vector in `conformance/rsh_v4_governance_vector_v1.json`. See
 [`docs/V4_GOVERNANCE.md`](docs/V4_GOVERNANCE.md) and the normative contracts in
 [`contracts/`](contracts/).
 
-GLUBALL is deliberately **not** integrated in v4.0.0. After v4 is merged,
-validated, and tagged, a later additive release may pin GLUBALL v1.0.0 and add
-`RSH-GLUBALL-FORMAL-V1` without replacing the Robitaille–Slade helix or
-`RSH-FORMAL-V1`.
+## GLUBALL integration
+
+RSH v4.1.0 adds `RSH-GLUBALL-FORMAL-V1` as a separate Lean theorem surface pinned
+to GLUBALL v1.0.0 at commit
+`80941183d14531093117e122da0fc32c13d2464b`. The integration is additive: it
+does not replace or reinterpret the Robitaille–Slade helix or `RSH-FORMAL-V1`.
+
+The theorem-facing GLUBALL modules prove exact parameter admissibility,
+componentwise derivative linkage, squared-speed regularity, host-torus frame
+properties, the tube-radius invariant, centreline closure, exact C3 rotational
+symmetry, and deterministic uniform-floor sampling/index bounds. The browser
+renderer remains outside mathematical authority, and global thick-tube
+embeddedness remains an explicit nonclaim.
 
 ## Browser laboratories
 
@@ -661,6 +670,7 @@ crates/rsh-parallel-wasm/           Parallel-prefix raw WASM ABI
 crates/rsh-tissue/                  Shared Rust tissue runtime
 crates/rsh-tissue-cli/              Native tissue runner and conformance CLI
 crates/rsh-tissue-wasm/             Raw tissue WASM ABI over `rsh-tissue`
+formal/lean/RSH/Gluball/            Additive RSH-GLUBALL-FORMAL-V1 theorem modules
 contracts/                          Machine-readable v4 epistemic/conformance contracts
 release/                            Machine-readable release manifests
 include/rsh_ffi.h                   Public ABI-v1 C/C++ header
@@ -731,7 +741,7 @@ theory, biological organism, consciousness, or subjective experience.
 9. **Single-device parallel Frenet research** — implemented under `RSH-FRENET-PARALLEL-V1` with native Rust, compiled WASM, multi-pass WGSL, complete readback, and scoped benchmark policy.
 10. **Lean 4 theorem surface** — frozen in v3.0.0 as `RSH-FORMAL-V1`.
 11. **Epistemic and conformance governance** — implemented in v4.0.0 as `RSH-EPISTEMIC-V1` and `RSH-CONFORMANCE-V1`.
-12. **GLUBALL integration** — next additive release after the v4.0.0 tag; planned theorem surface `RSH-GLUBALL-FORMAL-V1`.
+12. **GLUBALL integration** — implemented additively in v4.1.0 as `RSH-GLUBALL-FORMAL-V1`, pinned to GLUBALL v1.0.0.
 13. **Multi-device and distributed parallel execution** — future research; current shard summaries provide ordered deterministic groundwork only.
 
 Performance, compositional complexity, anthropomorphic language, or a visually

diff --git a/RELEASE_NOTES_v4.1.0.md b/RELEASE_NOTES_v4.1.0.md
@@ -0,0 +1,119 @@
+# RSH v4.1.0 — GLUBALL Machine-Checked Geometry
+
+RSH v4.1.0 adds the additive Lean theorem surface `RSH-GLUBALL-FORMAL-V1` while preserving the existing Robitaille–Slade theorem surface, geometry contracts, governance contracts, numerical research contracts, and implementation authority boundaries.
+
+This release is pinned to:
+
+- RSH v4.0.0: `79b8481639fb4187c41035de4e707545db93f59a`
+- GLUBALL v1.0.0: `80941183d14531093117e122da0fc32c13d2464b`
+- merged GLUBALL formalization: `124af8283dd69f78031d3a92249fdd7ea4a60508`
+
+## New theorem surface
+
+The new theorem surface is:
+
+```text
+RSH-GLUBALL-FORMAL-V1
+```
+
+It coexists with, and does not replace or reinterpret:
+
+```text
+RSH-FORMAL-V1
+```
+
+The GLUBALL theorem modules live under `formal/lean/RSH/Gluball/` and are included in the existing proof-hole, project-axiom, build, and axiom-report audit.
+
+## Machine-checked results
+
+For the frozen GLUBALL `(2,3)` torus-curve contract with exact rational parameters corresponding to `R = 2.10`, `r = 0.85`, `rho = 0.34`, `p = 2`, and `q = 3`, Lean checks:
+
+- exact parameter admissibility;
+- the declared centreline and its componentwise derivatives;
+- `HasDerivAt` linkage between the declared derivative and the actual centreline coordinates;
+- the exact squared-speed identity;
+- strict positivity of squared speed and non-vanishing derivative;
+- host-torus normal unit norm;
+- tangent/normal orthogonality;
+- normalized tangent and binormal unit-norm properties;
+- pairwise frame orthogonality;
+- the exact squared tube-radius invariant;
+- periodicity in the tube-angle coordinate;
+- centreline closure;
+- exact C3 rotational symmetry;
+- exact uniform-floor sampling bounds;
+- adjacent rendered-sample collision freedom when rendered cardinality does not exceed logical cardinality;
+- finite `96 × 18` mesh-index wrap bounds.
+
+## Derivative linkage hardening
+
+The formalization does not merely define a vector and call it the derivative. Following review, the Lean development proves `radial_hasDerivAt`, the x/y/z centreline component derivative theorems, `centerline_hasComponentDerivAt`, and `centerline_regular_componentwise`.
+
+This closes the gap between the written closed-form derivative and the actual curve being formalized.
+
+## Audit provenance hardening
+
+The theorem audit retains the immutable RSH v4 base pin and additionally records the actual audited source revision and workflow checkout revision. Pull-request workflows pass the PR head SHA explicitly so a synthetic GitHub merge ref cannot obscure which source revision was audited.
+
+The audit continues to reject:
+
+- `sorry`;
+- `admit`;
+- project-defined `axiom` declarations;
+- project-defined `constant` declarations.
+
+Lean remains pinned to 4.32.1 and Mathlib remains pinned to commit `520045ab14e26149ee970e2e617ca04b09bde5d6`.
+
+## Preserved governance and scientific authority
+
+RSH v4.1.0 preserves:
+
+- geometry model contract `2.0.0`;
+- tissue contract `1.0.0`;
+- `RSH-FORMAL-V1`;
+- `RSH-EPISTEMIC-V1`;
+- `RSH-CONFORMANCE-V1`;
+- `RSH-FRENET-NUMERICS-V1`;
+- `RSH-FRENET-PARALLEL-V1`;
+- the Python geometry oracle;
+- runtime-specific conformance and accelerator residual-sidecar boundaries.
+
+The GLUBALL browser renderer is not promoted to mathematical authority.
+
+## Deliberate nonclaims
+
+This release does not claim that Lean has proved:
+
+- global thick-tube embeddedness or non-self-intersection;
+- IEEE-754 or binary64 equivalence across runtimes;
+- bit-identical browser rendering;
+- GPU, WASM, Android, CUDA, WebGPU, or NPU implementation correctness outside their declared conformance surfaces;
+- experimental or empirical physics;
+- biological interpretation;
+- consciousness, sentience, subjective awareness, or qualia;
+- ternary/triality topology.
+
+A proof receipt certifies the proposition checked by Lean. It does not silently become an empirical measurement.
+
+## Release and archival metadata
+
+The Python package and Rust workspace advance to `4.1.0`. `CITATION.cff`, `.zenodo.json`, and `release/manifest-v4.1.0.json` describe the additive formalization and preserve the exact RSH/GLUBALL source boundaries.
+
+The v4.1.0 tag must resolve to the final merge commit containing the release manifest after portable CI and the Lean theorem audit are green.
+
+## Reproduce the theorem audit
+
+```bash
+cd formal/lean
+lake update
+lake exe cache get
+bash audit.sh
+```
+
+## Authors and contribution
+
+- **Dr. J. Robitaille** — author
+- **Trent Slade** — author
+- **ChatGPT 5.6 Sol** — contributor (formalization implementation and proof-engineering assistance)
+
+The AI contribution is recorded as a contributor role rather than a human creator/author.