Oriented Matroids of Coxeter Permutahedra (S4 & B3)

This repository contains a computational pipeline for calculating, classifying, and validating regions formed by certain oriented matroids of coxeter permutahedra. The project focuses specifically on the oriented matroids coming from S4 and B3 permutahedra.

The workflow integrates Julia (for efficient algebraic region computation) and Python/SageMath/Z3 (for symbolic validation and simplex classification).

🗂️ Repository Structure

The repository is divided into two primary case studies: S4 and B3.

S4 Files

• s4_polynomials.csv / julia_s4_polynomials.csv: CSV files containing the S4 polynomial definitions.
• S4_Regions.jl: A Julia script that reads the S4 polynomials, utilizes the HypersurfaceRegions package to compute the connected components (regions) of the hypersurface complements, and extracts their sign patterns.
• S4_sign_patterns.txt: The output text file generated by the Julia script, containing lists of + and - sign patterns for the computed S4 regions.
• S4_Region_Validation.ipynb: A Jupyter Notebook (utilizing SageMath) that validates the computed sign patterns by solving the corresponding inequality constraints over specific domains.
• S4_Simplices_Classification.ipynb: A Jupyter Notebook that computes which determinants have zeroes, which polynomials correspond to those determinants, which subsets of the polynomials have common zeroes, classifies intersections, and counts coplanar sets within simplices.

B3 Files

• b3_polynomials.csv / julia_b3_polynomials.csv: CSV file containing the B3 polynomial definitions.
• B3_Regions.jl: A Julia script that evaluates the B3 polynomials and computes their regions and sign patterns.
• B3_sign_patterns.txt: The output text file containing the sign patterns for the B3 regions.
• B3_Region_Validation.ipynb: A Jupyter Notebook (utilizing the Z3 Theorem Prover) that programmatically checks the satisfiability of the B3 sign patterns to validate their geometric existence.
• B3_Simplices_Classification.ipynb: A Jupyter Notebook that computes which determinants have zeroes, which polynomials correspond to those determinants, which subsets of the polynomials have common zeroes, classifies intersections, and counts coplanar sets within simplices.

⚙️ Prerequisites and Dependencies

To run the full pipeline, you will need the following installed:

Julia Environment:

• Julia (v1.6 or higher recommended)
• HypersurfaceRegions.jl

Python / SageMath Environment:

• SageMath (Version 10.2+ recommended)
• Jupyter Notebook or JupyterLab
• Z3 Theorem Prover (Python bindings: pip install z3-solver)
• Standard scientific Python libraries: numpy, scipy, ipywidgets, ast
• TQDM (Python bindings: pip install tqdm)

🚀 Workflow and Usage

Execute the pipeline in the following order:

1. Classify Simplices (Jupyter / Python) Start by opening S4_Simplices_Classification.ipynb / B3_Simplices_Classification.ipynb to run intersection analyses. This will find which polynomials contain a zero in the fundamental chamber and find common roots among subsets of polynomials.

2. Compute Regions and Sign Patterns (Julia) Next, run the Julia scripts to parse the polynomials and generate the sign patterns for the regions.

   julia S4_Regions.jl
   julia B3_Regions.jl

   This will read the respective .csv files and overwrite/generate S4_sign_patterns.txt and B3_sign_patterns.txt.

3. Validate Regions (Jupyter / Python) Finally, open the validation notebooks to check the satisfiability of the generated sign patterns.

   • S4: Open S4_Region_Validation.ipynb using a SageMath kernel. It evaluates the patterns against structural constraints to filter out valid open patterns.
   • B3: Open B3_Region_Validation.ipynb. Replace the two "REPLACE THIS" with the polynomials from julia_b3_polynomials.csv substituting ^ with **. Due to the larger computations involved, this relies heavily on the z3 SAT solver to verify combinations of polynomial inequalities and confirm their geometric existence.

📝 Notes

• Execution Times: Due to the number of polynomials and the degree of the hypersurfaces, the Z3 solver and SageMath root-finding algorithms may take significant time to evaluate strict inequalities. The B3 notebook includes batching and timeout handling (z3_worker.py) to manage heavy computations.
• Polynomial Syntax: Ensure that if you modify the .csv files, the polynomials remain in a format that can be parsed by Meta.parse in Julia and easily substituted into Python expressions.