# OMEGA NAUGHT — Julia mathematical proof companion v0.1

This package recreates the mathematical arguments in the supplied Lean proof package as a **complete written proof with executable Julia certificates**. It indexes all **147 named source theorems**, retains their exact Lean declarations and hypotheses, and includes all **29 original archive files verbatim** in `reference/Lean/`.

The Julia computations use `BigInt`, exact rational enclosures, a small polynomial normalizer, and exhaustive finite checks. The universal real, calculus, linear-algebra, and induction arguments are written out in `src/ProofGuide.jl` and its readable export `PROOFS.md`. **This is not a second Lean-style kernel formalization.** A Julia `true` or successful run is not a proof object for an arbitrary quantified theorem. The distinction is recorded theorem by theorem.

## Run

Tested with the official **Julia 1.11.6** release. Only Julia standard libraries are used; no Julia package installation is required.

```bash
julia --startup-file=no --project=. run_proofs.jl
```

This writes a fresh certificate set under `evidence/fresh/` and exits nonzero if any configured check fails. Exact checks use explicit conditions that remain active at every optimization level.

To repeat the recorded unoptimized and optimized runs and compare their outputs:

```bash
julia --startup-file=no --project=. scripts/reproduce.jl
```

To see an exact geometric reconstruction from a ledger:

```bash
julia --startup-file=no --project=. examples/reconstruction.jl
```

## What the mathematics establishes

Fix the specified one-arcsecond circular seed, golden bilateral extension rules, positive geometric radius `a`, and the selected measurements: the average of the two outer straight lengths and the opposite semicircle length. Their values are

\[
G=a\varphi,\qquad C=a\pi,\qquad W=G+C=a(\varphi+\pi),
\quad \lambda=\frac{G}{W}=\frac{\varphi}{\varphi+\pi}.
\]

Translations and real linear isometric embeddings preserve these measurements. The selected weighted mean is `T(x)=1+lambda*(x-1)`. With `Q=339949771344778`, `S=10^15`, and `D={0,...,32767}`,

\[
\lfloor\lambda d\rfloor=F(d)=\left\lfloor\frac{Qd}{S}\right\rfloor
\qquad(d\in D).
\]

The entire floor table for an arbitrary real parameter `r` agrees with this table **if and only if**

\[
\frac{4196}{12343}\le r<\frac{7039}{20706}.
\]

Forward invariance extends the equality to every finite iteration depth. For an independently retained `h>0`, repeating `y -> h*floor(lambda*y/h)` on `y=h*d` produces `h*F^[n](d)`.

The terminal integer and forward-ordered Euclidean remainder list reconstruct the initial integer and its trajectory. Reverse-step admissibility characterizes the records of unique initial integers when the multiplier is nonzero and the divisor is positive. The exact source statements for weaker auxiliary domains, including zero and negative divisors, are preserved. Scale, center, and frame are additional inputs to geometric reconstruction.

The full argument and exact hypotheses appear in `PROOFS.md`, `THEOREM_GUIDE.md`, and the unchanged Lean source. The selected readout is part of the construction's specification; uniqueness among measurements of an unmarked outline is not assumed. `W` is a reference sum, distinct from the complete outline component length.

## Recorded execution results

Both final runs, `-O0` and `-O3`, exited **0**. All six generated certificate files were identical byte for byte.

| Check | Actual recorded result |
|---|---:|
| Source theorem declarations indexed and compared | 147 / 147 |
| Original hash-inventory entries verified | 28 / 28 |
| Exact polynomial reduction certificates | 97 zero residuals |
| Complete canonical state domain | 32,768 seeds |
| Complete 23-step ledger records reconstructed | 32,768 / 32,768 |
| Recorded transitions checked | 753,664 |
| Transitions beginning at a positive state | 300,871 |
| Absorbing-zero transitions | 452,793 |
| Minimum `S-rho(d)` | 34,535,026,732, attained at 20,706 |
| Maximum extinction depth | 10 |
| Mean extinction depth | `300871/32768` |
| Generic signed ledger cases | 60,390 |
| Proposed ledger records independently compared with encoding images | 22,680 |
| Separate BigFloat geometric illustrations | 31 scales |

The precision sweep covers `p=0:18`; it has 414 mismatches at six places, 39 at seven places, and zero from eight through eighteen. The proof that agreement holds exactly when `p>=8` for **all natural precisions** is the monotonicity argument in P08, not an infinite sweep. The modular inverse proof covers every seed below `S/2`; exhaustive enumeration is only claimed on `D`.

## Reading order and contents

| File or directory | Purpose |
|---|---|
| `PROOFS.md` | Complete mathematical arguments, P01–P13 |
| `THEOREM_GUIDE.md` | All 147 exact source declarations, individual proof steps, and evidence descriptions |
| `THEOREMS.toml` | Machine-readable theorem inventory checked against the source |
| `DEPENDENCIES.md` | Typed dependencies, hypotheses, and retained reconstruction data |
| `TRANSLATION.md` | Julia/Lean conventions and computational trust boundaries |
| `REPRODUCTION.md` | Actual environment, commands, statuses, and outstanding checks |
| `src/` | Executable exact arithmetic, polynomial certificates, ledgers, geometry, proofs, and verification |
| `evidence/O0/`, `evidence/O3/` | Fresh exact state, gap, enclosure, polynomial, precision, and result files |
| `evidence/O0.log`, `evidence/O3.log` | Actual final execution logs |
| `evidence/run_manifest.toml` | Actual commands, timestamps, statuses, and empirical elapsed times |
| `reference/Lean/` | Complete supplied Lean archive contents, unchanged; its evidence is archival |
| `SHA256SUMS` | Final package file inventory, excluding this inventory itself |

`scripts/export_guides.jl` regenerates both readable proof guides from the Julia proof strings and theorem inventory. `scripts/check_inventory.jl` verifies the final package hashes.

Frozen SRSD v1.0 remains an external scalar interface. This companion introduces no SRSD algorithm, extension, or merger. The statistics workbook, codec results, timing studies, older papers, and earlier Python execution histories are not recast as Julia mathematical proofs.