%%writefile marx_ltv.lean

/-
  マルクスの労働価値説の矛盾を Lean で証明する
  文責: JRF / 補筆・証明: Claude Opus 5.5
  Lean 4 v4.34.1 + Mathlib
-/
import Mathlib

namespace MarxLTV

/-! ## 1. 2期間モデルと「労働力の空売り」

* `lam0`, `lam1` : 生活手段 1 単位の価値（社会的必要労働時間）。t=0, t=1。
* `b`            : 労働力 1 日分の再生産に必要な生活手段の量。
* 労働力 1 日分の価値は `v t = lam t * b`（『資本論』第1巻第4章第3節）。

マルクスの価値規定は「**現在の**再生産に必要な労働時間」なので、
イノベーションで `lam1 < lam0` となると、t=0 に存在したものの価値も t=1 には下がる
（第13章の「道徳的摩滅」）。
-/

/-- 2期間・1財経済。 -/
structure TwoPeriod where
  lam0 : ℝ
  lam1 : ℝ
  b    : ℝ
  hlam0 : 0 < lam0
  hlam1 : 0 < lam1
  hb    : 0 < b

variable (E : TwoPeriod)

/-- 労働力 1 日分の価値（t=0）。 -/
def v0 : ℝ := E.lam0 * E.b
/-- 労働力 1 日分の価値（t=1）。 -/
def v1 : ℝ := E.lam1 * E.b

/-- イノベーション：生活手段の社会的必要労働時間が下がる。 -/
def Innovation : Prop := E.lam1 < E.lam0

/-- 労働力の空売り（JRF 2026年4月）：t=0 に労働力 `N` 日分を現物で借り、t=1 に `N` 日分を現物で返す。
資本家の価値利得 = 受け取った価値 − 返した価値。 -/
def shortGain (N : ℝ) : ℝ := N * v0 E - N * v1 E

/-- 貸し手（労働者側）の価値利得。 -/
def lenderGain (N : ℝ) : ℝ := N * v1 E - N * v0 E

/-- 空売りの区間で資本家が「付け加えた価値」= 引き渡した価値 − 受け取った価値。
労働価値説では、ある主体が付け加えた価値はその主体の生きた労働に等しい。 -/
def shortValueAdded (N : ℝ) : ℝ := N * v1 E - N * v0 E

Writing marx_ltv.lean

%%writefile -a marx_ltv.lean

/-- 定理1.1：イノベーションがあれば、労働力の空売りは利益を生む。 -/
theorem short_sale_profit {N : ℝ} (hN : 0 < N) (hI : Innovation E) :
    0 < shortGain E N := by
  unfold shortGain v0 v1 Innovation at *
  have hb := E.hb
  have : E.lam1 * E.b < E.lam0 * E.b := mul_lt_mul_of_pos_right hI hb
  nlinarith

/-- 定理1.2（流通は価値を生まない、『資本論』第1巻第4章第2節）：空売りの区間はゼロサム。 -/
theorem circulation_zero_sum (N : ℝ) : shortGain E N + lenderGain E N = 0 := by
  unfold shortGain lenderGain; ring

/-- 定理1.3：空売りで儲けた資本家がその区間で付け加えた価値はマイナス。
つまり、資本家の「労働」を付加価値で測ると負になる。 -/
theorem short_value_added_neg {N : ℝ} (hN : 0 < N) (hI : Innovation E) :
    shortValueAdded E N < 0 := by
  have h := short_sale_profit E hN hI
  unfold shortGain at h; unfold shortValueAdded; linarith

/-- 定理1.4：イノベーションが期待外れで逆に `lam1 > lam0` になると、空売りした資本家の利得（所得）がマイナスになる。 -/
theorem short_sale_loss {N : ℝ} (hN : 0 < N) (hR : E.lam0 < E.lam1) :
    shortGain E N < 0 := by
  unfold shortGain v0 v1
  have : E.lam0 * E.b < E.lam1 * E.b := mul_lt_mul_of_pos_right hR E.hb
  nlinarith

Appending to marx_ltv.lean

%%writefile -a marx_ltv.lean

/-- 「資本家も労働者の一人である」という解釈（JRF 2025年9月の読み）を、
  空売りの区間に適用したもの。資本家の労働を `L` とすると、
  * 生産の側（労働価値説）: 付け加えた価値 = 労働 `L`
  * 分配の側（正当な取り分）: 所得 = 労働 `L`
  * 労働は時間の支出なので `0 ≤ L`。 -/
structure CapitalistAsWorker (N : ℝ) where
  L : ℝ
  nonneg : 0 ≤ L
  production : shortValueAdded E N = L
  distribution : shortGain E N = L

/-- **主定理1**：労働力を空売りした資本家を「労働者」とみなす一貫した帰属ができるのは、
  価値がまったく変わらない（`lam1 = lam0`）とき、つまりイノベーションがないときに限る。 -/
theorem capitalist_as_worker_iff_no_innovation {N : ℝ} (hN : 0 < N) :
    Nonempty (CapitalistAsWorker E N) ↔ E.lam1 = E.lam0 := by
  constructor
  · rintro ⟨L, hL, hp, hd⟩
    unfold shortValueAdded at hp; unfold shortGain at hd
    unfold v0 v1 at *
    have h0 : N * (E.lam0 * E.b) - N * (E.lam1 * E.b) = 0 := by linarith
    have h1 : N * E.b * (E.lam0 - E.lam1) = 0 := by linarith [h0]
    have hNb : N * E.b ≠ 0 := by have := E.hb; positivity
    have := (mul_eq_zero.mp h1).resolve_left hNb
    linarith
  · intro h
    refine ⟨⟨0, le_refl _, ?_, ?_⟩⟩ <;>
      simp [shortValueAdded, shortGain, v0, v1, h]

/-- 系：イノベーションがあれば、資本家の労働は「付加価値で測ればマイナス」になる。 -/
theorem innovation_contradiction {N : ℝ} (hN : 0 < N) (hI : Innovation E) :
    IsEmpty (CapitalistAsWorker E N) := by
  rw [← not_nonempty_iff, capitalist_as_worker_iff_no_innovation E hN]
  exact ne_of_lt hI

/-- 系：イノベーションの成否にかかわらず、価値が動けば（`lam1 ≠ lam0`）、
  空売りした資本家の「労働」は二つの測り方のどちらかでマイナスになる。 -/
theorem capitalist_labor_negative_somewhere {N : ℝ} (hN : 0 < N)
    (hne : E.lam1 ≠ E.lam0) :
    shortValueAdded E N < 0 ∨ shortGain E N < 0 := by
  rcases lt_or_gt_of_ne hne with h | h
  · exact Or.inl (short_value_added_neg E hN h)
  · exact Or.inr (short_sale_loss E hN h)

