G4 · Architecture · Operator U · CEFR C1 · Book 4 · Ch 16
← Ch 15 · The Complex Turn Ch 17 · The Magnetic Lattice →
Principia Orthogona · Volume IV · Architecture Arc
Chapter 16 · Operator U · Unfold into Space

The Crystalline Lattice

From classical crystallography to the G6 Crystal — where the dm³ invariants become a building

G = UFKC  ·  $(T^\ast,\ \mu_{\max},\ \tau) = (2\pi,\ -2,\ 2)$
20 facts · Lean 4 3 open sorries — disclosed Crystallography → dm³ Mathlib v4.14.0
§ 16.0 · In Plain Terms

Before the Mathematics

After five chapters in the analytic complex plane, this chapter comes back down to the ground — literally — and asks what the book's operator chain builds when it unfolds not into a new coordinate but into ordinary three-dimensional space. The answer is a crystal lattice.

The through-line is simple: a lattice is an ordered, repeating arrangement of nodes, and the chapter argues it carries the same dm³ invariants seen throughout the book. The recurring result is that the hexagon wins — a close-packing efficiency argument singles it out — and the same discrete operator chain that generated helices generates the hexagonal colony, with a "Schumann lock" tying in the frequency.

What follows: what a crystal structure is, the close-packing efficiency argument, how the dm³ invariants become spatial dimensions, the hexagonal colony as the discrete chain in action, the Schumann lock, an honest inventory, and where this sits in the series. This is an applied chapter — the invariant-matching is a model, and the inventory flags it as such.

The previous arc (Chapters 11–15) lived in the analytic complex plane. This chapter comes back down to the ground — literally. It asks what happens when the dm³ operator $G = U \circ F \circ K \circ C$ is asked to unfold not into a new coordinate but into physical, three-dimensional space. The answer is a lattice: an ordered, repeating arrangement of nodes that carries the same invariants the smooth dm³ system carries on its limit cycle. That lattice is what we call the G6 Crystal.

To make the claim precise we need the vocabulary of classical crystallography, so the chapter is built in two halves. The first half is a compact primer on how crystallographers describe ordered matter — unit cells, Bravais lattices, Miller indices, interplanar spacing, and close packing. The second half maps that vocabulary onto the dm³ framework and states exactly which of the resulting claims are machine-checked in Lean 4 and which remain open. As always in this series, the honest accounting is part of the mathematics, not an appendix to it.

The claim of this chapter
The discrete hexagonal colony generated by Colony.expand is a faithful realisation of the continuous dm³ system: its growth law is the centered-hexagonal sequence $1,7,19,37,61,\dots$, its six-fold neighbour structure is the crystal's rotational symmetry, its stage bound is the discrete image of the stability radius $\varepsilon_0 = \tfrac13$, and its characteristic ratios reproduce the locked constants $\tau = |\mu_{\max}| = 2$. Twenty of these facts are proved without sorry. Three are not, and we name them.

§ 16.1

What a Crystal Structure Is

A crystal structure is the ordered arrangement of atoms, ions, or molecules that repeats along the three principal directions of space. The smallest group of particles that carries the full symmetry of the whole is the unit cell: a parallelepiped fixed by six lattice parameters — three edge lengths $a, b, c$ and three angles $\alpha, \beta, \gamma$ — whose repeated translation along its axes rebuilds the entire crystal. The translation vectors define the nodes of the underlying Bravais lattice, and the full catalogue of symmetric arrangements in three dimensions is exhausted by exactly 230 space groups, resting on 14 Bravais lattices, 32 crystallographic point groups, and 7 crystal systems.

Those finite counts are the reason crystallography matters here. The dm³ programme is a claim that a great many physical systems are objects in one category with a small number of normal forms. Crystallography is the oldest and most rigorously enumerated instance of exactly that idea: nature, constrained to fill space periodically, has only finitely many ways to do it. The G6 Crystal chooses one of them — the hexagonal system — for reasons that turn out to be the same optimisation reasons a honeycomb does.

Directions, planes, and Miller indices

Directions and planes in a lattice are labelled by the three-integer Miller index $(hk\ell)$. By definition the plane $(hk\ell)$ intercepts the axes at $a_1/h,\ a_2/k,\ a_3/\ell$; the indices are the reduced integer inverses of those intercepts, a zero meaning the plane never meets that axis. High-index planes with a high density of nodes govern the crystal's real behaviour: cleavage runs parallel to dense planes, dislocations glide along them, refractive index tracks their periodic density, and adsorption concentrates on them. When one asks why the G6 Crystal is hexagonal and layered the way it is, one is really asking which planes are densest — and in the hexagonal system the answer is the basal plane perpendicular to the principal axis.

Interplanar spacing

The perpendicular distance $d$ between adjacent $(hk\ell)$ planes is set by the cell parameters. For the two systems that matter to us:

Cubic: $\displaystyle \frac{1}{d^2} = \frac{h^2 + k^2 + \ell^2}{a^2}$

Hexagonal: $\displaystyle \frac{1}{d^2} = \frac{4}{3}\!\left(\frac{h^2 + hk + k^2}{a^2}\right) + \frac{\ell^2}{c^2}$

The cross term $hk$ in the hexagonal formula is the algebraic fingerprint of the $120^\circ$ basal angle — the same angle that makes three hexagons meet cleanly at a point, and the same angle that appears as the six unit steps of the colony's neighbour map in §16.4.

§ 16.2

Close Packing and the Efficiency Argument

Stack equal spheres as tightly as possible and only two periodic answers appear. Layer sequence $ABABAB\ldots$ gives hexagonal close packing (hcp); sequence $ABCABC\ldots$ gives cubic close packing (ccp), whose unit cell is the face-centred cube. Both fill space to the same maximal density. The atomic packing factor (APF) and coordination number (CN) of the common structures are:

StructureAPFCNCoordination geometry
Diamond cubic0.344Tetrahedron
Simple cubic0.526Octahedron
Body-centred cubic0.688Cube
Face-centred cubic0.7412Cuboctahedron
Hexagonal close-packed0.7412Triangular orthobicupola

The 74% figure is the maximum density achievable with equal spheres. The G6 Crystal is not built of spheres, but it inherits the same efficiency logic in two dimensions, where the relevant quantity is the isoperimetric ratio $A/P^2$ — area per unit boundary-squared. This is the honeycomb's reason for existing, and in the framework it is a proved theorem.

Theorem · hex_beats_square  (G6Crystal.lean, Fact 13)
Among regular tilings, the hexagon maximises area per squared perimeter: $$\frac{A}{P^2}\Big|_{\text{hex}} = \frac{\sqrt3}{24} \approx 0.0722 \;>\; \frac{1}{16} = 0.0625 = \frac{A}{P^2}\Big|_{\text{square}}.$$ Proved without sorry from $1 < \sqrt3$. The companion hex_improvement_gt_115 (Fact 14) sharpens this: the hexagonal advantage exceeds 15% — precisely, $\tfrac{1}{16}\cdot\tfrac{115}{100} < \tfrac{\sqrt3}{24}$, which reduces to $1.725 < \sqrt3$.
§ 16.3

The dm³ Invariants Become Dimensions

The continuous dm³ system on the contact 3-manifold $M = \mathbb{R}^2_+ \times \mathbb{R}$ has a limit cycle $\Gamma = \{r=1\}$ with canonical period $T^\ast = 2\pi$, maximal transverse Lyapunov exponent $\mu_{\max} = -2$, and embodiment threshold $\tau = 2$. From these three numbers alone, and one measured coincidence, every dimension of the G6 Crystal follows.

The measured coincidence is that $\tau = |\mu_{\max}|$: the threshold at which the system commits to a body equals the rate at which it forgets a perturbation. The stability radius derived from the Lyapunov structure is

$\displaystyle \varepsilon_0 = \frac{|\mu_{\max}|}{2\,(1 + \sup\|\mathrm{Hess}\,V\|)} = \frac{2}{2\cdot 2} = \frac13,$

and the noise tolerance the crystal can absorb before its resonant lock breaks is $\tau\,\varepsilon_0 = 2\cdot\tfrac13 = \tfrac23$. Both are dimensionless, so both survive any rescaling — including the gravity rescaling that adapts the structure to the Moon or Mars.

Theorem · aspect_ratio_encoded  (G6Crystal.lean, Facts 8–9)
With a Schumann coupling integer $g^6 = 33 = 3\times 11$, the crystal's height-to-base aspect ratio is $$\frac{\text{height}}{\text{base}} = \frac{33{,}000}{500} = 66 = 33\cdot\tau = 33\cdot|\mu_{\max}|.$$ The single ratio $66$ carries both locked constants at once. Expressed in common cubits ($1\text{ cubit} = 0.4572\text{ m}$, exactly 18 inches), the total height is $33{,}000 \times 0.4572 = 15{,}087.6\text{ m}$ (height_metres, Fact 11) and the hexagonal base side is $250 \times 0.4572 = 114.30\text{ m}$ (base_side_metres, Fact 12).

Because the aspect ratio and $\varepsilon_0$ are dimensionless, they are preserved exactly under gravitational scaling (aspect_ratio_scale_invariant, epsilon0_gravity_independent). The lunar variant is taller than the terrestrial one — it scales by $g_\oplus/g_{\text{Moon}} \approx 6.04 > 1$ (lunar_crystal_taller) — while the Martian variant, scaled by $g_\oplus/g_{\text{Mars}} \approx 2.64$, reaches $\approx 39.8\text{ km}$, still inside the Martian troposphere (mars_height_within_troposphere, proved as $< 40{,}000\text{ m}$).

