Snapkitty/sovereign-agc

SOVEREIGN AGC

Apollo Guidance Computer — The Real Implementation

---

Saturn V · July 16, 1969	The AGC — 4KB RAM, 2 MHz	The destination

---

What This Is

The Apollo Guidance Computer ran on 4,096 words of erasable memory and 36,864 words of core rope. It used 15-bit 1's complement arithmetic with no floating-point hardware, minimax polynomial approximations for transcendental functions, and a handwritten phase-plane attitude controller. It landed human beings on the Moon.

This repository is Ahmad Parr's complete reconstruction of that computer — not a simulation, not a wrapper around someone else's emulator, but a ground-up reimplementation of every mathematical system from documented primary sources: the Virtual AGC project, Battin's An Introduction to the Mathematics and Methods of Astrodynamics, Luminary 099, Colossus 249, and the original Hastings polynomial coefficient tables.

---

How It Was Built

Ahmad used AI systems as research and implementation tools, the same way an engineer uses a compiler — as infrastructure, not as the architect. He researched with Perplexity in loops, directed different AI systems at different technical domains, and wrote the hardest parts himself.

What	Who	How
R orbital mechanics	Ahmad	Own code, Perplexity research loops
Fortran 2018 1's-complement ALU	Kimi	Directed with exact AGC specifications
Ada SPARK verification	Nova Parr	Ghost contracts on mathematical product
APL interpretive dispatcher	Gemini	Replaced verbose branching with array indexing
BURNBABY Janet table	Grok	6-program ignition state machine
Idris 2 Parrgorithm	Ahmad	Wrote it himself — no believe_me, no holes
Lean 4 safety proofs	Ahmad	Wrote them himself — zero sorry
OpenQASM ignition circuit	Ahmad	Quantum extension of BURNBABY
Forest-Ruth integrator	Nova Parr	4th-order symplectic with exact coefficients
Encke RK4 deviation	Nova Parr	q-factor formulation for stability

---

What's Actually Here

r/ — Orbital Mechanics (2,350 lines)

Ahmad's R library. Every function is a real implementation with citations to the primary astrodynamics literature.

File	Contents
kepler.R	Stumpff C(z)/S(z), safeguarded Newton+bisection Kepler solver, kepler_propagate_many (universal variable, N satellites), kepler_propagate_grid
elements.R	Cartesian ↔ Keplerian ↔ Modified Equinoctial Elements (MEE), analytic MEE Jacobian J_{x←q}, inverse Jacobian
propagator.R	MEE equations of motion (Gauss VOP), RK4 integrator, J2 acceleration, J2 secular rates, kepler_mee_propagate_j2_secular, J2/J3/J4 zonal
gravity.R	Full spherical harmonic gravity: kepler_associated_legendre, C_nm/S_nm model, body-fixed→inertial rotation (R3), kepler_spherical_harmonic_force closure
stm.R	State transition matrix: kepler_two_body_jacobian, variational equations, RK4 propagator, covariance propagation

The MEE formulation is nonsingular at circular and equatorial orbits. The spherical harmonic model handles zonal, tesseral, and sectorial terms. The STM propagates uncertainty correctly — phi %*% state0 maps perturbations, not the nominal state.

---

fortran/ — Fortran 2018 AGC Interpreter (1,431 lines)

Kimi's clean-room implementation. Fortran 2018 modules, no COMMON blocks, proper kinds.

agc_assembly_symbols.f90 — The constants module. INT64_KIND, AGC_WORD_MASK = 0x7FFF, AGC_SIGN_BIT = 0x4000, AGC_PLUS_ZERO = 0x0000, AGC_MINUS_ZERO = 0x7FFF. Every AGC numeric convention in one place.

agc_fixed_point.f90 — The 1's complement ALU:

pure function ones_comp_add(a, b) result(sum)
  ! End-Around Carry: fold carry out of bit 14 back into bit 0
  raw = iand(a, AGC_WORD_MASK) + iand(b, AGC_WORD_MASK)
  raw = iand(raw, AGC_WORD_MASK) + ishft(raw, -15)  ! fold 1
  raw = iand(raw, AGC_WORD_MASK) + ishft(raw, -15)  ! fold 2 (rare)
  sum = iand(raw, AGC_WORD_MASK)
end function ones_comp_add

The double fold handles the rare case where the EAC correction itself generates a carry — the case most implementations miss. Also: agc_shift_right_rne (round-to-nearest-even using ibits() for performance), agc_q28_to_q14_rne (specialized constant-fold for DP→SP downscaling).

agc_trig.f90 — Hastings minimax polynomial approximations, exact coefficient values from the Luminary listing:

! sin(x) ≈ c1*x + c3*x^3 + c5*x^5 + c7*x^7 + c9*x^9
real, parameter :: SIN_C1 =  1.57079631847
real, parameter :: SIN_C3 = -0.64596371106
real, parameter :: SIN_C5 =  0.07968967928

forest_ruth.f90 — 4th-order symplectic integrator. Energy drift is bounded oscillatory, not secular. Exact Forest-Ruth coefficients: THETA = 1.35120719195965764.

encke_rk4.f90 — Encke's method with RK4. The q-factor keeps the sensitive difference of two nearly-equal gravitational accelerations numerically stable.

---

ada/ — SPARK Formal Verification (207 lines)

Nova Parr's Ada SPARK implementation of DMPSUB — the AGC's double-precision multiply. Every step of the carry chain is machine-checked.

-- Ghost functions let GNATprove reason about mathematical values
function Math_Product (A0, A1, B0, B1 : Integer_64) return Integer_64
  with Ghost,
       Post => Math_Product'Result = (A0 * 2**14 + A1) * (B0 * 2**14 + B1);

-- Post-condition: if no overflow, the limbs equal the mathematical product mod 2**42
Post =>
  (if not OVFIND then
     Limbs_To_TP(MPAC(0), MPAC(1), MPAC(2)) =
     Math_Product(A0_Old, A1_Old, B0, B1) mod 2**42)

Feed dmp_sub.ads + dmp_sub.adb to gnatprove to discharge the carry-chain assertions.

---

idris/ — Dependently-Typed SR5 Hard Gate (99 lines)

Ahmad wrote this himself. The SR5 overflow invariant is carried as a proof in the type, not asserted at runtime.

record RegisterDP28 where
  constructor MkDP28
  value       : Nat
  bounded_prf : value `LT` DP28_MAX  -- proof travels with the data

hardGateSR5 : RegisterDP28 -> RegisterDP28
hardGateSR5 (MkDP28 val prf) =
  MkDP28 (val `div` 32) (shift_right_5_invariant val prf)
  -- The divided value is PROVEN < 2^28 at compile time.

No believe_me. No holes. shift_right_5_invariant is proved by div32_shrinks which is proved by induction on Nat. The maneuver timer cannot overflow — mathematically, not by assertion.

---

apl/ — Array-Oriented Dispatcher (193 lines)

Gemini's implementation. The AGC's DANZIG/INDJUMP dispatch table becomes a single APL expression:

⍝ 32 opcodes, O(1) lookup, zero branching
⍎ (32|CYR) ⊃ INDJUMP_TBL

⍝ Mode-aware push-up: array switch replaces nested ifs
DECR ← (0 1 ¯1 ⍳ MODE) ⊃ 2 3 6

Full 32-entry INDJUMP_TBL and 4-entry STORE_TBL. Every address mode (direct, indexed, push-up) and every store code path (STORE, STODL, STOVL, STCALL) is implemented. Run in any Dyalog APL session.

---

burnbaby/ — Ignition Module

The master ignition routine and its formal verification.

fortran/burnbaby.f90 — Grok's Janet table. Six programs (P12/P40/P41/P42/P63/ABORT), one countdown, all branching resolved by table lookup:

TIG-35 → blank DSKY
TIG-30 → restore display, start ullage  
TIG-5  → V99 "Please Enable Engine"
TIG-0  → IGNYET? check → IGNITION → [Janet(WHICH,10)]

lean/BurnBaby.lean — Ahmad's proofs. The only zero-sorry theorems in the codebase:

theorem thrust_requires_astronaut (ctx : IgnitionContext) :
    evaluate_ignition ctx = EngineState.Thrust → ctx.AstronautGo = true

theorem thrust_at_tig_zero (ctx : IgnitionContext) :
    evaluate_ignition ctx = EngineState.Thrust → ctx.TGO ≤ 0

These are not tests. They are proofs. The engine cannot fire without crew consent and cannot fire before TIG-0 — the safety invariants of BURNBABY, formalized in Lean 4, discharged without sorry.

qasm/burnbaby.qasm — Ahmad's quantum extension. The WHICH register (program selector) in superposition, collapsed by the TIG-5 astronaut consent measurement. ANU vacuum entropy seeds ullage settling noise.

---

Compared to the Original

	Original AGC (1969)	Sovereign AGC (2026)
Word width	15-bit 1's complement	Bit-exact emulation (EAC double-fold)
Trig functions	Hastings polynomials, fixed-point	Faithfully reproduced, same coefficients
Orbital propagator	Encke deviation + conic	Encke RK4 + Forest-Ruth 4th-order symplectic
Gravity model	Point mass + J2	Full spherical harmonics C_nm/S_nm to degree 4+
Targeting	Lambert TIMETHET	Lambert + bisection + STM + covariance
Dispatcher	AGC assembly, sequential	APL array-indexed, O(1), deterministic
Ignition	BURNBABY Janet table	BURNBABY + OpenQASM 3.0 quantum variant
Arithmetic proofs	None	Ada SPARK carry-chain contracts
Safety proofs	Crew training, hardware qual	Lean 4 zero-sorry machine proofs
SR5 gate	Hardware shift register	Idris 2 type-carrying bounds proof
Languages	1 (AGC assembly)	7
Energy conservation	Discrete impulse model	Bounded oscillation (symplectic)

The original AGC landed on the Moon with no formal verification. This reconstruction has the mathematics to prove it was correct to do so.

---

Three Repos — What Goes Where

This reconstruction spans three repositories. They are related but distinct:

Repo	Role	What's Here
sovereign-agc (this repo)	Complete canonical implementation	All languages, R orbital mechanics, APL dispatcher, Ada SPARK, Idris 2 Parrgorithm, Lean 4 zero-sorry proofs, OpenQASM
sovereign-apollo	Fleet build — orchestration record	TypeScript deterministic baseline (Claude), FORTRAN 77 port (Meta), full mission timeline, 22-event deterministic replay
sovereign-fortran-agc	Canonical source corpus	Fortran orbital mechanics, PTX/SASS kernels, no_std Rust CUDA driver, Forth executive, Lean stubs

sovereign-apollo documents how one human (Ahmad) directed seven AI systems to rebuild the AGC — the process, attribution, and fleet coordination. sovereign-fortran-agc is the original email corpus: the orbital mechanics and GPU stack that came out of Ahmad's audit of Nova Parr's work. This repo is where all of it was assembled into a single formally-verified reconstruction.

---

License

Three-layer license matching the three technical domains:

Layer	Files	License
Sovereign Core	burnbaby/, apl/	Sovereign Source License v1.0
Mathematical / Algorithmic	fortran/, r/, ada/, idris/	Apache License 2.0
Formal Proofs	burnbaby/lean/, idris/Parrgorithm.idr	MIT License

The substrate is not for sale. It is not for porting. It is for Execution in the Wild. — Bel Esprit d'Accord Trust

---

© 2026 Bel Esprit d'Accord Trust · SNAPKITTYWEST

Ahmad Ali Parr · Jessica Westerhoff