JPYC.supplyConserved_empty
名称・種別
- 名称:
JPYC.supplyConserved_empty - 種別: theorem
- モジュール:
JpycFormalVerification.State - ソース:
JpycFormalVerification/State.lean:168-169 - 概要: 初期状態 State.empty が SupplyConserved を満たす、という定理。
- 仕様: 対象
型シグネチャ
lean
JPYC.SupplyConserved JPYC.State.empty命題「SupplyConserved State.empty」を主張する定理です。すなわち 初期状態は供給保存を満たす。
解説
何を述べているか。 初期状態 State.empty において totalSupply = Σ balances（= SupplyConserved）が成り立つ、という証明です。
直感。 空状態では総供給も全残高もすべて 0 なので、両辺がともに 0 で一致します（simp で展開すれば即座に決まります）。
なぜ安全性に効くか。 供給保存 SupplyConserved の 充足可能性 の証人です。これが「transfer / mint / burn が供給保存を保つ」という連鎖の基点になります。
図解
Lean ソースコード
lean
theorem supplyConserved_empty : SupplyConserved State.empty := by
simp [SupplyConserved, State.totalBalances, State.empty]