SR-71 BlackGlider

Conway evolves the flight. BlackGlider renders the history.

SR-71 BlackGlider is a mathematically uncompromised flight through Conway’s Game of Life. A single global B3/S23 universe is the whole physical truth. Surfaces, textures, altitude, banking and curved spacetime belong to a one-way geometric embedding: they may reveal and dramatise Conway’s causal history, but they may never author it.

Important

This repository establishes and gates the architectural foundation; it is not yet a complete game. The executable spike contains an exact B3/S23 kernel, a genuine stable-reflector turn, causal counterfactual measurement, and a curved flight embedding demonstrated unable to change the canonical history.

Table of Contents

• The step forward
• What the foundation establishes
• What is verified today
  • What those numbers do not mean
  • Why the badge no longer says "foundation proven"
• Flight geometry
• Turns
• Repository status
• AI-Assisted Installation
• Licence

The step forward

This is the third project in a line of increasingly demanding questions about what a game can honestly claim when its world is Conway’s Life.

Project	Question opened	What SR-71 carries forward
F19 Stealth Glider	Can a five-cell glider cross a hostile evolving substrate, with disturbance measured against a counterfactual world?	The substrate is computation rather than scenery; phase and causal trace are gameplay truth.
F117A Stealth Glider	Can that same evolving world become radar cover, with a 3D flight experience remaining downstream of a 2D cellular automaton?	Presentation may become richer without pretending that a different cellular physics exists underneath it.
SR-71 BlackGlider	Can surfaces, textures, local frames and apparent spacetime curvature create flight while every objective manoeuvre remains a real Conway reaction?	The separation becomes constitutional: no player overlay, no splicing, no imposed heading. There is one global Life history and a proof-bearing observer.

The change is not merely faster aircraft or more elaborate graphics. F19 and F117A admitted a pre-contact kinematic player layer. That layer could reproduce straight glider flight exactly, but a commanded heading substitution was not an isolated glider’s B3/S23 evolution. SR-71 does not inherit that exception.

Its governing proposition is stronger:

For a fixed initial pattern G₀, every canonical state is exactly Gₜ = Lifeᵗ(G₀), independently of rendering, camera state, textures, spacetime embedding and every post-launch user input.

What the foundation establishes

The foundation tests currently establish:

• all 512 possible nine-bit local configurations implement exactly B3/S23;

• the demonstration counterfactual is a stable 49-cell Snark reflector;

• an incoming NE glider is turned into an outgoing SE glider by raw B3/S23;

• after recovery, the actual/no-launch difference is exactly the outgoing five cells—no causal ash;

• aggressively changing bank, pitch and surface curvature produces a canonical history byte-identical to the headless run;

• the exact 45-degree chart maps Conway NE/SE/SW/NW to BlackGlider up/forward/down/back;

• a canonical byte encoding replays to the same 240-generation result;

• every possible 4-by-4 world agrees for one synchronous generation with an independently written finite-grid oracle;

• all 16 combinations of glider heading and phase are detected and exhibit the correct four-generation translation;

• presentation inputs have no capability to modify a World and remain non-interfering over the exercised histories;

• an Idris2 companion constructively checks all 18 legal combinations of centre state and Moore-neighbour count against a separately stated B3/S23 specification, plus the exact heading map, deterministic iteration, observer exclusion, and declared causal-radius function.

These statements have deliberately different strengths. The Idris2 results are formal theorems about the compact model in that file. The Rust results are exhaustive over stated finite domains or bounded traces. There is not yet a machine-checked refinement proof that the Rust implementation is the Idris2 model, nor a proof about the compiled executable.

What is verified today

Measured on 2026-08-07 by running each tool in a clean working tree. Every figure below is a tool output, not a status-file assertion.

Gate	Result	What it actually covers
cargo test --all-targets	12/12 pass	Constitutional obligations C1–C7 (tests/foundation.rs) and C8–C13 (tests/constitutional.rs). 613 LOC of kernel across src/.rs, 357 LOC of tests. The crate is #![forbid(unsafe_code)] and has *zero external dependencies. There are no unit tests inside src/lib.rs.
zig build test (in src/interface/ffi/)	11/11 tests, 5/5 steps	3 inline unit tests in src/main.zig, 8 integration tests in test/integration_test.zig.
idris2 --typecheck abi.ipkg	PASS	The shipped ABI seam — three modules under src/interface/Abi/ (Types.idr, Layout.idr, Foreign.idr). This is the one Idris2 artefact the FFI depends on.
scripts/check-proofs.sh {idris2,coq,agda,lean4}	PASS, 10 gated modules	7 Idris2 (Idris2 0.7.0), 1 Coq (coqc 8.20.1), 1 Agda (2.6.4.3), 1 Lean (4.32.2). The quarantine list is empty: no module is recorded as known-broken.
tests/aspect_tests.sh	PASS	SPDX header coverage and a dangerous-construct scan over proof code.

What those numbers do not mean

Read the caveats with the same weight as the counts.

