beanapologist/mu-ov-cipher

μ-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 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

Links

• Eigenverse — 606+ Lean 4 theorems
• OilVinegar.lean — 28 OV meta-theorems
• Morphisms.lean — S, F, T composition maps
• Interactive demo

License

MIT