Van Aubel Extensions

This repository studies Van Aubel's theorem through complex structures on real vector spaces.

The central identity is affine-algebraic; its familiar equal-length and perpendicularity conclusions arise after an orthogonal inner-product structure is added.

Mathematical notes

The mathematical arguments are presented in three notes:

• Van Aubel as a Complex-Structure Identity;
• Edge-Operator Realizations and Rigidity of the Van Aubel Center Identity;
• Complex-Affine Naturality and Transfer of the Van Aubel Center Construction.

Note

This is an evolving research project. Its statements and exposition may be refined as related results are checked and organized.

Tip

If you notice any issues or have any suggestions and have the time,
please leave them in the Issues section. Thank you.

I would like to express my sincere gratitude to GPT for cross-checking my mathematical derivations, helping organize them, structuring the mathematical arguments, and developing the Lean files.

The central identity

Let $V$ be a real vector space, and let $J \colon V \to V$ be a linear map satisfying:

$$ J^2 = -I. $$

Choose one sign $\varepsilon \in {-1,+1}$, and for a directed edge $XY$ define:

$$ M_{XY} = X + \frac{(Y-X)+\varepsilon J(Y-X)}{2}. $$

Given four ordered points $A,B,C,D$, put:

$$ P=M_{AB}, \qquad Q=M_{BC}, \qquad R=M_{CD}, \qquad S=M_{DA}. $$

Then:

$$ R-P=\varepsilon J(S-Q). $$

This identity is affine-algebraic and needs only $J^2=-I$.

If $V$ is an inner-product space and $J$ is orthogonal, it gives the metric conclusions:

$$ {\lVert R-P\rVert}=\lVert S-Q\rVert, \qquad \langle R-P,S-Q\rangle=0. $$

Thus the two segments joining opposite centers have equal length and perpendicular directions.

In an oriented Euclidean plane, this specializes to the classical Van Aubel theorem.

Scope and results

The mathematical development considers:

• arbitrary ordered quadruples, including coincident, collinear, degenerate, and non-coplanar configurations
• vector-space and affine-space versions of the center identity
• the square construction and its metric consequences for orthogonal complex structures
• the classical oriented two-dimensional theorem
• the $J$-parallelogram formed by the side midpoints of the four centers, which becomes a square in the orthogonal setting
• existence of orthogonal complex structures exactly in even-dimensional finite-dimensional real inner-product spaces
• a transfer theorem for complex-affine coefficient identities
• rigidity when independently chosen edge operators are orthogonal
• rigidity of independently chosen edge signs on a nonzero real vector space
• an explicit nonorthogonal exceptional family in real dimension $4$
• concrete higher-dimensional behavior, including perpendicular but disjoint affine lines

For the central identity, the same operator $J$ and the same sign $\varepsilon$ are used on all four directed edges.

Orthogonality is required only for the equal-length and perpendicularity conclusions, not for the algebraic identity itself.

Verification and supporting materials

The papers contain the mathematical derivations. The Lean development and the numerical program are supporting checks of those derivations.

Lean checks

The Lean development provides machine-checked counterparts of the following non-categorical results:

• the central identity
• the intrinsic affine and vector-coordinate edge-operator classifications
• sign, orthogonal, and real-dimension-two rigidity
• pairwise-distinct nonorthogonal exceptional families in every complex dimension at least two
• complex-affine naturality of centers and identities, including degenerate edge configurations
• metric transport and isometry criteria
• recursive complex-affine term normal forms and universal transfer
• counterexamples separating algebraic transport from metric preservation

The category-theory formulation in the third note is expository and is not included in the Lean development.

The project is pinned to Lean v4.33.1 and mathlib v4.33.1.

Install elan, then build from the Lean project directory:

cd lean
lake build

The umbrella module provides a single import path:

import VanAubelExtensions

#check VanAubelExtensions.vanAubelIdentity
#check VanAubelExtensions.affineVanAubelIdentity
#check VanAubelExtensions.vanAubelTheorem
#check VanAubelExtensions.nonempty_orthogonalComplexStructure_iff_even
#check VanAubelExtensions.complexCoefficientIdentity_transfer
#check VanAubelExtensions.affineUniversalOperatorIdentity_iff_parametrized
#check VanAubelExtensions.universalOperatorIdentity_rigidity_of_finrank_two
#check VanAubelExtensions.ComplexAffineTerm.evalAffine_transfer_from_affineComplexLine
#check VanAubelExtensions.exceptional_family_in_every_complex_dimension_ge_two

The current development builds without sorry, admit, or project-defined axioms.

Module guide

Module	Contents
Basic	Orthogonal complex structures and their elementary properties
CenterIdentity	Linear and affine center constructions and the central identity
SquareGeometry	Edge configurations, their square properties under orthogonal signed hypotheses, naturality and degeneration, target metric re-realization, isometry criteria, and the planar theorem
Dimension	Standard even-dimensional structures and the dimension characterization
Rigidity	Intrinsic affine and vector four-operator parametrizations, complex-structure classification, sign and orthogonal rigidity, and sharp dimension-two rigidity
MidpointSquare	The derived midpoint $J$-parallelogram and its metric square consequences
ComplexAffineTransfer	Complex scalar action, center and identity naturality, recursive affine-term syntax and normal forms, coefficient uniqueness, and universal transfer
Examples	Incidence and metric counterexamples, the pairwise-distinct ℂ² exceptional family, and its extension to every complex dimension at least two

lean/VanAubelExtensions.lean imports all of these modules and is the recommended entry point.

Numerical consistency checks

The NumPy verifier tests both signs, several even dimensions, randomly conjugated orthogonal complex structures, and explicit degenerate configurations.

It checks the vector identity, equality of norms, and orthogonality. Deterministic boundary tests also cover invalid inputs and expected failures for nonorthogonal structures and mixed edge signs.

python3 -m venv venv
source venv/bin/activate
python -m pip install --requirement verify/requirements.txt
python -m unittest discover --start-directory verify --pattern "test_*.py"
python verify/verify_van_aubel.py

The dimensions, number of trials, seed, and tolerance are configurable:

python verify/verify_van_aubel.py \
  --dimensions 2 4 8 \
  --trials 1000 \
  --seed 42 \
  --tolerance 1e-10

These calculations are supplementary diagnostics rather than proofs.

Interactive demonstration

Open simple_demo/van-aubel-multidimensional-lab.html in a browser.

The standalone page supports draggable planar configurations, both orientation signs, degenerate examples, and experiments in multiple even dimensions.

It does not load external scripts, fonts, stylesheets, or other remote resources.

The same HTML file is both the editable source and the directly distributable standalone page.

Citation

If you use this work, please cite mindofcharles and the project Van-Aubel-Extensions.

Machine-readable citation metadata, including the author ORCID, is available in CITATION.cff.

License

This repository has two licensed components:

• Lean 4 source code, executable scripts, the interactive demonstration, and project configuration are licensed under the Apache License 2.0;
• mathematical notes, research articles, and Markdown documentation are licensed under Creative Commons Attribution 4.0 International.

See LICENSE.txt and NOTICE.txt for the repository-level licensing notice.