Appending to marx_ltv.lean

%%writefile -a marx_ltv.lean

/-! ## 2. 空売りを許す市場での一般定理

ポジションの集合 `P` を加法群とし（空売り＝逆ポジション `-p` が常に取れる）、
`gain : P →+ ℝ` を各ポジションの価値利得（期首と期末の価値の差）とする。
「所得はその人の労働の価値である」（帰属仮説）と「労働は非負」を課す。 -/

/-- 帰属仮説：どのポジションの保有者も、利得 = 労働 ≥ 0。 -/
def AttributionHyp {P : Type*} [AddCommGroup P] (gain : P →+ ℝ) : Prop :=
  ∀ p : P, 0 ≤ gain p

/-- **主定理2（ミラー・トレーダー）**：空売りを許すと、帰属仮説のもとで利得は恒等的にゼロ。 -/
theorem mirror_trader {P : Type*} [AddCommGroup P] (gain : P →+ ℝ)
    (h : AttributionHyp gain) : ∀ p, gain p = 0 := by
  intro p
  have h1 := h p
  have h2 := h (-p)
  rw [map_neg] at h2
  linarith

/-- 対偶：価値を動かすポジションが一つでもあれば、誰かの「労働」はマイナス。 -/
theorem exists_negative_labor {P : Type*} [AddCommGroup P] (gain : P →+ ℝ)
    {p : P} (hp : gain p ≠ 0) : ∃ q, gain q < 0 := by
  rcases lt_or_gt_of_ne hp with h | h
  · exact ⟨p, h⟩
  · exact ⟨-p, by rw [map_neg]; linarith⟩

/-- 有限人数版：流通（交換）は価値を生まない、つまり利得の総和はゼロ。
  そこで全員の利得 = 労働 ≥ 0 とすると、全員の利得はゼロになる。 -/
theorem zero_sum_forces_zero {ι : Type*} (s : Finset ι) (gain : ι → ℝ)
    (hsum : ∑ i ∈ s, gain i = 0) (hnn : ∀ i ∈ s, 0 ≤ gain i) :
    ∀ i ∈ s, gain i = 0 :=
  (Finset.sum_eq_zero_iff_of_nonneg hnn).mp hsum

Appending to marx_ltv.lean

%%writefile -a marx_ltv.lean

/-! ## 3. 空売り市場がなくても：賃金の後払いは労働力の空売りである

『資本論』第1巻第4章第3節：資本主義のもとでは労働力の代価は使用の**後で**支払われ、
「労働者は資本家に信用を与える」。実物賃金 `b` を t=1 に払う雇用契約を考える。 -/

/-- 賃金後払い契約で、資本家が受け取る労働力の価値（t=0）と払う賃金の価値（t=1）の差。 -/
def wageCreditGain (N : ℝ) : ℝ := N * v0 E - N * (E.lam1 * E.b)

/-- 定理3.1：賃金後払いは、労働力 `N` 日分の空売りとまったく同じ利得を生む。 -/
theorem wage_arrears_is_short_sale (N : ℝ) : wageCreditGain E N = shortGain E N := by
  unfold wageCreditGain shortGain v1; ring

/-- **主定理3**：空売り市場がなくても、賃金を後払いする雇用とイノベーションがあれば、
  後払いの区間での労働者側の利得 `-wageCreditGain`（＝帰属仮説のもとでの労働者の「労働」）はマイナスになる。
  資本家側は定理1.3と同じく付加価値がマイナスになるので、「全員が労働者」という一貫した帰属はできない。 -/
theorem innovation_alone_suffices {N : ℝ} (hN : 0 < N) (hI : Innovation E) :
    ¬ (0 ≤ -wageCreditGain E N) := by
  rw [wage_arrears_is_short_sale]
  have := short_sale_profit E hN hI
  linarith

Appending to marx_ltv.lean

!pip install -q japanize-matplotlib
import japanize_matplotlib

     ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 0.0/4.1 MB ? eta -:--:--
     ╸━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 0.1/4.1 MB 2.4 MB/s eta 0:00:02
     ━━╸━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 0.3/4.1 MB 4.0 MB/s eta 0:00:01
     ━━━━━━━━╺━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 0.8/4.1 MB 7.6 MB/s eta 0:00:01
     ━━━━━━━━━━━━━━━━━━━━━╺━━━━━━━━━━━━━━━━━━ 2.2/4.1 MB 15.4 MB/s eta 0:00:01
     ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━╸ 4.1/4.1 MB 24.4 MB/s eta 0:00:01
     ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 4.1/4.1 MB 21.1 MB/s eta 0:00:00
  Preparing metadata (setup.py) ... done
  Building wheel for japanize-matplotlib (setup.py) ... done

import numpy as np
import matplotlib.pyplot as plt
from matplotlib import font_manager

# 日本語フォント（Colab などで無ければ英字のまま描く）
for name in ["Noto Sans CJK JP", "IPAexGothic", "IPAGothic"]:
    if any(name in f.name for f in font_manager.fontManager.ttflist):
        plt.rcParams["font.family"] = name
        break
plt.rcParams.update({
    "axes.spines.top": False, "axes.spines.right": False,
    "axes.edgecolor": "#8a8984", "axes.labelcolor": "#52514e",
    "xtick.color": "#52514e", "ytick.color": "#52514e",
    "axes.grid": True, "grid.color": "#e6e5e1", "grid.linewidth": 0.8,
    "lines.linewidth": 2, "figure.dpi": 100, "axes.unicode_minus": False,
})
C1, C2, C3, C4 = "#2a78d6", "#eb6834", "#1baf7a", "#6250d6"   # 系列色（固定順）
INK, INK2 = "#0b0b0b", "#52514e"

# シミュレーション1：イノベーションの起こる経済で労働力を毎期空売りする（または賃金を後払いする）
rng = np.random.default_rng(20261019)
T, b, N = 60, 1.0, 1.0
p_innov, p_shock = 0.15, 0.05      # 1期あたりのイノベーション確率と、費用が上がるショックの確率

def lam_path(rng, T):
    lam = np.empty(T + 1); lam[0] = 1.0
    for t in range(T):
        f = 1.0
        if rng.random() < p_innov: f *= 1 - rng.uniform(0.10, 0.30)
        if rng.random() < p_shock: f *= 1 + rng.uniform(0.05, 0.15)
        lam[t + 1] = lam[t] * f
    return lam