• The Rust coverage is exhaustive, not general. 512/512 local B3/S23 rule configurations and 65,536/65,536 four-by-four worlds are proofs by exhaustion over a stated finite domain. The Snark result is a single 240-generation trace. None of these is a proof over unbounded worlds or unbounded time.

• Three of the four prover suites are template exemplars. The Coq (TypeSafety.v), Agda (Properties.agda) and Lean (ApiTypes.lean) modules are verbatim RSR template stubs — a toy type system, list-append length, and a Result functor. They compile and they are gated, and they prove nothing about Conway physics. Their green must not be read as domain verification. The Idris2 MANIFEST already records this for Types.idr.

• No refinement connects the model to the implementation. The Idris2 proofs and the Rust kernel are verified separately; nothing machine-checked establishes that they agree, and nothing is proved about the compiled executable.

• The Idris2 ABI modules constrain a model, not the shipped FFI. grep finds no reference to CABICompliant or StructLayout outside verification/proofs/ and src/interface/Abi/; the only inhabitant is a fieldless empty struct. No Rust or Zig type is presented to the certificate.

• The renderer and the mission semantics do not exist. STATE.a2ml records 25% complete. There is no playable level, no production renderer and no control semantics.

• verification/proofs/tlaplus/StateMachine.tla is unwired — check-proofs.sh supports only idris2|lean4|agda|coq — and is an uninstantiated template modelling a generic request pipeline, irrelevant to this project.

Why the badge no longer says "foundation proven"

It previously did. The label has been lowered to foundation exhaustively tested because "proven" over-reads the evidence: some obligations really are proofs by exhaustion, but C2–C4 rest on one bounded trace, C8 covers only four-by-four worlds for one generation, and the three non-Idris2 prover gates carry no domain content at all. The foundation is green and the green is real; it is not a general proof, and the badge should not imply one.

Run the evidence yourself — this is the golden path for humans and agents alike:

just test && just quality

just test runs the Rust suite, the Zig FFI tests, the shipped ABI seam typecheck, and all four check-proofs.sh gates. just quality runs fmt-check, lint and the test suite again. An absent prover toolchain is fatal by design: a gate that cannot run must never report OK.

See the mathematical contract, the one-way architecture, and the claim ledger. The proof frontier states how far verification can usefully go before a finite mission must be engineered and frozen. The debt register is the honest inventory of what is unwired, stubbed, ungated or unimplemented, and is the right place to look before trusting any green signal here.

Flight geometry

Canonical cell coordinates remain integer lattice coordinates (x,y). The initial BlackGlider chart is the exact linear map

\$X=(x+y)/2,qquad Y=(x-y)/2.\$

The implementation stores the exact doubled coordinates u=x+y, v=x-y and divides only at the raster boundary. Its inverse exists exactly on the same-parity sublattice, so no rounding enters the canonical chart.

It re-expresses genuine diagonal Life motion as orthogonal flight directions:

Conway heading	BlackGlider chart
NE	up
SE	forward
SW	down
NW	back

Later embeddings may curve and texture this chart. They do not redefine the Moore neighbourhood. Cells that look close after a fold do not become Conway neighbours; cells stretched apart do not cease to be neighbours.

Turns

There are two deliberately different events:

• A frame manoeuvre changes how the same Conway worldline is experienced. The world, not only the aircraft, transforms consistently; mission outcome cannot change.

• A Conway turn changes heading relative to the canonical substrate. It must be found in the raw grid as a real B3/S23 reaction. The foundation uses Mike Playle’s stable Snark reflector to demonstrate one such 90-degree turn.

Ailerons, elevons, banking and local curvature may express a detected Conway turn. They may never cause one by assigning a heading or moving five cells.

Repository status

This is an RSR-derived repository in the Metadatastician estate, minted from the canonical local rsr-template-repo on 2026-08-01. The foundation is green; the mission, production renderer, control semantics and playable level remain future work. No release or playability claim is made yet.

Its primary estate clade is fv — Formal Verification & Proofs. That is a value-proposition decision: the project’s defining work is establishing and mechanically defending the equivalence between claimed flight events and an uncompromised Conway history. The interactive experience is downstream of that proof-bearing contract.

AI-Assisted Installation

AI assistance is optional and confers no authority to weaken the mathematical contract. Humans and agents use the same local golden path: just test && just quality. just test checks the Rust evidence, the Zig FFI tests, the shipped Idris2 ABI seam, and every gated module across all four provers. An assisting agent must read 0-AI-MANIFEST.a2ml, the machine-readable identity and policy files, MATHEMATICAL-CONTRACT.md, VERIFICATION.md, and DEBT.md before changing the project. It must not upload code or local context to an external service without the maintainer’s informed choice.

The complete protocol and privacy boundary are in the AI-assisted installation guide.

Licence

Code, configuration and scripts are MPL-2.0. Prose documentation is CC-BY-SA-4.0. Per-file SPDX headers are authoritative; licence texts live in LICENSES/.