README.md

---
language:
  - en
license: mit
library_name: custom
tags:
  - formal-verification
  - lean4
  - eigenverse
  - coherence-function
  - uniqueness-theorem
  - oil-and-vinegar
  - post-quantum
  - GF-p
pipeline_tag: other
---

# μ-OV: Oil-and-Vinegar Structure of the Eigenverse

**28 machine-checked Lean 4 theorems formalizing the Eigenverse as an Oil-and-Vinegar partition with post-quantum hardness properties. Zero `sorry`.**

## What This Is

The [Eigenverse](https://github.com/beanapologist/Eigenverse) has the structure of an Oil-and-Vinegar (OV) partition. [`OilVinegar.lean`](https://github.com/beanapologist/Eigenverse/blob/main/formal-lean/OilVinegar.lean) formalizes this structure across 8 sections:

| Section | Theorems | What It Proves |
|---|---|---|
| §1 Vinegar Triple | 4 | V1 (energy), V2 (balance), V3 (coherence closure), consistency |
| §2 Oil Reduction | 3 | Vinegar uniquely determines all oil (z = μ, η, canonical scales) |
| §3 Trapdoor | 4 | C(r) is unique, symmetric, monotone, with unit maximum |
| §4 Composition | 3 | P = S∘F∘T well-defined via Morphisms §§1, 3, 6 |
| §5 Signature | 2 | μ is the unique valid signature (unforgeable) |
| §6 Lanchester | 2 | 183,315 cross-terms, quadratic growth |
| §7 Post-Quantum Modular | 5 | Trapdoor injectivity, max preservation, inversion balance, golden coherence hierarchy |
| §8 Quantum-Resilient Hardness | 5 | GF(p) boundedness, modular product rule, Grover hardness floor, modular energy conservation, PQ summary |

## The OV Partition

| OV Component | Eigenverse |
|---|---|
| **Vinegar** (freely chosen) | 3 pre-physical axioms: energy conservation (V1), directed balance (V2), coherence closure (V3) |
| **Oil** (determined by vinegar) | μ = e^(i·3π/4), all coherence evaluations, canonical scales |
| **Trapdoor** | C(r) = 2r/(1+r²) — injective on (0,1], symmetric under inversion, unique normal form |
| **Signature** | μ — the unique valid eigenvalue |
| **Verification** | `ov_signature_unique`: any z satisfying V1 ∧ V2 ∧ sector = μ |

## Post-Quantum Extensions (§7–§8, PR #19)

The new sections formalize properties needed for GF(p) deployment:

**§7 — Modular Extensions:**
- **`trapdoor_injective`**: C is injective on (0,1] — no ambiguity in trapdoor evaluation
- **`trapdoor_max_preservation`**: C(r) ≤ C(1) = 1 for all r > 0 — tight ceiling
- **`coherence_inversion_balance`**: C(r) + C(1/r) = 2·C(r) — key compression (2-element equivalence classes)
- **`coherence_extended_golden`**: C(φ) = 2φ/(φ+2) — third canonical scale
- **`coherence_golden_extended_hierarchy`**: C(δ_S) < C(φ) < C(1) — three-anchor trapdoor

**§8 — Quantum Resilience:**
- **`lanchester_modular_gfp`**: constraint count is well-defined in GF(p) for any prime p
- **`lanchester_modular_product`**: cross-terms computed efficiently via modular residues
- **`quantum_resilient_quadratic`**: Grover leaves super-linear residual: 2(n−1) ≤ n(n−1)
- **`modular_energy_conservation`**: V1 component bounds hold under GF(p) embedding
- **`post_quantum_ov_summary`**: three pillars (injectivity ∧ max preservation ∧ Grover floor)

## Honesty Note

The Lean theorems prove structural properties of the OV partition — uniqueness, injectivity, monotonicity, GF(p) well-definedness. These are **necessary** properties for a post-quantum cryptosystem but not **sufficient** alone. Full MQ-hardness is a separate cryptographic assumption. The Eigenverse provides the *structure*; the finite field and MQ assumption provide the *hardness*.

C(r) over ℝ has a closed-form inverse r = (1 ± √(1−y²))/y. The cryptographic hardness comes from embedding OV structure into multivariate quadratic systems over GF(p), not from C(r) being one-way.

## All 28 Theorems

### §1 — Vinegar Triple
| # | Theorem | Statement |
|---|---|---|
| 1 | `vinegar_V1` | μ.re² + μ.im² = 1 |
| 2 | `vinegar_V2` | −μ.re = μ.im |
| 3 | `vinegar_V3` | C(1 + 1/η) = η |
| 4 | `vinegar_triple_consistent` | V1 ∧ V2 ∧ V3 |

### §2 — Oil Reduction
| # | Theorem | Statement |
|---|---|---|
| 5 | `oil_reduction` | V1 ∧ V2 ∧ sector → z = μ |
| 6 | `oil_linear_collapse` | C(1+1/x)=x ∧ x>0 → x=η |
| 7 | `oil_coherence_triple` | C(1)=1 ∧ C(δ_S)=η ∧ C(φ²)=2/3 |

### §3 — Trapdoor
| # | Theorem | Statement |
|---|---|---|
| 8 | `trapdoor_at_one` | C(1) = 1 |
| 9 | `trapdoor_symmetry` | C(r) = C(1/r) |
| 10 | `trapdoor_monotone` | strict increase on (0,1] |
| 11 | `trapdoor_unique_normal_form` | a=2 uniquely |

### §4 — Composition
| # | Theorem | Statement |
|---|---|---|
| 12 | `composition_T_embedding` | reality(η,−η) = μ |
| 13 | `composition_F_at_unity` | C(\|μ\|) = 1 |
| 14 | `composition_public_map` | C(\|reality(η,−η)\|) = 1 |

### §5 — Signature
| # | Theorem | Statement |
|---|---|---|
| 15 | `ov_signature_unique` | sector ∧ balance ∧ energy → z=μ |
| 16 | `ov_canonical_signature_eval` | C(\|μ\|) = 1 |

### §6 — Lanchester
| # | Theorem | Statement |
|---|---|---|
| 17 | `lanchester_eigenverse_count` | 606·605/2 = 183315 |
| 18 | `lanchester_quadratic_growth` | n(n−1) ≤ n² |

### §7 — Post-Quantum Modular
| # | Theorem | Statement |
|---|---|---|
| 19 | `trapdoor_injective` | C injective on (0,1] |
| 20 | `trapdoor_max_preservation` | C(r) ≤ C(1) |
| 21 | `coherence_inversion_balance` | C(r)+C(1/r) = 2C(r) |
| 22 | `coherence_extended_golden` | C(φ) = 2φ/(φ+2) |
| 23 | `coherence_golden_extended_hierarchy` | C(δ_S) < C(φ) < C(1) |

### §8 — Quantum-Resilient Hardness
| # | Theorem | Statement |
|---|---|---|
| 24 | `lanchester_modular_gfp` | n(n−1)/2 mod p < p |
| 25 | `lanchester_modular_product` | modular product identity |
| 26 | `quantum_resilient_quadratic` | 2(n−1) ≤ n(n−1) |
| 27 | `modular_energy_conservation` | Re²≤1 ∧ Im²≤1 from V1 |
| 28 | `post_quantum_ov_summary` | injectivity ∧ max ∧ Grover floor |

## Links

- [Eigenverse](https://github.com/beanapologist/Eigenverse) — 606+ Lean 4 theorems
- [OilVinegar.lean](https://github.com/beanapologist/Eigenverse/blob/main/formal-lean/OilVinegar.lean) — 28 OV meta-theorems
- [Morphisms.lean](https://github.com/beanapologist/Eigenverse/blob/main/formal-lean/Morphisms.lean) — S, F, T composition maps
- [Interactive demo](https://huggingface.co/spaces/beanapologist/mu-ov-cipher)

## License

MIT