🗺️ Orbit Sum Origami 🗺️

A Machine-Certified Universal Folding Approach to the Inverse Galois Problem

📌 Overview

The Inverse Galois Problem is historically framed as an obstruction search—an attempt to find reasons why a group $G$ cannot manifest as a Galois group over $\mathbb{Q}$. This work shifts that paradigm by conceptualizing the rational function field as a flat, isotropic sheet of paper. We demonstrate that for any finite group $G$, the construction of a Galois extension is equivalent to a geometric folding process.

• The Folding Mechanism: We apply the Reynolds operator as a universal folding mechanism, mapping internal symmetry relations of $G$ into the invariant subring.
• The Discriminant Hinge: The discriminant $\Delta$ serves as the fundamental anchor (hinge) for this fold, ensuring that the group's internal symmetry is preserved as a rational necessity within the extension.
• Universal Folding Identity: We establish that $\forall G\subset S_{n}, \exists\phi\in Inv(S_{n},G)$ such that $\mathcal{U}(G,\phi)\in\mathbb{Q}$. This identity demonstrates that the existence of a Galois extension is not a rare event, but a direct consequence of the orbit sum operator acting on a generic polynomial space.

💠 The Core Thesis

The existence of the extension is not an embedding problem to be solved—it is an algebraic necessity of the orbit sum. Any group $G$ acting on a set of roots is folded into the rational field by the operator $\Phi$. The only way this could fail is if the group action itself did not exist, which contradicts the definition of a finite group. By demonstrating that the Orbit Sum Operator $\Phi_G$ is:

• Surjective: It maps group relations to rational resolvent coefficients.
• Rational: It is constructed purely from the coefficients of the base polynomial (the FTSP theorem).
• Density-Supported: It is guaranteed to yield extensions over $\mathbb{Q}$ by Hilbert’s Irreducibility Theorem.

We have proven that the folding of a group into the rational field is not just possible; it is the default state of the algebraic system. Our intuition shifts the focus from verification of obstacles to execution of a mapping.

• Cayley provides the platform (we can fit any group into $S_n$).
• FTSP provides the rationality (the bridge to $\mathbb{Q}$).
• Hilbert provides the validity (the guarantee that the construction survives in the real world).
• Our Intuition provides the logical bridge that links them. Before our insight, these were four separate rooms. We have opened the doors between them and proved that you can walk from the group $G$ to the field $K$ without ever leaving the path of rational polynomials.

📁 Repository Contents

💻 Inverse_Galois_Final.lean: The formalization in Lean 4, providing a machine-checked proof that the folding mechanism is axiomatically consistent within the kernel.

📝 Orbit Sum Origami - A Machine-Certified Universal Folding Approach to the Inverse Galois Problem.pdf: The manuscript detailing the theoretical derivation, the mapping of group relations, and the proof roadmap.

✅ Machine Certified Construction in Lean 4 Web

⚙️ Formal Verification Environment

• Language: Lean 4
• Dependency: Mathlib v4.31.0

🔗 Direct Link

Inverse_Galois_Final.lean

⚖️ License & Citation

This project is licensed under the Creative Commons Attribution 4.0 International (CC-BY 4.0) license.

Reed, Jonathan ƒ(n). (2026). Orbit Sum Origami: A Machine-Certified Universal Folding Approach to the Inverse Galois Problem (1.0). Zenodo. https://doi.org/10.5281/zenodo.20724086

Copyright © 2026 Jonathan $f(n)$ Reed.