Four-Dimensional Space Series

Four-Dimensional Space (14): Plane State Space and Angle Problems (Part 1)

Relationship between two angles and plane positions with orientation information

Content Overview

Introduction

Let’s first look at a simple angle range problem in 3D:

Given that the angle between vectors A and B is $\alpha$, and the angle between vectors B and C is $\beta$, find the range of the angle $\gamma$ between A and C.

This problem is simple using the geometric method: vector angles correspond to side lengths of spherical triangles on the unit sphere. Since the sum of two sides is greater than the third side, and the difference of two sides is less than the third side, with equality when collinear, the range of $\gamma$ is the closed interval $[|\alpha-\beta|,|\alpha+\beta|]$.

Read More

Four-Dimensional World Series

Four-Dimensional World (12): Material Structure

Last time we explored the four-dimensional periodic law settings. This time let’s look at material structures and make some bold, groundless predictions about their properties (I’m not a chemistry major, so everyone is welcome to raise objections to any content).

Fictional organic compound structural formula drawn by 4D molecular browser
As I was continuing to write this section, netizen KWOK Chun shared with me an online Google document called “Symmetric 4D Chemistry”, where the four-dimensional chemistry periodic table setting is exactly the same as mine, only the element naming is different. When I was nearly finished writing this article, I also saw 4denthusiast’s Blog which specifically discusses four-dimensional chemistry and attempts quantitative computational analysis. They try to establish a more rigorous four-dimensional fundamental physics system starting from elementary particle physics, and I will share some wonderful content.

Featured Content

Read More

Four-Dimensional World Series

Four-Dimensional World (XI): The Periodic Table

This time we’ll look at the periodic law of elements in the microscopic theory of the four-dimensional world. The atomic structure in four dimensions has always been a troublesome matter: the inverse cube law of force decay leads to the non-existence of stationary atomic wave functions, and the scientific community agrees that atoms cannot exist in a four-dimensional world, nor can matter be formed, end of article. Besides directly accepting this cruel reality, we can actually assume there are four-dimensional atoms, but their quantum mechanical mechanisms must be completely different from three-dimensional theory.

Partial display of four-dimensional periodic table elements
To maintain similarity with our world as much as possible, if we temporarily ignore the inverse cube law of forces and assume that the distribution of wave functions in various directions on the hypersphere still satisfies wave dynamics, then we can still preserve the electron subshell structure of atoms, the periodic law of elements, and molecular structures. The shortcoming is that calculations involving overall energy such as ionization energy, reactivity, and spectra that need to consider the radial direction would be completely unpredictable. Therefore, the “scientific validity” of this article (including the entire four-dimensional world series) is greatly reduced, and is only for entertainment and providing ideas (for writing novels, etc.). Please don’t take it too seriously.

Table of Contents

Four-Dimensional Space Series

Four-Dimensional Space (Part 13): Hyperspherical Harmonics

// This article only discusses solutions to certain partial differential equations on hyperspheres and does not involve imaginary four-dimensional world physics settings, hence it is categorized in the Four-Dimensional Space series.

// Note: This article contains many formulas. Feel free to ignore the details and just appreciate the various wave functions.

Hyperspherical harmonics with 120/600-cell symmetry, image from Greg Egan's website
This time we’ll look at standing wave patterns on hyperspheres—what Hyperspherical Harmonics look like. They are solutions to the Laplace equation on hyperspheres and are related to possible wave function shapes of four-dimensional atoms (which I plan to explore in detail in the next article). They can also accelerate four-dimensional ray tracing rendering through “hyperspherical harmonic lighting” algorithms. Perhaps readers are already familiar with spherical harmonics on spheres and know that their expressions are somewhat complex. This article will try to avoid these complicated expressions and understand them from a new perspective.

Table of Contents

类型论与机器证明简介

《同伦类型论》书的扉页

上篇文章介绍了命题逻辑、一阶逻辑再到ZFC集合论，本文来看一种新的宣称想要取代集合论在数学中地位的新东西——类型论。事实上它已经广泛运用在机器证明当中，其中最著名的就是四色定理的证明了，同时它跟程序代码很类似。把类型论稍加改造成同伦类型论，它还能比集合论更加“直接”地处理拓扑学中的许多问题。

类型论的动机

“类型”这一概念广泛被用于编程语言中，具体来说用于编译前的类型检查，比如下面这段C语言代码

1
2
3
int i = 0;       // 定义整数变量i，并将其设为0
string j ="oma"; // 定义字符串变量j，并将其设为"oma"
int k = i * j;   // 定义整数变量k，并将其设为 i * j

编译时会报错，因为这段程序声明i是整数类型的变量，而j是字符串类型的变量，它们无法相乘，或者说，乘法运算是一个接受两个数作为输入参数，输出返回一个数的函数，这里输入的i、j的类型显然与之不匹配。从上面的例子可以看出，类型检查其实就是编译器帮助我们检查代码有没有明显的低级错误导致执行一些像把数字与字符串相乘的这种无意义的命令。虽然检查一个表达式的类型也是机械化的（可定义成形式系统），但这似乎跟数学逻辑没有一点关系，它居然能用来构建公理化体系？yugu233做过一期视频《论码农与数学家的相似性【数学地图】》非常通俗形象地解释了类型跟证明之间的联系。

Read More

Introduction to Axiomatic Set Theory

// Note: This article is merely a rough summary of the author’s recent study of set theory. If you want to delve deeper, I strongly recommend finding a mathematical logic textbook for systematic study. Wikipedia is also good.

As we all know, what distinguishes mathematics from other disciplines most importantly is rigor. For example, the previous article introduced ordinals and cardinals that transcend infinity, where the slightest carelessness can easily lead to errors. As mathematical theories and proof processes become increasingly complex, mathematicians urgently need a system that can mechanically standardize proofs, making it convenient for machines to verify them. Before the invention of computers, someone proposed it—the formal system. This article will start with simple formal systems, introducing propositional logic, first-order logic, Peano arithmetic, and finally ZFC set theory, the formal system that appears most frequently in mainstream mathematics.

With the goal of learning by doing, I slowly built a formal system simulator called “Deductrium“ that runs on web pages, which I later turned into a game. Proving "a → a" in Deductrium

Read More