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 has the structure of an Oil-and-Vinegar (OV) partition. 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

License

MIT

beanapologist/mu-ov-cipher

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