Formal evidence
The formal-evidence review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.
Geometry · formal theorem
Napoleon’s Theorem — Algebraic Core
Given three complex points and ω² − ω + 1 = 0, the centroids of consistently oriented equilateral constructions on their sides form an equilateral triple.
Scope: Given three complex points and a number ω satisfying ω² − ω + 1 = 0, the centroids of consistently oriented equilateral constructions on their sides form an equilateral triple.
Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formal theorem
Exact formal proposition
Hypotheses and conclusion
This is the meaningful proposition proved by the checked wrapper declaration. It is extracted from the same commit-pinned Lean source.
noncomputable def NapoleonTheoremStatement : Prop :=
∀ ω a b c : ℂ,
IsSixtyDegreeRotationParameter ω →
let ab := orientedEquilateralApex ω a b
let bc := orientedEquilateralApex ω b c
let ca := orientedEquilateralApex ω c a
let cab := centroid a b ab
let cbc := centroid b c bc
let cca := centroid c a ca
IsEquilateralBy (1 - ω) cab cbc ccaDefinitions used in this proposition
IsSixtyDegreeRotationParameter
def IsSixtyDegreeRotationParameter (ω : ℂ) : Prop :=
ω ^ 2 - ω + 1 = 0orientedEquilateralApex
def orientedEquilateralApex (ω a b : ℂ) : ℂ :=
a + ω * (b - a)centroid
noncomputable def centroid (a b c : ℂ) : ℂ :=
(a + b + c) / 3IsEquilateralBy
def IsEquilateralBy (ω x y z : ℂ) : Prop :=
z - x = ω * (y - x)Lean wrapper declaration
The checked endpoint names the proposition displayed above. This short declaration is useful for source identity, but the expanded proposition is the mathematical statement to read first.
theorem napoleonTheorem : NapoleonTheoremStatementThe theorem at a glance
Napoleon's theorem at a glance
Accessible transcript
ω² − ω + 1 = 0 and apex(a,b)=a+ω(b−a) ⇒ the three centroids form an equilateral triple
The same root ω of ω² − ω + 1 defines all three oriented side constructions. Expanding their centroids as affine expressions and reducing powers of ω proves that the three centroids form an equilateral triple. This is the common-orientation algebraic core, not every synthetic variant.
Read the complete poster transcript
COMPLEX GEOMETRY · ALGEBRAIC CORE
NAPOLEON’S THEOREM
THREE EQUILATERAL CONSTRUCTIONS CREATE A FOURTH
CHOOSE ONE ω WITH
ω² − ω + 1 = 0
ON EACH ORIENTED SIDE
apex(a,b) = a + ω(b − a)
A · B · C
TAKE THE THREE CENTROIDS
THEY FORM AN EQUILATERAL TRIPLE
encoded by 1 − ω
HOW THE PROOF MOVES
1 · USE ONE COMMON ORIENTATION
The same ω acts on all three sides.
2 · EXPAND THE THREE CENTROIDS
Each centroid is an affine expression in a, b, c, and ω.
3 · REDUCE THE ROTATION PARAMETER
ω² = ω − 1
4 · CLOSE THE CENTROID RELATION
The remaining complex identity is polynomial algebra.
EXACT SCOPE
The algebraic complex-plane core with one common orientation parameter.
It does not instantiate ω as eⁱπ⁄³ or claim every nearby synthetic variant.
Theorem schematic
Three side constructions, one centroid triangle
ω² − ω + 1 = 0 ⇒ the three constructed centroids satisfy an equilateral relation
Choose one common parameter ω satisfying ω² − ω + 1 = 0 and use it to construct an oriented equilateral apex on each side. The centroids of those three side constructions satisfy the corresponding equilateral relation.
Result boundary
What this theorem does—and does not—establish
Given three complex points and a number ω satisfying ω² − ω + 1 = 0, the centroids of consistently oriented equilateral constructions on their sides form an equilateral triple.
- This is the complex-algebra core of the theorem; it does not choose a particular sixth root such as exp(πi/3) or determine the external-versus-internal orientation of a Euclidean diagram.
- It does not by itself give the full classical geometric presentation of Napoleon’s theorem.
About these visual explanations
These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.
Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
Continue the mathematics
Open questions and extensions
The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.
What the source ZIP contains
The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.
Publication review
Review record
Publication reviews accepted
Lean checks the exact proof. Accepted review records cover evidence completeness, statement alignment, scope, and public wording; the visual review covers explanation only.
Statement alignment
The formal declaration was accepted against the named theorem and its exact variant.
Result boundary
The accepted boundary keeps nearby stronger or commonly confused claims out of scope.
Public wording
The public-wording review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.
Canonical source
The first-party source link is pinned to the checked package commit and exact Lean file.
Accepted result
A validated accepted-result record binds the four reviews to the checked formalization.