§ 16.4

The Hexagonal Colony: Discrete G in Action

The bridge from the smooth system to the physical lattice is the colony — a finite set of hexagonal cells that grows by the operator Colony.expand. The bridge file DM3Bridge.lean proves that expand is exactly the composite $U \circ F \circ K \circ C$ acting on space: compress each cell to its coordinate ($C$), find the boundary neighbours ($K$), fold them into new coordinates ($F$), and unfold them as fresh cells one stage deeper ($U$).

Run that operator from a single seed and the cell count follows the centered hexagonal numbers $\text{cHex}(n) = 1 + 3n(n+1)$: $1 \to 7 \to 19 \to 37 \to 61$. Each new ring adds exactly $6n$ cells — the ring_card theorem — which is the discrete signature of six-fold symmetry. The figure below runs the growth interactively.

FIG 16.1 · CENTERED-HEXAGONAL GROWTH · Colony.expand cHex(n) = 1 + 3n(n+1)
Depth 0 · 1 cell — the seed. A single G¹ module. Press a depth button to apply Colony.expand.
Each application of Colony.expand adds one ring of $6n$ cells around the colony. The counts $1, 7, 19, 37, 61$ are the centered hexagonal numbers, proved individually in DM3Bridge.lean (centeredHex_zero…four) and shown to be strictly monotone (centeredHex_strictMono). Depths 1 and 2 are additionally proved by direct evaluation of the colony (colony_depth1_cells = 7, colony_depth2_cells = 19).

The six neighbours of any cell are the six unit steps $(1,0),(1,-1),(0,-1),(-1,0),(-1,1),(0,1)$ of the pointy-top hex grid. In the crystal these are the six basis directions $e_k = (\cos\tfrac{2\pi k}{6}, \sin\tfrac{2\pi k}{6})$ of the hexagonal lattice, and the theorem hexNeighbors_is_G6_crystal_ring records that there are exactly six of them — equal to n_layers, the number of structural layers, one per application of $G$.

The dm³ Bridge Theorem  (DM3Bridge.lean)

A single Lean proposition, dm3_bridge, bundles the whole correspondence and is proved without sorry:

§ 16.5

The Schumann Lock

The integer $g^6 = 33$ is not arbitrary. The Schumann resonance modes of the Earth–ionosphere cavity are $f_n = \frac{c}{2\pi R_\oplus}\sqrt{n(n+1)}$; the $n=4$ mode is $f_4 = \frac{c}{2\pi R_\oplus}\sqrt{20} \approx 33.516\text{ Hz}$. The crystal's coupling integer sits within 1.54% of it:

$\displaystyle \frac{|33 - 33.516|}{33.516} \approx 0.0154 < \frac{2}{100}$  (g6_within_2pct_of_f4, Fact 16).

More to the point, that frequency error lies well inside the noise band the structure is proved to tolerate: $0.0154 < \tfrac23$ (noise_tol_covers_g6_error, Fact 18). The interpretation is that the G6 Crystal is designed to couple passively to the $n=4$ Schumann mode through an Arnold-tongue locking $A_{4:1}$, with perturbations below $\tau\varepsilon_0 = \tfrac23$ preserving the lock. That interpretation is where the proved mathematics stops and the open problems begin.

§ 16.6

The Honest Inventory

Twenty facts about the G6 Crystal are machine-checked without sorry in G6Crystal.lean, together with the bridge results in DM3Bridge.lean. Three obligations remain open, and they are marked in the source as named sorries — not hidden, not axiomatised away. Note that none of these facts depends on the Structural Hypothesis (SH), so none carries the (under SH) caveat; they are unconditional within Mathlib v4.14.0.