lam = lam_path(rng, T)
short_gain = N * b * (lam[:-1] - lam[1:])   # 資本家の利得（= 帰属労働：所得の側）
value_added = -short_gain                   # 資本家が付け加えた価値（= 帰属労働：生産の側）

fig, axes = plt.subplots(2, 1, figsize=(8, 6), sharex=True, gridspec_kw={"height_ratios": [1, 1.2]})
axes[0].step(range(T + 1), lam, where="post", color=C1)
axes[0].set_ylabel("λ（生活手段1単位の価値）")
axes[0].set_title("イノベーションで λ が下がる（道徳的摩滅）", loc="left", color=INK)
t = np.arange(T)
axes[1].bar(t - 0.2, short_gain, width=0.4, color=C1, label="所得の側：空売りの利得")
axes[1].bar(t + 0.2, value_added, width=0.4, color=C2, label="生産の側：付け加えた価値")
axes[1].axhline(0, color=INK2, linewidth=1)
axes[1].set_ylabel("資本家の「労働」")
axes[1].set_xlabel("期 t")
axes[1].legend(frameon=False, loc="upper right")
axes[1].set_title("どちらの測り方でも、λ が動いた期には必ずどちらかがマイナス", loc="left", color=INK)
fig.tight_layout(); plt.show()

moved = np.abs(short_gain) > 1e-12
print(f"λ が動いた期: {moved.sum()} / {T}")
print(f"  所得の側がマイナスの期: {(short_gain < 0).sum()}  生産の側がマイナスの期: {(value_added < 0).sum()}")
print(f"  両方とも非負で済んだ期（λ が動いた期のうち）: {((short_gain >= 0) & (value_added >= 0) & moved).sum()}")

λ が動いた期: 14 / 60
  所得の側がマイナスの期: 3  生産の側がマイナスの期: 11
  両方とも非負で済んだ期（λ が動いた期のうち）: 0

# 1000 経路で：「資本家も労働者」と一貫して言える（どの期も両方非負）経路はいくつあるか
runs = 1000
ok = 0; neg_share = []
for _ in range(runs):
    l = lam_path(rng, T)
    g = b * (l[:-1] - l[1:])
    ok += np.all(np.abs(g) < 1e-12)
    neg_share.append(np.mean(np.abs(g) > 1e-12))
print(f"一貫した帰属が可能な経路: {ok} / {runs}")
print(f"マイナスの「労働」が現れる期の割合（平均）: {np.mean(neg_share):.3f}")
print(f"理論値（どちらかのショックが起きる確率） 1-(1-{p_innov})(1-{p_shock}) = {1-(1-p_innov)*(1-p_shock):.3f}")

一貫した帰属が可能な経路: 0 / 1000
マイナスの「労働」が現れる期の割合（平均）: 0.190
理論値（どちらかのショックが起きる確率） 1-(1-0.15)(1-0.05) = 0.193

%%writefile -a marx_ltv.lean

/-! ## 4. 幸運は労働か：時点の議論

期 `t` に帰属される労働を `A t`、その期首の資産価値を `V t` とする。
「価値の変化はすべて誰かの労働（幸運も研究開発も含む）による」とすると
  `V (t+1) = V t + A t`。
幸運によって価値が `V t0` から `V t1` に変わるなら、その「幸運の労働」はどこかの期に置かれる。
置く場所は、幸運より前（予見された）でも後（事後的な努力）でもよい。 -/

/-- 価値の変化を区間の帰属労働の和で表す（望遠鏡和）。 -/
theorem value_change_eq_sum (V A : ℕ → ℝ) (hV : ∀ t, V (t + 1) = V t + A t)
    (t0 k : ℕ) : V (t0 + k) - V t0 = ∑ i ∈ Finset.range k, A (t0 + i) := by
  induction k with
  | zero => simp
  | succ k ih =>
    rw [Finset.sum_range_succ, ← ih, ← add_assoc, hV]
    ring

/-- 幸運で価値が動けば、ある期 `t` に非ゼロの労働が帰属されている。 -/
theorem luck_labor_somewhere (V A : ℕ → ℝ) (hV : ∀ t, V (t + 1) = V t + A t)
    (t0 k : ℕ) (hΔ : V (t0 + k) ≠ V t0) : ∃ i < k, A (t0 + i) ≠ 0 := by
  by_contra hcon
  push Not at hcon
  apply hΔ
  have h := value_change_eq_sum V A hV t0 k
  have : ∑ i ∈ Finset.range k, A (t0 + i) = 0 :=
    Finset.sum_eq_zero (fun i hi => hcon i (Finset.mem_range.mp hi))
  linarith

/-- **主定理4（幸運の裁定）**：幸運で価値が動くとき、その「幸運の労働」をどの期に置いても、
  その期をまたいで現物を貸し借りする二人（買い持ちと空売り）のどちらかの「労働」はマイナスになる。 -/
theorem luck_arbitrage (V A : ℕ → ℝ) (hV : ∀ t, V (t + 1) = V t + A t)
    (t0 k : ℕ) (hΔ : V (t0 + k) ≠ V t0) :
    ∃ t, (V (t + 1) - V t < 0) ∨ (-(V (t + 1) - V t) < 0) := by
  obtain ⟨i, -, hi⟩ := luck_labor_somewhere V A hV t0 k hΔ
  refine ⟨t0 + i, ?_⟩
  rw [hV]
  rcases lt_or_gt_of_ne hi with h | h
  · left; linarith
  · right; linarith

/-- 幸運の前に置いても後に置いても、同じ結論になる（スケッチの場合分けをそのまま書いたもの）。 -/
theorem luck_before_or_after (V A : ℕ → ℝ) (hV : ∀ t, V (t + 1) = V t + A t)
    (τ tstar : ℕ) (hA : A tstar ≠ 0) :
    (tstar < τ ∨ τ ≤ tstar) ∧
      ((V (tstar + 1) - V tstar < 0) ∨ (-(V (tstar + 1) - V tstar) < 0)) := by
  refine ⟨lt_or_ge tstar τ, ?_⟩
  rw [hV]
  rcases lt_or_gt_of_ne hA with h | h
  · left; linarith
  · right; linarith

/-- 価値を**下げる**イノベーション（道徳的摩滅）なら、空売りの相手がいなくても、
  帰属労働はどこかでマイナスになる。 -/
theorem depreciating_innovation_negative (V A : ℕ → ℝ) (hV : ∀ t, V (t + 1) = V t + A t)
    (t0 k : ℕ) (hdown : V (t0 + k) < V t0) : ∃ i < k, A (t0 + i) < 0 := by
  by_contra hcon
  push Not at hcon
  have h := value_change_eq_sum V A hV t0 k
  have : 0 ≤ ∑ i ∈ Finset.range k, A (t0 + i) :=
    Finset.sum_nonneg (fun i hi => hcon i (Finset.mem_range.mp hi))
  linarith

