Seven conics occupy seven vertices of a cube. Neighboring conics touch twice. On every completed square face, the four contact chords meet at a point. Can the eighth conic be recovered?
Penrose’s theorem says yes, with appropriate interpretations of degeneracies. The cube records compatibility: it is not a solid containing the conics. Click in the floating experiment. The new curve simultaneously meets three contact conditions. [1]
Click an edge of the miniature cube to isolate its two conics and their contact chord. Select a face to see its four chords. Drag the three hollow handles to move the initial chords.
1. An edge means double contact
For homogeneous quadratic forms, a convenient algebraic contact relation is
On the chord ℓ = 0, the conics have the same restriction up to scale. At a common smooth point, their differentials agree up to the same scale. When there are two distinct contact points, they therefore have the same tangent at each. This is stronger than simply sharing two tangent lines.
These qualifications matter. A quadratic identity does not by itself guarantee a nonzero conic, nonsingularity, or two real contact points. The demo reports degeneracy and real-contact diagnostics; its curves are numerical drawings, not proofs.
2. One symmetric matrix, eight conics
Start with q0, three linear forms p1, p2, p3, and a symmetric matrix M. For every subset S of {1,2,3}, set
Here MS is a principal submatrix. Adding one index is a Schur-complement operation: the change in q is a multiple of a square. Eliminating two indices in either order also puts all four contact chords in one pencil. This constructs a compatible cube. [1]
The sliders change M’s off-diagonal entries; the hollow handles change the constant terms of the three seed chords. The base conic is the unit circle. All eight curves are recomputed from the same parameters.
Clearing denominators gives the identity checked by the algebraic Lean module:
It is a polynomial identity over any commutative ring. Its geometric interpretation needs additional hypotheses. The parameter determinants DS and determinants of the conic matrices are different diagnostics.
3. Another cube: points and lines
Fomin–Pylyavskyy also have a seven-to-eight cube theorem, their Proposition 9.1. This time the vertices alternate between points and lines. Three coherent faces determine a missing line, and the remaining three faces are coherent. They identify this with Desargues’ theorem. [2]
. The seed lines form a triangle. The three additional points move along rays from a common point O to its vertices. Change their positions with the sliders, or drag O. Reveal the final line to see the three side-intersection points lie on it.
For a face (A, ℓ, B, m), the condition is that the join AB contains the meet ℓ ∩ m. Its mixed cross-ratio is
The four edge pairings must be nonzero: an edge in this cube means non-incidence. The actual incidence is encoded by the face. The blue construction lines in the picture are not edges of the tiled surface.
4. Why the surface closes the proof
Forget coordinates for a moment and place a nonzero scalar on each edge. A consistently oriented face uses two edge factors in its numerator and two in its denominator. Every physical edge is used once with each sign. Hence
If all but one face have rf = 1, the remaining face must too. This is the cancellation core of the master theorem. It works for any finite paired-edge certificate, not just a cube. The full geometric theorem combines it with the interpretation of coherence. [2]
. Begin with all six ratios equal to one. Perturb one edge: precisely two faces change, by reciprocal factors. Their total product stays one. These calculations use integer fractions, not floating-point tolerances.
The Lean certificate stores two bijections from face slots to physical edges. This records actual cancellation data, rather than assuming that the total product is one as an input axiom. The six-face cube has its own finite checked permutations.
5. The bridge retains the quadratic data
A conic equation has six homogeneous coefficients, so its projective class is a point of ℙ5. A line ℓ gives the special coefficient vector ν2(ℓ) representing its square. Thus
↓ in coefficient space
[q], [q′], [ν2(ℓ)] are collinear.
. The two curves vary, but their coefficient vectors stay in one linear pencil with a double-line vector. The readout shows all six coordinates; it is not a misleading two-dimensional picture of ℙ5.
The special point must remain on the Veronese surface of double lines. Removing that restriction changes the problem. The formal bridge checks evaluation of the square, its behavior under rescaling, its nonvanishing, and the coefficient-pencil identity.
6. What the formalization establishes
The independent Lake project lives alongside this page. Its root import includes every implemented module; Audit.lean prints the dependencies of every public theorem listed here. The browser never supplies evidence to Lean.
| Layer | Implemented scope |
|---|---|
| Penrose | Polynomial edge identities; one algebraic eighth expression; face-pencil identity; polarization. |
| Fomin–Pylyavskyy | General finite cancellation; forced last face; cube certificate; coordinate ratio/incidence equivalence. |
| Connection | Double-line coefficients; evaluation; rescaling and nonvanishing; linear-pencil interpretation. |
| Not yet implemented | Arbitrary-input normalization; complete projective contact theory; geometric completion and uniqueness; singular complete conics; a full comparison theorem. |
Browse the Lean project · Build and axiom audit · Recorded theorem dependencies · Development blueprint
cd apps/incidence-cubes/formal
lake exe cache get
lake build
lake env lean Audit.leanThe next substantial goal is a theorem taking geometric seven-conic data to the matrix normal form. Subsequent modules should handle projective equivalence, contact nondegeneracy and uniqueness without strengthening the hypotheses silently.
Sources and reproducibility
[1] R. Arnold, A. Chern, M. Eide, C. Gunn, T. Neukirchner, R. Penrose. Penrose’s eight-conic theorem, especially §§6–7. See also Chern’s project page.
[2] S. Fomin and P. Pylyavskyy. Incidences and tilings, Proposition 2.5, Theorem 2.6 and Proposition 9.1.
The mathematical engine has no external runtime dependencies. It is independently exercised by deterministic tests; their recorded results are separate from Lean evidence. The visual construction is intentionally a general-position family, not a sampler of every admissible configuration.
The useful common language is compatibility—not congruence of shapes.