finish p7

lib.typ

@@ -44,4 +44,11 @@
 #let inprod(a,b) = {$angle.l #a,#b angle.r$}
 #let trig = sym.triangle.stroked.t
 
-#let mtext(body) = text(font: cnmainfont, weight: "regular", body)
+#let ii = {$upright(i)$}
+#let mtext(body) = text(font: cnmainfont, weight: "regular", body)
+
+#let thoerem_box(name, c) = {
+	identp
+	box(baseline: 4pt, inset: 4pt, fill: c, text(font: cnfont, fill: white, weight: "semibold", name))
+}
+#let lemma_icon = thoerem_box([引理], theme_blue)

main.typ

@@ -87,7 +87,7 @@ $ (-1),(1),(1),-1,(-1),(1),-1,-1 $
 
 #identp 如果 $a$ 存在一个 $-1$ 在一个 1 的后面，即存在下标 $i,j$ 满足 $i<j$ 且 $a_i=1,a_j=-1$，那么交换 $i,j$ 位置上的值后，得到一个新序列 $a'$，显然 $a'$ 中 1 的数量也为 $c$。
 
-#identp *引理* 进行上述变换后所有合法子区间的左端点的数量不降，即 $S(a)<= S(a')$ 一定成立。
+#lemma_icon 进行上述变换后所有合法子区间的左端点的数量不降，即 $S(a)<= S(a')$ 一定成立。
 
 #identp 假设上述引理成立，那么我们就只需要论证由 $n-c$ 个 $-1$ 开头，然后 $c$ 个 1 组成的序列 $b$ 满足 $S(b)<= 2c$，这是显然的。而对于任何其他序列，它们都可以通过有限次上述变换得到序列 $b$。
 
@@ -654,9 +654,9 @@ $ cases(c_1=1/2 (b_1 - sqrt(3) b_2),c_2=1/2 (sqrt(3) b_1+b_2)) #tab #mtext("或"
 
 #identp 在说明一般情况之前，我们首先要引入如下引理：
 
-#identp *引理* 一个横纵坐标均为整数的点绕着另一个横纵坐标均为整数的点旋转 $90 degree$ 后得到的点仍然是一个横纵坐标均为整数的点。（算出旋转后的点的坐标即可完成证明，读者自行验证该引理。）
+#lemma_icon 一个横纵坐标均为整数的点绕着另一个横纵坐标均为整数的点旋转 $90 degree$ 后得到的点仍然是一个横纵坐标均为整数的点。（算出旋转后的点的坐标即可完成证明，读者自行验证该引理。）
 
-#identp 下面说明一般情况，（反证法，无穷递降法）假设存在格点正 $k(k>=5)$ 边形。从所有的格点正 $k$ 边形中找出面积最小的一个，设它的顶点按逆时针顺序依次为 $P_1,dots,P_k$。对于每个顶点 $P_i$，把它绕点 $P_(i-1)$（特别地，点 $P_1$ 绕点 $P_k$）逆时针旋转 $90 deg$，得到点 $Q_i$（如图 @P7fig1）。
+#identp 下面说明一般情况，（反证法，无穷递降法）假设存在格点正 $k(k>=5)$ 边形。从所有的格点正 $k$ 边形中找出面积最小的一个，设它的顶点按逆时针顺序依次为 $P_1,dots,P_k$。对于每个顶点 $P_i$，把它绕点 $P_(i-1)$（特别地，点 $P_1$ 绕点 $P_k$）逆时针旋转 $90 deg$，得到点 $Q_i$（如@P7fig1）。
 
 #align(center, stack(dir: ltr, spacing: 5%,
 	[#figure(image(
@@ -670,7 +670,7 @@ $ cases(c_1=1/2 (b_1 - sqrt(3) b_2),c_2=1/2 (sqrt(3) b_1+b_2)) #tab #mtext("或"
 	), caption: [连接辅助线]) <P7fig2>]
 ))
 
-#identp 下面我们证明 $Q_1 dots.c Q_k $ 也是一个正 $k$ 边形（为了方便描述，我们给出 $Q_1 Q_2=Q_2 Q_3$ 的证明，其它的边之间的相等关系是同理可证的）。如图 @P7fig2，连接 $P_1 Q_1$、$P_1 Q_2$、$P_2 Q_2$、$P_2 Q_3$ 以及 $P_3 Q_3$ 五条线段。由于正多边的每个内角和每条边都相等，在 $trig P_1 P_2 Q_2$ 和 $trig P_2 P_3 Q_3$ 中，我们有
+#identp 下面我们证明 $Q_1 dots.c Q_k $ 也是一个正 $k$ 边形（为了方便描述，我们给出 $Q_1 Q_2=Q_2 Q_3$ 的证明，其它的边之间的相等关系是同理可证的）。如@P7fig2，连接 $P_1 Q_1$、$P_1 Q_2$、$P_2 Q_2$、$P_2 Q_3$ 以及 $P_3 Q_3$ 五条线段。由于正多边的每个内角和每条边都相等，在 $trig P_1 P_2 Q_2$ 和 $trig P_2 P_3 Q_3$ 中，我们有
 
 $ cases(P_1 P_2=P_2 P_3,angle P_1 P_2 Q_2=angle P_2 P_3 Q_3,P_2 Q_2=P_3 Q_3) $
 