Appending to marx_ltv.lean

# シミュレーション2：幸運の労働をどこに置くか。特許の価値が τ=10 で 0 から 1 に跳ねる
T2, tau, G = 20, 10, 1.0
schemes = {
    "前に置く（τ前の10期に均等に積む）": np.r_[np.full(tau, G / tau), np.zeros(T2 - tau)],
    "その時点に置く（τ に一括）":         np.r_[np.zeros(tau), [G], np.zeros(T2 - tau - 1)],
    "後に置く（τ 後の努力として）":       np.r_[np.zeros(tau + 1), np.full(T2 - tau - 1, G / (T2 - tau - 1))],
}

for name, A in schemes.items():
    V = np.r_[0.0, np.cumsum(A)]             # V(t+1) = V(t) + A(t)
    long_pnl = V[1:] - V[:-1]                # 各期をまたぐ現物の貸借：借り手（買い持ち）
    short_pnl = -long_pnl                    # 貸し手の逆側（空売り）
    bad = np.where((long_pnl < 0) | (short_pnl < 0))[0]
    print(f"{name}\n    買い持ちの利得の最小 {long_pnl.min():+.3f} / 空売りの利得の最小 {short_pnl.min():+.3f}"
          f" / どちらかがマイナスになる期 t = {bad.tolist()}")

前に置く（τ前の10期に均等に積む）
    買い持ちの利得の最小 +0.000 / 空売りの利得の最小 -0.100 / どちらかがマイナスになる期 t = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
その時点に置く（τ に一括）
    買い持ちの利得の最小 +0.000 / 空売りの利得の最小 -1.000 / どちらかがマイナスになる期 t = [10]
後に置く（τ 後の努力として）
    買い持ちの利得の最小 +0.000 / 空売りの利得の最小 -0.111 / どちらかがマイナスになる期 t = [11, 12, 13, 14, 15, 16, 17, 18, 19]

%%writefile -a marx_ltv.lean

/-! ## 5. 帰属労働は「本人の行為」の関数ではない

労働とは本人が行うことである。だから、同じことをした人には同じ労働が帰属されるべきだ。
ところが、他人が生活手段部門で起こしたイノベーションで `lam` が下がると、
自分は何もしていない資本家の利得（相対的剰余価値、第1巻第10章）が増える。 -/

/-- 労働者 `N` 人を 1 日 `h` 時間働かせる資本家の剰余価値。価値は `lam * b` で決まる。 -/
def surplusValue (lam b h N : ℝ) : ℝ := N * (h - lam * b)

