Randomness in Gnosis (Lean + TypeScript)

• Parent README: ../README.md
• Formal index: ../FORMAL_LEDGER.md
• Physics sandbox layers (classical ODE, Landauer, BH sketch, CHSH bridge): ./PHYSICS_SANDBOX.md
• Lean corpus index: ../lean/README.md
• ForkRaceFold module list: ../lean/Lean/ForkRaceFoldTheorems/README.md

This note is the package-level map for how Gnosis treats randomness: what is proved in Lean, what is runtime simulation, and what is explicitly not derivable without extrinsic cryptographic assumptions.

Coordinate system

• Negligible advantage / CsPrngSecurity — the formal meaning of “computationally indistinguishable from ideal” in this stack lives in CryptographicPseudorandom.lean. Finite games (IND-PRG, one-query PRF) are in FiniteIndPrgGames.lean and FiniteIndPrfGames.lean.
• Extrinsic crypto claims — anything that imports real-world hardness must surface as named axiom / opaque scaffolding; see CryptographicExternalAxioms.lean.
• Clinamen vs seed security — existence of a +1 swerve does not imply universal CSPRNG security; the anti-bridge is ClinamenCryptoAntiBridge.lean, with narrative separation in ClinamenSeedIndistinguishability.lean.
• Epistemic / deterministic-universe reading — Rule 30 and “indistinguishable from noise” as definitions appear in EpistemicRandomness.lean.
• Aperiodic PRNG story (not CSPRNG proof) — Kronecker–Weyl / certified irrationals / Wallington non-lock narrative: AperiodicPseudorandom.lean.
• Helix geometry for the nested PRNG — rotation indices and distances: LaceyNestedRotation.lean.
• Physical information (Landauer) — bit erasure lower bound k_B T ln 2, entropy-per-bit k_B ln 2, and a typed “substrate” nod (PhysicalBitCarrier): LandauerInformationPhysics.lean. This is orthogonal to cryptographic games: thermodynamic cost of forgetting does not substitute for negligible advantage.
• Black hole information (combinatorial template) — global reversible steps as [Equiv], coarse maps to fewer macro labels (pigeonhole ⇒ not injective), and Equiv.injective_comp so scrambling does not add macro resolution: BlackHoleInformationSketch.lean. Full QFT, Hawking flux, and AdS/CFT stay narrative-only in the module doc.

TypeScript runtime (simulation / procedural)

• @a0n/gnosis/randomness — core barrel: formal anchors (GNOSIS_RANDOMNESS_LEAN_MODULES, GNOSIS_SIMULATION_PRNG_DISCLAIMER, GNOSIS_RANDOMNESS_RUNTIME_STANCE) plus re-exports of createLaceyNestedRng, LaceyNestedRng, helix helpers. Same symbols are on the package root via lib.ts.
• src/randomness.ts — implementation of that barrel.
• src/lacey-nested-prng.ts — Lacey-style nested PRNG; documented as not a CSPRNG; comments point to the Lean modules above.
• src/bitwise-cipher.ts — rotating half-helix frame; same non-crypto stance as other simulation paths.

Build the Lean slice

From open-source/gnosis/lean:

lake build ForkRaceFoldTheorems

Narrower:

lake build ForkRaceFoldTheorems.CryptographicPseudorandom

Adjust module names if your lakefile exposes a different root.

What we do not claim here

• No ontological “true randomness” theorem: the Lean path uses games, advantages, and negligible functions as the rigorous vocabulary.
• No automatic bridge from clinamen (+1) alone to universal CsPrngSecurity; that separation is a design feature, not a gap to paper over.