@@ -691,16 +691,88 @@ $ cases(P_1 Q_2=P_2 Q_3,angle Q_2 P_1 Q_1=angle Q_3 P_2 Q_2,P_1 Q_1=P_2 Q_2) $
 $ S_(trig A B C)=1/2 abs(b_1 c_2 - b_2 c_1) $ <P7solBeq1>
 ]
 
-是一个有理数，而任意格点多边形都可以划分为若干个不相交的格点三角形。于是我们得出了这样一个引理：任意一个格点多边形的面积均为有理数。
+是一个有理数，而任意格点多边形都可以划分为若干个不相交的格点三角形。于是我们得出了这样一个引理：
 
-#identp 另一方面，我们知道正多边形的面积公式是
+#lemma_icon 任意一个格点多边形的面积均为有理数。
 
-$ S=(k a^2)/(4 tan pi/k) $
+#identp 另一方面，我们容易推导出正多边形的面积公式是
 
-其中 $k$ 表示该正多边形的边数，$a$ 表示正多边形的边长。若该正多边形至少有一条边的两个端点的横纵坐标均为整数，则 $a^2$ 一定是一个有理数，故正多边形的面积 $S$ 是有理数当且仅当 $tan pi/k$ 是有理数。
+$ S=(n a^2)/(4 tan pi/n) $
 
-#identp 由@P7solBeq1 我们知道，一个格点多边形的面积一定是一个有理数，因此我们只需说明“对于任意整数 $k>=3$，只有当 $k=4$ 时 $tan pi/k$ 才是有理数”，即可完成对原命题的论证。下面给出两个证明，其中第二个证明需要较多的代数知识。
+其中 $n$ 表示该正多边形的边数，$a$ 表示正多边形的边长。若该正多边形至少有一条边的两个端点的横纵坐标均为整数，则 $a^2$ 一定是一个有理数，故正多边形的面积 $S$ 是有理数当且仅当 $tan pi/n$ 是有理数。
 
-=== 证明 a
+#identp 由@P7solBeq1 我们知道，一个格点多边形的面积一定是一个有理数，因此我们只需说明“对于任意整数 $n>=3$，$n=4$ 当且仅当 $tan pi/n$ 是有理数”，即可完成对原命题的论证。这个命题可以很容易地使用抽象代数中关于“首一多项式”和“代数整数”的相关理论证明，下面则给出一个较为繁琐的初等方法。
 