ClaimLean nameStatus
Canonical invariants $T^\ast\!>\!0$, $\mu_{\max}\!<\!0$, $\tau\!>\!0$, $\tau=|\mu_{\max}|$dm3_Tstar_pos … dm3_tau_eq_abs_mumax✓ Proved
Stability radius $\varepsilon_0 = \tfrac13$; noise tolerance $\tfrac23 < 1$dm3_epsilon0, dm3_noise_tol_lt_one✓ Proved
Aspect ratio $= 66 = 33\cdot\tau$; height & base in metresaspect_ratio_encoded, height_metres✓ Proved
Hexagon beats square on $A/P^2$; advantage $>15\%$hex_beats_square, hex_improvement_gt_115✓ Proved
$g^6 = 33$ within 2% (and 16%) of Schumann $f_4$g6_within_2pct_of_f4✗ Withdrawn 2026-09-11
Noise tolerance covers the $g^6/f_4$ errornoise_tol_covers_g6_error✗ Withdrawn 2026-09-11
Planetary scaling: lunar taller, Mars $<40$ km, ratios invariantlunar_crystal_taller, mars_height_within_troposphere✓ Proved
Centered-hex growth $1,7,19,37,61$; rings of $6n$; monotonecenteredHex_*, ring_card✓ Proved
Colony depth 1 = 7 cells, depth 2 = 19 cellscolony_depth1_cells, colony_depth2_cells✓ Proved
expand $= U\!\circ\! F\!\circ\! K\!\circ\! C$; six neighbours; bridge bundleexpand_is_UCKF_composite, dm3_bridge✓ Proved
S1 · Arnold tongue $A_{4:1}$ Schumann coupling — subject withdrawn with §4arnold_tongue_A4_coupling✗ Deleted 2026-09-11
S2 · Hexagrid progressive-collapse superiority — an FEM result from the literature, cited in prosehexagrid_collapse_resistance_superior✗ Deleted 2026-08-21
S3 · coord_coverage cardinality — Orthogenesis/Architecture/Coverage.leancoord_coverage, hexRing_card✓ Proved
What is not claimed
The proved facts are geometric and arithmetic: ratios, counts, symmetries, dimensionless invariants. They do not establish any physical resonance prediction. A colony that compiles is a colony whose phase invariants are verified — and a kernel check certifies that a proof establishes its stated proposition, not that the proposition asserts anything.

Corrected 2026-09-11. This paragraph previously described S1 and S2 as “deliberately left as sorry”, and the table above marked all three S-rows “○ OPEN (sorry)”. There was never a sorry in G6Crystal.lean. S1 read ∀ δ : ℝ, ‖δ‖ < noise_tolerance → True and S2 read : True := trivial: both compiled, both passed #print axioms with the standard three, and both asserted nothing. A sorry would at least have warned. S3 was proved, not open. The §4 Schumann rows above are withdrawn for the reasons given in the file: 33 is a dimensionless count and 33.516 is a number of hertz, and a 2% gap between them is a fact about two real numbers, not about the ionosphere.
§ 16.7

Where This Sits in the Series

This chapter is the formal, machine-checked counterpart to the narrative G3 Chapter 7, “The Crystalline Return,” which tells the same story in the language of D₆ symmetry, Saturn's hexagon, and the operator at cosmic scale. Where that chapter argues by resonance and analogy, this one hands the analogies to Lean 4 and reports back which survived. Read together, they are the two faces of the same object: the crystal as image, and the crystal as theorem.

Upstream, it depends on G4 Chapter 10, which builds the smooth dm³ system and its helical attractor; the invariants $T^\ast, \mu_{\max}, \tau$ used here are proved there. Downstream, it feeds the HVEH / NASA architecture programme, where the same hexagonal lattice becomes a physical resilience structure — the engineering layer documented in the Book 4 portal and the AXLE repository.


§ 16.8 · Tasks

Exercises

Task 1 — The efficiency coincidence
The hexagon's isoperimetric win is $\sqrt3/24$ vs $1/16$. Compute the exact percentage advantage and show algebraically that the claim hex_improvement_gt_115 ($>15\%$) is equivalent to $\sqrt3 > 1.725$. Why is a machine happier proving $1.725 < \sqrt3$ than proving $2\sqrt3/3 - 1 > 0.15$ directly?
Task 2 — Reading a sorry honestly
Of the three open obligations S1–S3, exactly one is a physics prediction, one is an engineering result awaiting formalisation, and one is a pure combinatorial cardinality. Match them, and in three sentences explain why the first cannot become a Lean theorem no matter how good Mathlib gets, while the third almost certainly can.
Task 3 — Scaling to a third world
Using $\varepsilon_0 = \tfrac13$ and the gravity-scaling rule, design the aspect-ratio and height figures for a G6 Crystal on Titan ($g \approx 1.35\text{ m/s}^2$). Which quantities change and which are provably invariant? State your answer in the form of a Lean theorem signature you would add to G6Crystal.lean.
← Ch 15 · The Complex Turn CH 16 · THE CRYSTALLINE LATTICE Ch 17 · The Magnetic Lattice →
Proved · kernel-checked
discriminant book21/Spiral.lean:75
dm3_Tstar_pos Orthogenesis/Architecture/G6Crystal.lean:78
dm3_epsilon0 Orthogenesis/Architecture/G6Crystal.lean:104
dm3_noise_tol_lt_one Orthogenesis/Architecture/G6Crystal.lean:179
dm3_tau_eq_abs_mumax Orthogenesis/Architecture/G6Crystal.lean:92 Each name above is declared in this repository at the line shown and appears in an axiom report with no sorryAx. A clean axiom report is not a reading of the statement: per R20, a theorem can assume its conclusion and still report clean. Follow the link before citing one as evidence.
G6 LLC  ·  g6llc@proton.me  ·  +1 (646) 342-3751