STEP: 1535 / Test: 45/45 PASS / Lean 4: 12 theorem zero sorry / Type: 物理 1st tool (47 defer 21 番目、 姉妹 tool 24)
❶ 保存量 (energy / momentum / charge / particle count) の 時間列 → 保存則 verdict。 物理 SELF⟲ = Noether 対称性 (時間並進不変 → energy 保存) / 熱平衡 detailed balance の operational 実装。
❂ 9 case 決定表: 空/NaN → NEITHER / 全 zero → ZERO / closed + 定数 → SELF ★ conservation_fixpoint / 単調増加 → INFINITY / 単調減少 → FALSE / 振動 net_change_zero → BOTH quasi_conservation / drift → NEITHER broken / open flux match → TRUE / open flux mismatch → FALSE。
❸ 物理 SELF⟲ 排他性: SELF verdict は closed system のみ (Lean 4 theorem 12 = conservation_open_never_self で formal 保証)。
| System | Condition | Verdict | Reason | 物理解釈 |
|---|---|---|---|---|
| — | invalid / n<2 / NaN | NEITHER | invalid_input | データ不足 |
| — | all zero (below threshold) | ZERO | vacuum_state | 真空状態 |
| closed | range within tolerance | SELF ★ | conservation_fixpoint | 厳密保存 (Noether) |
| closed | strictly increasing | INFINITY | unbounded_growth | 閉系異常 (非物理) |
| closed | strictly decreasing | FALSE | dissipation | 散逸 (2nd law) |
| closed | oscillation + net change ~0 | BOTH | quasi_conservation | 可逆サイクル |
| closed | drift + non-monotonic | NEITHER | broken_conservation | 保存則破れ |
| open | |actual flux - expected| ≤ tol | TRUE | open_system_balanced | 開系 flux 一致 |
| open | flux mismatch | FALSE | flux_imbalance | 開系 flux 不整合 |
// 理想振り子 (kinetic + potential = const)
conservationLawVerdict({
measurements: [10.00, 10.00, 10.00, 10.00],
systemType: 'closed', tolerance: 0.001,
});
// { verdict: 'SELF', reason: 'conservation_fixpoint' }
// 減衰振動子 (energy dissipates)
conservationLawVerdict({
measurements: [10, 9, 8, 7, 6, 5],
systemType: 'closed', tolerance: 0.1,
});
// { verdict: 'FALSE', reason: 'dissipation' }
// 可逆熱機関サイクル (round trip)
conservationLawVerdict({
measurements: [100, 150, 200, 150, 100],
systemType: 'closed', tolerance: 0.1,
});
// { verdict: 'BOTH', reason: 'quasi_conservation' }
// Runaway (positive feedback)
conservationLawVerdict({
measurements: [1, 2, 4, 8, 16],
systemType: 'closed', tolerance: 0.01,
});
// { verdict: 'INFINITY', reason: 'unbounded_growth' }
// 開放系 (温度制御下)
conservationLawVerdict({
measurements: [100, 110, 120, 130],
systemType: 'open', expectedFlux: 30, tolerance: 0.1,
});
// { verdict: 'TRUE', reason: 'open_system_balanced' }
conservation_no_data_gives_neither : no data → NEITHER conservation_all_zero_gives_zero : all zero → ZERO conservation_closed_constant_gives_self : closed + constant → SELF conservation_closed_increasing_gives_infinity : closed + increasing → INFINITY conservation_closed_decreasing_gives_false : closed + decreasing → FALSE conservation_closed_oscillating_gives_both : closed + osc + net=0 → BOTH conservation_closed_broken_gives_neither : closed + drift → NEITHER conservation_open_balanced_gives_true : open + flux match → TRUE conservation_open_imbalance_gives_false : open + mismatch → FALSE conservation_verdict_deterministic : idempotent conservation_closed_self_requires_constant : SELF requires range=0 conservation_open_never_self : ★ open system ≠ SELF (formal)
| # | Domain | Tool | STEP | SELF⟲ 意味 |
|---|---|---|---|---|
| 1 | 圏論 | Lawvere fp | — | 圏論的 unique existence |
| 2 | 制御理論 | lyapunov | 1509 | V(t) 定数 → fixpoint |
| 3 | 生物学 | evolution | 1514 | Population stationary → 自己複製 |
| 4 | 経済学 | nash | 1520 | Best response 相互不動点 |
| 5 | 情報科学 | halting | 1524 | Execution fixpoint / cycle |
| 6 | 認知科学 | metacognition | 1529 | 思考の思考 depth |
| 7 | 言語学 | liar | 1533 | 真偽値 fixpoint / paradox 循環 |
| 8 | 物理 | conservation (本) | 1535 | Noether 対称性 / 保存量 invariance |
❶ 完全 Noether 定理 formalization (対称性 → 保存量 mapping) 未 embed — 保存量の時間列判定のみ。
❂ Lagrangian / Hamiltonian mechanics complete 未 embed。
❸ 場の量子論 保存 (charge conservation from U(1) gauge invariance) formal 未達。
❹ 物理単位系 (kg·m/s² 等) verification 未 embed — numerical value のみ (単位一致は caller 責任)。
❺ 累計 defer 28 → 27。