-// TODO
+#identp 我们首先用反证法说明奇整数 $n>=5$ 时，$cos^2 pi/n$ 的值为无理数。假设 $n>=3$ 是某个奇整数，且 $cos^2 pi/n$ 的值为有理数，不妨设为 $p/q$，其中 $q>0$，且整数 $p,q$ 互质。于是
+
+#[
+#show: math_numbering
+$ cos pi/n=sqrt(p/q) #tab sin pi/n=sqrt(1-p/q) $ <P7solBabasic>
+]
+
+#identp 考虑对欧拉公式 $(cos pi/n+ii sin pi/n)^n=-1$ 使用二项式定理展开，得到
+
+#[
+#show: math_numbering
+$ sum_(k=0)^n binom(n,k) ii^k sin^k pi/n cos^(n-k)pi/n=-1 $ <P7solBaexpand>
+]
+
+取出@P7solBaexpand 两边的实数部分，并代入@P7solBabasic，得到
+
+#[
+#show: math_numbering
+$ sum_(k=0)^(floor(n\/2)) binom(n,2k)(-1)^k (1-p/q)^k (p/q)^(n/2-k)=-1 $ <P7solBareal>
+]
+
+我们知道 $q != 0$，于是我们可以在@P7solBareal 两边同时乘以 $sqrt(q^n p)$，这给出
+
+#[
+#show: math_numbering
+$ sum_(k=0)^(floor(n\/2)) binom(n,2k)(-1)^k (q-p)^k p^((n+1)/2-k)=-sqrt(q^n p) $ <PgirdsolBafinal>
+]
+
+#identp 当 $0<=k<=floor(n\/2)$ 时，由于我们假设 $n$ 为奇整数，故一定有 $(n+1)/2-k>=1$，同时 $binom(n,2k)$、$(-1)^k$ 与 $(q-p)^k$ 这三项一定均为整数，于是@PgirdsolBafinal 中左边的和式中的每一项都一定是 $p$ 的整数倍，于是 $sqrt(q^n p)$ 一定是 $p$ 的整数倍，也即 $gcd(p,q)=p$，又因为 $p,q$ 互质，于是一定有 $p=1$，也即 $cos^2 pi/n=1/q$。
+
+#identp 至此，我们论证了对于每个奇整数 $n>=3$，要么 $cos^2 pi/n$ 是无理数，要么存在正整数 $q$ 使得 $cos^2 pi/n=1/q$ 。对于每个 $n>=5$，一定有 
+
+$ 1>cos^2 pi/n>=cos^2 pi/5=1/16 (1+sqrt(5))^2>1/3 $
+
+于是不存在一个正整数 $q$ 使得 $cos^2 pi/n=1/q$。
+
+#identp 综上所述，对于每个奇整数 $n>=5$，一定有 $cos^2 pi/n$ 是无理数。更进一步地，有 $cos pi/n$ 也是无理数。
+
+#identp 对于一个整数 $n>=4$，我们可以把它写成 $n=p 2^k$ 的形式，其中 $p$ 是一个奇整数，$k$ 是一个自然数。下面我们对 $k$ 使用数学归纳法以证明“对于每个 $n>=4$ 均有 $cos pi/4$ 为无理数”。
+
+#identp 具体地说，用 $P(k)$ 表示关于自然数 $k$ 的命题模式“对于任意奇整数 $p$ 满足 $p 2^k>=4$，均有 $cos pi/(p 2^k)$ 是无理数”。显然 $P(0)$ 我们前面已经证明过的奇数情况，故 $P(0)$ 成立。
+
+#identp 现在假设 $P(k)$ 成立，目标是证明 $P(k+1)$ 也成立。根据余弦函数的倍角公式（也称“升幂/降幂公式”）$cos 2alpha=2cos^2alpha-1$，于是
+
+$ cos pi/n=2cos^2 pi/(2n)-1 $
+
+因此如果 $cos pi/n$ 是无理数，那么 $cos pi/(2n)$ 也是无理数。当 $p 2^k>=4$ 时，向这个结论代入 $n=p 2^(k+1)$：根据归纳假设有 $cos pi/(p 2^k)$ 是无理数，于是 $cos pi/(p 2^(k+1))$ 也是无理数。而当 $p 2^k<4$ 但是 $p 2^(k+1)>=4$ 时，显然 $p 2^(k+1)$ 的值只能为 4 或 6，并且容易发现
+
+$ cos pi/4 = sqrt(2)/2 #tab cos pi/6=sqrt(3)/2 $
+
+亦均为无理数，于是 $P(k+1)$ 成立。
+
+#identp 根据数学归纳原理，对于任意自然数 $k$，$P(k)$ 成立。也就是说，我们证明了对于任意的 $n>=4$，均有 $cos pi/n$ 为无理数。
+
+#identp 下面我们开始说明对于除了 1,2 和 4 之外的正整数 $n$，$tan pi/n$ 都是无理数。首先，根据正切函数的余弦方程（中文语境也称“万能公式”）$cos 2alpha=(1-tan^2 alpha)/(1+tan^2 alpha)$，有
+
+$ cos pi/n=(1-tan^2 pi\/2n)/(1+tan^2 pi\/2n) $
+
+因此对于每个偶整数 $n>=8$，均有 $tan pi/n$ 为无理数。
+
+#identp 另一方面，根据正切的余弦表达式 $tan^2 alpha=1\/cos^2 alpha-1$，有
+
+$ tan^2 pi/n=1/(cos^2 pi/n)-1 $
+
+而我们之前已经证明了当 $n>=5$ 是奇整数时，$cos^2 pi/n$ 是无理数，故对于任意奇整数 $n>=5$，$tan pi/n$ 都是无理数。
+
+#identp 最后，容易发现
+
+$ tan pi/3=sqrt(3) #tab tan pi/6=sqrt(3)/3 $
+
+亦均为无理数。
+
+#identp 综上所述，对于除了 1,2 和 4 之外的正整数 $n$，$tan pi/n$ 都是无理数。

template.typ

@@ -31,12 +31,23 @@
 	set ref(supplement: it => {
 		if it.func() == math.equation {
 			"式"
-		} else if it.func() == figure {
-			""
 		} else {
-			"Typset Error!"
+			auto
 		}
 	})
+	// show math.equation: set ref(supplement: "式")
+	// show ref: it => {
+	// 	let eq = math.equation
+	// 	let el = it.element
+	// 	if el != none and el.func() == eq {
+	// 		// Override equation references.
+	// 		"式 "
+	// 		str(counter(eq).at(el.location()).at(0))
+	// 	} else {
+	// 		// Other references as usual.
+	// 		it
+	// 	}
+	// }
 
 	set par(leading: 0.75em)