Skip to content

README.md

Latest commit

 

History

History
78 lines (58 loc) · 3.77 KB

README.md

File metadata and controls

78 lines (58 loc) · 3.77 KB

ugp-lean

Research Program

This repository is part of the Reflexive Reality research program by Nova Spivack.

What this formalizes: UGP Formalization (§B2): machine-checked Lean 4 formalization of the Universal Generative Principle — ridge sieve, GTE orbit, Quarter-Lock, Turing universality, self-reference.

Link Description
Research page Full index of all papers, programs, and Lean archives
Full abstracts Complete abstract for this library's papers
Zenodo program hub Citable DOI hub for the NEMS program

All results are machine-checked in Lean 4 with a zero-sorry policy on proof targets. See MANIFEST.md for the sorry audit (if present).

Lean 4 formalization of the Universal Generative Principle (UGP) and Generative Triple Evolution (GTE). Proves RSUC, certifies the n=10 sieve and canonical orbit, Quarter-Lock, and Turing universality. The classification is n-parameterized: predicates and candidate sets are indexed by ridge level n; at n=10 this yields the certified Lepton Seed.

Build

lake update
lake build

Toolchain: Lean 4.29.0-rc3, Mathlib v4.29.0-rc3.

Documentation

Document Description
docs/README.md Documentation index
docs/BUILD.md Build guide, troubleshooting
docs/MODULES.md Module reference
docs/THEOREMS.md Theorem catalog
docs/DESIGN.md Non-circularity, architecture
docs/ADVISOR_STATUS.md Advisor status: scope, soundness, gaps

Module structure

Layer Modules Purpose
Core RidgeDefs, MirrorDefs, TripleDefs, SievePredicates, Disconfirmation, RidgeRigidity, MirrorAlgebra Definitions, no computation
Compute PrimeLock, Sieve, SieveExtended, ExclusionFilters, DecidablePredicates Algorithms, native_decide
Classification Bounds, TheoremA, TheoremB, RSUC, FormalRSUC, MonotonicStrengthening RSUC two-theorem architecture
GTE Evolution, Orbit Canonical orbit
Phase4 DeltaUGP, GaugeCouplings, UCL, PR1 Gauge, δ_UGP, stubs
Universality Rule110, UWCA, TuringUniversal, ArchitectureBridge Rule 110, Turing-universal
Instance NemSBridge NEMS Paper 25 bridge

Non-circularity: Core/ may not import Compute/. See docs/DESIGN.md.

Key theorems

  • ridgeSurvivors_10 — At n=10, survivors = {(24,42), (42,24)}
  • theoremA_general — ∀n, UnifiedAdmissibleAt n t → t ∈ CandidatesAt n; theoremA is the n=10 corollary
  • rsuc_theorem — Residual Seed Uniqueness; MDL selects Lepton Seed (1,73,823)
  • quarterLockLaw — k_M = k_gen2 + ¼k_L²
  • canonical_orbit_triples — (1,73,823) → (9,42,1023) → (5,275,65535)
  • strengthening_cannot_add_survivors — Predicate strengthening cannot add survivors to Residual
  • ugp_is_turing_universal — UGP substrate Turing-universal

References

  • MANIFEST.md — Paper→Lean theorem mapping
  • Assumptions.md — Premise ledger
  • UGP Formalization paper — NEMS_PAPERS/UGP_GTE_Formalization/ (definitive formal spec; theorem-indexed mapping)
  • UGP_LEAN_PROGRAM_ROADMAP.md (in workspace)

Archival software (Zenodo): https://doi.org/10.5281/zenodo.19429247

Archival paper (Zenodo preprint) (Zenodo): https://doi.org/10.5281/zenodo.19433539
⚡