Math Prover

定理適用の明示

• 全ての行に、どのような定理・操作を適用したかを 行末に quad (because ...) で記述する。
• 高校の教科書レベルで自明なもの（実数の四則演算、分配法則、移項など）は省略してもよい。
• 本論文中で証明されている Definition/Claim/Theorem の適用は、同じ証明中に複数回現れるとしても、決して省略してはならない。 必ず #ref(<label>) で参照する。

良い例

$
  arg^([0, 2pi))((gamma_2(-theta_(mu)))^2)
  =
  cases(
    2 arg^([0, 2pi))(gamma_2(-theta_(mu))) & quad (0 <= arg^([0, 2pi))(gamma_2(-theta_(mu))) < pi),
    2 arg^([0, 2pi))(gamma_2(-theta_(mu))) - 2pi & quad (pi <= arg^([0, 2pi))(gamma_2(-theta_(mu))) < 2pi),
  )
  quad
  (because #ref(<range_of_args_of_square_of_complex_numbers>))
$

2. インデントによる階層構造の可視化

全ての数式の階層構造に インデントを使用して、視覚的に階層構造がわかるようにする。

ルール

• Typst の数式ブロック内で、sqrt(...), (... / ...), mat(...), cases(...) などのネスト構造は 必ずインデントで表現する。
• 各階層は 2スペース でインデントする。
• 閉じ括弧は対応する開き括弧と同じインデントレベルに置く。

良い例

$
  a(theta_mu)
  &=
  sqrt(
    (
      (1 - alpha_1 e^(sqrt(-1) theta_mu))
    )
    /
    (
      (1 - alpha_1 e^(-sqrt(-1) theta_mu))
    )
    dot.c
    (
      (1 - alpha_2^(-1) e^(sqrt(-1) theta_mu))
    )
    /
    (
      (1 - alpha_2^(-1) e^(-sqrt(-1) theta_mu))
    )
  )
$

悪い例（フラットに書いている）

$
  a(theta_mu) &= sqrt((1 - alpha_1 e^(sqrt(-1) theta_mu)) / (1 - alpha_1 e^(-sqrt(-1) theta_mu)) dot.c (1 - alpha_2^(-1) e^(sqrt(-1) theta_mu)) / (1 - alpha_2^(-1) e^(-sqrt(-1) theta_mu)))
$

3. 証明の構造

Step 分割

• 証明が長い場合は === Step N: <内容> で区切る。
• 各 Step は1つの中間的な目標（中間等式の導出など）に対応させる。

接続詞

• Step 間の接続には「より、」「特に、」「したがって、」などの日本語を使用する。
• 式変形の連鎖は &= を使い、\ で改行して縦に並べる。

Proof ブロック

#proof[
  <前提条件の記述>

  === Step 1: <目標>

  $
    <式変形>
  $

  === Step 2: <目標>

  $
    <式変形>
  $

  <結論の記述>
]

4. Typst 記述規約

• Definition は #definition("名前")[...]
• Claim は #claim("名前")[...]
• Theorem は #theorem("名前")[...]
• Proof は #proof[...]
• 相互参照は <label> と @label または #ref(<label>) を使用
• because の中で参照する場合は #ref(<label>) を使用

分数の括弧ルール

Typst の数式モードでは、/ は直前・直後の 1トークン のみを分子・分母として扱う。分子または分母が複数トークンからなる場合は、必ず括弧で囲むこと。

良い例

(3pi)/2       // 分子が 3π（2トークン）なので括弧が必要
(2 s_1 c_2)/(c_1 + 1)  // 分子・分母とも複数トークン
pi/2          // 分子が π（1トークン）なので括弧不要

悪い例

3pi/2         // ✗ 3 * (π/2) と解釈され、意図した (3π)/2 にならない
2 s_1 c_2/c_1 + 1  // ✗ 分数の範囲が曖昧

5. チェックリスト（証明記述後の自己確認）

証明を書き終えたら、以下を確認すること:

• 全ての式変形が1ステップ1定理になっているか
• 本論文中の Definition/Claim/Theorem の適用に全て quad (because #ref(<...>)) が付いているか
• 数式のネスト構造が全てインデントで表現されているか
• typst compile main.typ がエラーなしで通過するか
• #ref による相互参照が正しく解決されるか