/-- 定理5.1（相対的剰余価値）：`lam` が下がると、資本家の行為（`h`, `N`）が同じでも剰余価値は増える。 -/
theorem relative_surplus_value {lam lam' b h N : ℝ} (hb : 0 < b) (hN : 0 < N)
    (hl : lam' < lam) : surplusValue lam b h N < surplusValue lam' b h N := by
  unfold surplusValue
  have : lam' * b < lam * b := mul_lt_mul_of_pos_right hl hb
  nlinarith

/-- **主定理5**：「利得 = 労働」と「労働は本人の行為だけで決まる」は両立しない。 -/
theorem attribution_not_function_of_action {lam lam' b h N : ℝ} (hb : 0 < b) (hN : 0 < N)
    (hl : lam' < lam) :
    ¬ ∃ f : ℝ × ℝ → ℝ, ∀ l, surplusValue l b h N = f (h, N) := by
  rintro ⟨f, hf⟩
  have h1 := hf lam
  have h2 := hf lam'
  have := relative_surplus_value hb hN hl (h := h)
  linarith

Appending to marx_ltv.lean

%%writefile -a marx_ltv.lean

/-! ## 6. もう一方の角：正統派の読み（利潤は搾取）では価値がイノベーションを映さない

正統派のマルクス解釈では資本家の利得は労働ではなく、搾取（移転）である。
こう読めば上の矛盾は避けられるが、代わりに価値の尺度がイノベーションを映さなくなる。 -/

/-- 定理6.1（価値の生産性中立）：総労働 `L` で `lam` 時間/単位の財を作れば、
  生産量は `L / lam`、その総価値は `L`。生産性がいくら上がっても総価値は変わらない。 -/
theorem value_blind_to_innovation {L lam : ℝ} (hlam : lam ≠ 0) :
    lam * (L / lam) = L := by
  field_simp

/-- 定理6.2：同じ総労働で、生産性が `g` 倍の経済は `g` 倍の使用価値を作るが、総価値は等しい。 -/
theorem same_value_more_use_value {L lam g : ℝ} (hL : 0 < L) (hlam : 0 < lam) (hg : 1 < g) :
    (lam / g) * (L / (lam / g)) = lam * (L / lam) ∧ L / lam < L / (lam / g) := by
  have hg0 : 0 < g := by linarith
  constructor
  · field_simp
  · rw [div_div_eq_mul_div]
    rw [div_lt_div_iff_of_pos_right hlam]
    nlinarith

Appending to marx_ltv.lean

# シミュレーション3：資本家の取り分を抑えると、イノベーションの原資はどうなるか
#   毎期の総労働 L=1、剰余価値率 e。剰余のうち割合 s を研究開発（R&D）に回す。
#   イノベーション確率 p = 1-exp(-κ R)、成功すると λ が 10% 下がる。
def growth(s, T=100, runs=2000, e=0.5, kappa=1.0, drop=0.1, rng=rng):
    R = s * e / (1 + e)              # 1 期の価値生産 1 のうち剰余は e/(1+e)
    p = 1 - np.exp(-kappa * R)
    hits = rng.random((runs, T)) < p
    lam = np.cumprod(np.where(hits, 1 - drop, 1.0), axis=1)
    return np.exp(np.mean(-np.log(lam), axis=0))  # 労働1時間あたりの使用価値（幾何平均）

fig, ax = plt.subplots(figsize=(8, 4.2))
for s, c in zip([0.05, 0.2, 0.5, 1.0], [C1, C2, C3, C4]):
    y = growth(s)
    ax.plot(np.arange(1, 101), y, color=c, label=f"s = {s}")
    ax.annotate(f"s = {s}", (100, y[-1]), xytext=(4, 0), textcoords="offset points",
                va="center", color=INK2, fontsize=9)
ax.set_yscale("log")
ax.set_yticks([1, 2, 5, 10, 20]); ax.set_yticklabels(["1", "2", "5", "10", "20"]); ax.minorticks_off()
ax.set_xlabel("期")
ax.set_ylabel("労働1時間あたりの使用価値（対数）")
ax.set_title("剰余のうち研究開発に回す割合 s と生産性：総価値はどの s でも毎期 1 のまま", loc="left", color=INK)
ax.legend(frameon=False, loc="upper left")
fig.tight_layout(); plt.show()

%%writefile -a marx_ltv.lean

/-! ## 7. 先例：結合生産ではマルクスの価値がマイナスになる（Steedman 1975 の型）

次の数値例は本稿の筆者が作ったもので、Steedman (1975) と同じ型の現象を示す。
工程1：財1を 5、労働 1 を投入して → 財1を 6、財2を 1 産出
工程2：財2を 10、労働 1 を投入して → 財1を 3、財2を 12 産出
価値 `x1`, `x2` は「産出の価値 = 投入の価値 + 生きた労働」で決まる。 -/

theorem joint_production_negative_value (x1 x2 : ℝ)
    (h1 : 6 * x1 + 1 * x2 = 5 * x1 + 1)
    (h2 : 3 * x1 + 12 * x2 = 10 * x2 + 1) :
    x1 = -1 ∧ x2 = 2 := by
  constructor <;> linarith

/-- この経済の純生産物は (財1, 財2) = (4, 3) とどちらも正である。 -/
theorem joint_production_net_positive :
    (6 + 3 : ℝ) - 5 = 4 ∧ (1 + 12 : ℝ) - 10 = 3 := by norm_num

end MarxLTV

Appending to marx_ltv.lean

%%writefile -a marx_ltv.lean

#print axioms MarxLTV.capitalist_as_worker_iff_no_innovation
#print axioms MarxLTV.mirror_trader
#print axioms MarxLTV.innovation_alone_suffices
#print axioms MarxLTV.luck_arbitrage
#print axioms MarxLTV.attribution_not_function_of_action

Appending to marx_ltv.lean

%%bash
set -e
export PATH="$HOME/.elan/bin:$PATH"
if [ -f lakefile.lean ] && grep -q mathlib lakefile.lean; then
  echo "using the existing Lake project in the current directory"
  echo "." > .leandir
else
  if ! command -v lake >/dev/null 2>&1; then
    curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
      | sh -s -- -y --default-toolchain none
  fi
  mkdir -p marxlean && cd marxlean
  echo 'leanprover/lean4:v4.34.1' > lean-toolchain
  cat > lakefile.lean <<'EOF'
import Lake
open Lake DSL

package marxlean

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.34.1"
EOF
  lake update 2>&1 | tail -3
  lake exe cache get 2>&1 | tail -3
  cd ..
  echo "marxlean" > .leandir
fi

Downloaded: 1 file(s) [attempted 1/8908 = 0%, 173 KB/s], Decompressed: 0
Downloaded: 32 file(s) [attempted 32/8908 = 0%, 176 KB/s], Decompressed: 3
Downloaded: 138 file(s) [attempted 138/8908 = 1%, 822 KB/s], Decompressed: 12
Downloaded: 212 file(s) [attempted 212/8908 = 2%, 3266 KB/s], Decompressed: 12
Downloaded: 314 file(s) [attempted 314/8908 = 3%, 694 KB/s], Decompressed: 12
Downloaded: 408 file(s) [attempted 408/8908 = 4%, 50 KB/s], Decompressed: 63
Downloaded: 470 file(s) [attempted 470/8908 = 5%, 3903 KB/s], Decompressed: 63
Downloaded: 518 file(s) [attempted 518/8908 = 5%, 2071 KB/s], Decompressed: 63
Downloaded: 574 file(s) [attempted 574/8908 = 6%, 1156 KB/s], Decompressed: 63
Downloaded: 632 file(s) [attempted 632/8908 = 7%, 809 KB/s], Decompressed: 63
Downloaded: 685 file(s) [attempted 685/8908 = 7%, 399 KB/s], Decompressed: 63
Downloaded: 748 file(s) [attempted 748/8908 = 8%, 345 KB/s], Decompressed: 63
Downloaded: 796 file(s) [attempted 796/8908 = 8%, 640 KB/s], Decompressed: 63
Downloaded: 835 file(s) [attempted 835/8908 = 9%, 527 KB/s], Decompressed: 63
Downloaded: 888 file(s) [attempted 888/8908 = 9%, 170 KB/s], Decompressed: 63
Downloaded: 939 file(s) [attempted 939/8908 = 10%, 886 KB/s], Decompressed: 63
Downloaded: 989 file(s) [attempted 989/8908 = 11%, 155 KB/s], Decompressed: 63
Downloaded: 1037 file(s) [attempted 1037/8908 = 11%, 810 KB/s], Decompressed: 63
Downloaded: 1093 file(s) [attempted 1093/8908 = 12%, 1789 KB/s], Decompressed: 63
Downloaded: 1143 file(s) [attempted 1143/8908 = 12%, 590 KB/s], Decompressed: 63
Downloaded: 1194 file(s) [attempted 1194/8908 = 13%, 1149 KB/s], Decompressed: 63
Downloaded: 1245 file(s) [attempted 1245/8908 = 13%, 1090 KB/s], Decompressed: 63
Downloaded: 1295 file(s) [attempted 1295/8908 = 14%, 310 KB/s], Decompressed: 63
Downloaded: 1348 file(s) [attempted 1348/8908 = 15%, 402 KB/s], Decompressed: 63
Downloaded: 1404 file(s) [attempted 1404/8908 = 15%, 164 KB/s], Decompressed: 63
Downloaded: 1454 file(s) [attempted 1454/8908 = 16%, 91 KB/s], Decompressed: 63
Downloaded: 1502 file(s) [attempted 1502/8908 = 16%, 368 KB/s], Decompressed: 63
Downloaded: 1558 file(s) [attempted 1558/8908 = 17%, 140 KB/s], Decompressed: 63
Downloaded: 1608 file(s) [attempted 1608/8908 = 18%, 982 KB/s], Decompressed: 63
Downloaded: 1664 file(s) [attempted 1664/8908 = 18%, 424 KB/s], Decompressed: 63
Downloaded: 1714 file(s) [attempted 1714/8908 = 19%, 115 KB/s], Decompressed: 63
Downloaded: 1765 file(s) [attempted 1765/8908 = 19%, 140 KB/s], Decompressed: 63
Downloaded: 1816 file(s) [attempted 1816/8908 = 20%, 376 KB/s], Decompressed: 63
Downloaded: 1866 file(s) [attempted 1866/8908 = 20%, 109 KB/s], Decompressed: 63
Downloaded: 1917 file(s) [attempted 1917/8908 = 21%, 482 KB/s], Decompressed: 63
Downloaded: 1967 file(s) [attempted 1967/8908 = 22%, 151 KB/s], Decompressed: 63
Downloaded: 2016 file(s) [attempted 2016/8908 = 22%, 401 KB/s], Decompressed: 63
Downloaded: 2066 file(s) [attempted 2066/8908 = 23%, 481 KB/s], Decompressed: 63
Downloaded: 2117 file(s) [attempted 2117/8908 = 23%, 91 KB/s], Decompressed: 63
Downloaded: 2167 file(s) [attempted 2167/8908 = 24%, 460 KB/s], Decompressed: 63
Downloaded: 2220 file(s) [attempted 2220/8908 = 24%, 2951 KB/s], Decompressed: 63
Downloaded: 2271 file(s) [attempted 2271/8908 = 25%, 163 KB/s], Decompressed: 63
Downloaded: 2324 file(s) [attempted 2324/8908 = 26%, 2661 KB/s], Decompressed: 63
Downloaded: 2375 file(s) [attempted 2375/8908 = 26%, 114 KB/s], Decompressed: 63
Downloaded: 2425 file(s) [attempted 2425/8908 = 27%, 526 KB/s], Decompressed: 63
Downloaded: 2478 file(s) [attempted 2478/8908 = 27%, 175 KB/s], Decompressed: 63
Downloaded: 2534 file(s) [attempted 2534/8908 = 28%, 1013 KB/s], Decompressed: 63
Downloaded: 2594 file(s) [attempted 2594/8908 = 29%, 51 KB/s], Decompressed: 63
Downloaded: 2644 file(s) [attempted 2644/8908 = 29%, 87 KB/s], Decompressed: 63
Downloaded: 2695 file(s) [attempted 2695/8908 = 30%, 86 KB/s], Decompressed: 63
Downloaded: 2746 file(s) [attempted 2746/8908 = 30%, 393 KB/s], Decompressed: 63
Downloaded: 2796 file(s) [attempted 2796/8908 = 31%, 102 KB/s], Decompressed: 63
Downloaded: 2812 file(s) [attempted 2812/8908 = 31%, 337 KB/s], Decompressed: 63
Downloaded: 2854 file(s) [attempted 2854/8908 = 32%, 623 KB/s], Decompressed: 63
Downloaded: 2937 file(s) [attempted 2937/8908 = 32%, 196 KB/s], Decompressed: 63
Downloaded: 2972 file(s) [attempted 2972/8908 = 33%, 75 KB/s], Decompressed: 364
Downloaded: 3036 file(s) [attempted 3036/8908 = 34%, 74 KB/s], Decompressed: 364
Downloaded: 3056 file(s) [attempted 3056/8908 = 34%, 2483 KB/s], Decompressed: 364
Downloaded: 3109 file(s) [attempted 3109/8908 = 34%, 2894 KB/s], Decompressed: 364
Downloaded: 3149 file(s) [attempted 3149/8908 = 35%, 215 KB/s], Decompressed: 364
Downloaded: 3174 file(s) [attempted 3174/8908 = 35%, 617 KB/s], Decompressed: 364
Downloaded: 3225 file(s) [attempted 3225/8908 = 36%, 134 KB/s], Decompressed: 364
Downloaded: 3273 file(s) [attempted 3273/8908 = 36%, 343 KB/s], Decompressed: 364
Downloaded: 3326 file(s) [attempted 3326/8908 = 37%, 1002 KB/s], Decompressed: 364
Downloaded: 3379 file(s) [attempted 3379/8908 = 37%, 247 KB/s], Decompressed: 364
Downloaded: 3430 file(s) [attempted 3430/8908 = 38%, 1672 KB/s], Decompressed: 364
Downloaded: 3509 file(s) [attempted 3509/8908 = 39%, 1172 KB/s], Decompressed: 364
Downloaded: 3548 file(s) [attempted 3548/8908 = 39%, 1714 KB/s], Decompressed: 364
Downloaded: 3607 file(s) [attempted 3607/8908 = 40%, 58 KB/s], Decompressed: 364
Downloaded: 3663 file(s) [attempted 3663/8908 = 41%, 88 KB/s], Decompressed: 364
Downloaded: 3721 file(s) [attempted 3721/8908 = 41%, 578 KB/s], Decompressed: 364
Downloaded: 3769 file(s) [attempted 3769/8908 = 42%, 2152 KB/s], Decompressed: 364
Downloaded: 3822 file(s) [attempted 3822/8908 = 42%, 723 KB/s], Decompressed: 364
Downloaded: 3873 file(s) [attempted 3873/8908 = 43%, 2515 KB/s], Decompressed: 364
Downloaded: 3926 file(s) [attempted 3926/8908 = 44%, 2042 KB/s], Decompressed: 364
Downloaded: 3979 file(s) [attempted 3979/8908 = 44%, 3720 KB/s], Decompressed: 364
Downloaded: 4027 file(s) [attempted 4027/8908 = 45%, 443 KB/s], Decompressed: 364
Downloaded: 4056 file(s) [attempted 4056/8908 = 45%, 141 KB/s], Decompressed: 364
Downloaded: 4100 file(s) [attempted 4100/8908 = 46%, 2564 KB/s], Decompressed: 364
Downloaded: 4155 file(s) [attempted 4155/8908 = 46%, 178 KB/s], Decompressed: 364
Downloaded: 4186 file(s) [attempted 4186/8908 = 46%, 247 KB/s], Decompressed: 364
Downloaded: 4235 file(s) [attempted 4235/8908 = 47%, 130 KB/s], Decompressed: 364
Downloaded: 4285 file(s) [attempted 4285/8908 = 48%, 114 KB/s], Decompressed: 364
Downloaded: 4343 file(s) [attempted 4343/8908 = 48%, 242 KB/s], Decompressed: 364
Downloaded: 4414 file(s) [attempted 4414/8908 = 49%, 70 KB/s], Decompressed: 364
Downloaded: 4461 file(s) [attempted 4461/8908 = 50%, 101 KB/s], Decompressed: 364
Downloaded: 4525 file(s) [attempted 4525/8908 = 50%, 1387 KB/s], Decompressed: 364
Downloaded: 4548 file(s) [attempted 4548/8908 = 51%, 1218 KB/s], Decompressed: 364
Downloaded: 4598 file(s) [attempted 4598/8908 = 51%, 109 KB/s], Decompressed: 364
Downloaded: 4646 file(s) [attempted 4646/8908 = 52%, 161 KB/s], Decompressed: 364
Downloaded: 4697 file(s) [attempted 4697/8908 = 52%, 739 KB/s], Decompressed: 364
Downloaded: 4768 file(s) [attempted 4768/8908 = 53%, 431 KB/s], Decompressed: 364
Downloaded: 4823 file(s) [attempted 4823/8908 = 54%, 504 KB/s], Decompressed: 364
Downloaded: 4889 file(s) [attempted 4889/8908 = 54%, 722 KB/s], Decompressed: 364
Downloaded: 4899 file(s) [attempted 4899/8908 = 54%, 720 KB/s], Decompressed: 364
Downloaded: 4952 file(s) [attempted 4952/8908 = 55%, 465 KB/s], Decompressed: 364
Downloaded: 5005 file(s) [attempted 5005/8908 = 56%, 2569 KB/s], Decompressed: 364
Downloaded: 5056 file(s) [attempted 5056/8908 = 56%, 261 KB/s], Decompressed: 364
Downloaded: 5102 file(s) [attempted 5102/8908 = 57%, 843 KB/s], Decompressed: 364
Downloaded: 5157 file(s) [attempted 5157/8908 = 57%, 1938 KB/s], Decompressed: 364
Downloaded: 5208 file(s) [attempted 5208/8908 = 58%, 78 KB/s], Decompressed: 364
Downloaded: 5261 file(s) [attempted 5261/8908 = 59%, 3022 KB/s], Decompressed: 364
Downloaded: 5316 file(s) [attempted 5316/8908 = 59%, 47 KB/s], Decompressed: 364
Downloaded: 5374 file(s) [attempted 5374/8908 = 60%, 307 KB/s], Decompressed: 364
Downloaded: 5432 file(s) [attempted 5432/8908 = 60%, 269 KB/s], Decompressed: 364
Downloaded: 5480 file(s) [attempted 5480/8908 = 61%, 282 KB/s], Decompressed: 364
Downloaded: 5531 file(s) [attempted 5531/8908 = 62%, 778 KB/s], Decompressed: 364
Downloaded: 5586 file(s) [attempted 5586/8908 = 62%, 996 KB/s], Decompressed: 364
Downloaded: 5676 file(s) [attempted 5676/8908 = 63%, 360 KB/s], Decompressed: 364
Downloaded: 5734 file(s) [attempted 5734/8908 = 64%, 537 KB/s], Decompressed: 364
Downloaded: 5793 file(s) [attempted 5793/8908 = 65%, 1164 KB/s], Decompressed: 364
Downloaded: 5851 file(s) [attempted 5851/8908 = 65%, 708 KB/s], Decompressed: 364
Downloaded: 5940 file(s) [attempted 5940/8908 = 66%, 103 KB/s], Decompressed: 364
Downloaded: 6003 file(s) [attempted 6003/8908 = 67%, 811 KB/s], Decompressed: 364
Downloaded: 6056 file(s) [attempted 6056/8908 = 67%, 449 KB/s], Decompressed: 364
Downloaded: 6145 file(s) [attempted 6145/8908 = 68%, 2673 KB/s], Decompressed: 364
Downloaded: 6174 file(s) [attempted 6174/8908 = 69%, 354 KB/s], Decompressed: 364
Downloaded: 6251 file(s) [attempted 6251/8908 = 70%, 332 KB/s], Decompressed: 364
Downloaded: 6279 file(s) [attempted 6279/8908 = 70%, 50 KB/s], Decompressed: 364
Downloaded: 6316 file(s) [attempted 6316/8908 = 70%, 448 KB/s], Decompressed: 364
Downloaded: 6388 file(s) [attempted 6388/8908 = 71%, 245 KB/s], Decompressed: 364
Downloaded: 6443 file(s) [attempted 6443/8908 = 72%, 252 KB/s], Decompressed: 364
Downloaded: 6511 file(s) [attempted 6511/8908 = 73%, 998 KB/s], Decompressed: 364
Downloaded: 6559 file(s) [attempted 6559/8908 = 73%, 302 KB/s], Decompressed: 364
Downloaded: 6598 file(s) [attempted 6598/8908 = 74%, 1103 KB/s], Decompressed: 364
Downloaded: 6675 file(s) [attempted 6675/8908 = 74%, 108 KB/s], Decompressed: 364
Downloaded: 6726 file(s) [attempted 6726/8908 = 75%, 1441 KB/s], Decompressed: 364
Downloaded: 6788 file(s) [attempted 6788/8908 = 76%, 266 KB/s], Decompressed: 364
Downloaded: 6832 file(s) [attempted 6832/8908 = 76%, 1328 KB/s], Decompressed: 364
Downloaded: 6921 file(s) [attempted 6921/8908 = 77%, 2022 KB/s], Decompressed: 364
Downloaded: 6976 file(s) [attempted 6976/8908 = 78%, 1402 KB/s], Decompressed: 364
Downloaded: 7077 file(s) [attempted 7077/8908 = 79%, 353 KB/s], Decompressed: 364
Downloaded: 7130 file(s) [attempted 7130/8908 = 80%, 1121 KB/s], Decompressed: 364
Downloaded: 7179 file(s) [attempted 7179/8908 = 80%, 56 KB/s], Decompressed: 364
Downloaded: 7260 file(s) [attempted 7260/8908 = 81%, 143 KB/s], Decompressed: 364
Downloaded: 7330 file(s) [attempted 7330/8908 = 82%, 1195 KB/s], Decompressed: 364
Downloaded: 7383 file(s) [attempted 7383/8908 = 82%, 856 KB/s], Decompressed: 364
Downloaded: 7434 file(s) [attempted 7434/8908 = 83%, 1040 KB/s], Decompressed: 364
Downloaded: 7485 file(s) [attempted 7485/8908 = 84%, 357 KB/s], Decompressed: 364
Downloaded: 7546 file(s) [attempted 7546/8908 = 84%, 365 KB/s], Decompressed: 364
Downloaded: 7588 file(s) [attempted 7588/8908 = 85%, 1833 KB/s], Decompressed: 364
Downloaded: 7649 file(s) [attempted 7649/8908 = 85%, 1876 KB/s], Decompressed: 364
Downloaded: 7721 file(s) [attempted 7721/8908 = 86%, 1127 KB/s], Decompressed: 364
Downloaded: 7769 file(s) [attempted 7769/8908 = 87%, 582 KB/s], Decompressed: 364
Downloaded: 7814 file(s) [attempted 7814/8908 = 87%, 181 KB/s], Decompressed: 364
Downloaded: 7887 file(s) [attempted 7887/8908 = 88%, 870 KB/s], Decompressed: 364
Downloaded: 7935 file(s) [attempted 7935/8908 = 89%, 974 KB/s], Decompressed: 364
Downloaded: 7997 file(s) [attempted 7997/8908 = 89%, 382 KB/s], Decompressed: 364
Downloaded: 8052 file(s) [attempted 8052/8908 = 90%, 561 KB/s], Decompressed: 364
Downloaded: 8152 file(s) [attempted 8152/8908 = 91%, 5559 KB/s], Decompressed: 364
Downloaded: 8205 file(s) [attempted 8205/8908 = 92%, 260 KB/s], Decompressed: 364
Downloaded: 8293 file(s) [attempted 8293/8908 = 93%, 521 KB/s], Decompressed: 364
Downloaded: 8335 file(s) [attempted 8335/8908 = 93%, 867 KB/s], Decompressed: 364
Downloaded: 8410 file(s) [attempted 8410/8908 = 94%, 629 KB/s], Decompressed: 364
Downloaded: 8496 file(s) [attempted 8496/8908 = 95%, 503 KB/s], Decompressed: 364
Downloaded: 8538 file(s) [attempted 8538/8908 = 95%, 362 KB/s], Decompressed: 364
Downloaded: 8614 file(s) [attempted 8614/8908 = 96%, 179 KB/s], Decompressed: 364
Downloaded: 8665 file(s) [attempted 8665/8908 = 97%, 1983 KB/s], Decompressed: 364
Downloaded: 8731 file(s) [attempted 8731/8908 = 98%, 288 KB/s], Decompressed: 364
Downloaded: 8798 file(s) [attempted 8798/8908 = 98%, 620 KB/s], Decompressed: 364
Downloaded: 8851 file(s) [attempted 8851/8908 = 99%, 1512 KB/s], Decompressed: 364
Downloaded: 8908 file(s) [attempted 8908/8908 = 100%, 1512 KB/s], Decompressed: 364
Decompressed 8908 file(s)
Already decompressed 8908 file(s)
Using cache from origin: (some leanprover-community/mathlib4)
No files to download
Already decompressed 8908 file(s)

info: downloading installer

%%bash
export PATH="$HOME/.elan/bin:$PATH"
LEANDIR=$(cat .leandir)
FILE=$(pwd)/marx_ltv.lean
cd "$LEANDIR"
time lake env lean "$FILE" && echo "=== marx_ltv.lean: all theorems checked ==="

'MarxLTV.capitalist_as_worker_iff_no_innovation' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarxLTV.mirror_trader' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarxLTV.innovation_alone_suffices' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarxLTV.luck_arbitrage' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarxLTV.attribution_not_function_of_action' depends on axioms: [propext, Classical.choice, Quot.sound]
=== marx_ltv.lean: all theorems checked ===

real	2m58.136s
user	0m12.783s
sys	0m12.965s

記号	内容	出典
(V1) 価値規定	商品の価値は、その再生産に現在社会的に必要な労働時間	第1章。第13章の「道徳的摩滅」：新しい機械が出ると既存の機械の価値も下がる
(V2) 労働力の価値	労働力の価値 = 労働者の生活手段の価値 `v = λ·b`	第4章第3節
(V3) 流通は価値を生まない	「流通または商品交換は価値を創造しない」。不等価交換は既存の価値を再分配するだけで、一方のマイナスは他方のプラス	第4章第2節
(V4) 賃金の後払い	労働力の代価は使用の後に支払われ、「労働者は資本家に信用を与える」	第4章第3節

定理	Lean 名	内容
1.1	`short_sale_profit`	イノベーションがあれば労働力の空売りは儲かる
1.2	`circulation_zero_sum`	空売りの区間はゼロサム（流通は価値を生まない）
1.3	`short_value_added_neg`	儲けた資本家が付け加えた価値はマイナス
1.4	`short_sale_loss`	外れれば所得がマイナス
主1	`capitalist_as_worker_iff_no_innovation`	「資本家も労働者」の一貫した帰属 ⇔ `λ1 = λ0`
系	`innovation_contradiction`, `capitalist_labor_negative_somewhere`	イノベーションがあれば帰属は不可能。価値が動けばどちらかの測り方でマイナス
主2	`mirror_trader`, `exists_negative_labor`	空売りを許す市場で「利得 = 労働 ≥ 0」なら利得は恒等的に 0
4.x	`zero_sum_forces_zero`	有限人数のゼロサム版
3.1	`wage_arrears_is_short_sale`	賃金の後払い ≡ 労働力の空売り
主3	`innovation_alone_suffices`	空売り市場がなくても、イノベーションさえあれば矛盾
6.x	`value_change_eq_sum`, `luck_labor_somewhere`	幸運の労働は時間のどこかに置かれる
主4	`luck_arbitrage`, `luck_before_or_after`	前に置いても後に置いても、裁定で誰かの労働がマイナス
6.y	`depreciating_innovation_negative`	価値を下げるイノベーションなら相手がいなくてもマイナス
5.1	`relative_surplus_value`	他人のイノベーションで剰余価値が増える
主5	`attribution_not_function_of_action`	帰属労働は本人の行為の関数ではない（語義矛盾）
6.1–6.2	`value_blind_to_innovation`, `same_value_more_use_value`	正統派の角：価値は生産性を映さない
7	`joint_production_negative_value`	結合生産でのマイナスの価値（Steedman 型の例）

マルクスの労働価値説の矛盾を Lean で証明する¶

―― 労働力の空売り・幸運・イノベーション¶

要旨¶

目次¶

1. はじめに：JRF の過去の議論と証明のスケッチ¶

1.1 これまでの議論¶

1.2 証明のスケッチ（JRF）¶

1.3 何を証明し、何を証明しないか¶

2. 準備：労働価値説の何を公理とするか¶

3. 労働力の空売り（2期間モデル）¶

主定理1：資本家を「労働者」とみなす帰属は、イノベーションのないときにしかできない¶

4. 空売りを許す市場の一般定理（ミラー・トレーダー）¶

5. 空売り市場がなくても：賃金の後払いとイノベーション¶

シミュレーション1：イノベーションの起こる経済で毎期空売りする¶

6. 幸運は労働か：時点の議論¶

シミュレーション2：幸運の労働をどこに置くか¶

7. 帰属労働は本人の行為の関数ではない¶

8. もう一方の角：正統派の読みとイノベーションの原資¶

シミュレーション3：資本家の取り分を抑えると、イノベーションの原資はどうなるか¶

9. 先例：結合生産でのマイナスの価値（Steedman）¶

10. 予想される反論と応答¶

11. まとめ（定理一覧）¶

12. 参考文献¶

13. Lean 一括チェック¶