導入成本的二次律與可修改半徑：線性生產撞上規模正比的對帳，以及跑道如何在無告警下耗盡

-- 導入成本的二次律與可修改半徑：以關聯模型把成本物理寫成可查詢的不變式。
-- 執行：sqlite3 :memory: < this.sql    （任一不變式不成立即由 CHECK 約束中止）

PRAGMA foreign_keys = ON;

-- 模型參數。c = 單次導入的對帳單價；B = 可用注意力/脈絡預算；R_min = 可安全修改的下限。
CREATE TABLE params (key TEXT PRIMARY KEY, val REAL NOT NULL CHECK (val > 0));
INSERT INTO params (key, val) VALUES
  ('c',       0.01),     -- 每個既有單元的對帳成本
  ('B',       1.0),      -- 單次變更可支配的注意力預算
  ('R_min',   0.05),     -- 可修改半徑低於此值即視為跑道耗盡
  ('d',       4.0),      -- 繞過（另起新單元）的固定成本
  ('N0',      100.0);    -- 起始系統規模

-- 兩條產能情境：每 tick 新增 p 個單元。p 翻倍用來檢驗撞牆時間的敏感度。
CREATE TABLE scenarios (p REAL PRIMARY KEY CHECK (p > 0), label TEXT NOT NULL);
INSERT INTO scenarios VALUES (6.0, '基準產能'), (12.0, '產能翻倍');


-- 變更帳本：以參照完整性與觸發器把成本物理寫成不可繞過的狀態不變式。
CREATE TABLE units (unit_id INTEGER PRIMARY KEY, created_tick INTEGER NOT NULL CHECK (created_tick > 0));
CREATE TABLE changes (
    change_id        INTEGER PRIMARY KEY,
    tick             INTEGER NOT NULL CHECK (tick > 0),
    kind             TEXT    NOT NULL CHECK (kind IN ('create', 'modify')),
    unit_id          INTEGER NOT NULL REFERENCES units(unit_id),
    integration_cost REAL    NOT NULL CHECK (integration_cost >= 0)
);

-- 不變式一：修改必須指向既有單元。繞過行為在帳上與修改行為不可混為一談。
CREATE TRIGGER modify_must_target_existing_unit
BEFORE INSERT ON changes FOR EACH ROW WHEN NEW.kind = 'modify'
BEGIN
    SELECT CASE WHEN NOT EXISTS (SELECT 1 FROM units WHERE unit_id = NEW.unit_id)
        THEN RAISE(ABORT, '不變式違反：modify 必須指向既有單元') END;
END;

-- 不變式二：修改的導入成本必須與當前系統規模成正比，不得以固定值登帳。
CREATE TRIGGER integration_cost_must_scale_with_size
BEFORE INSERT ON changes FOR EACH ROW WHEN NEW.kind = 'modify'
BEGIN
    SELECT CASE WHEN ABS(NEW.integration_cost
                         - (SELECT val FROM params WHERE key = 'c') * (SELECT COUNT(*) FROM units)) > 1e-9
        THEN RAISE(ABORT, '不變式違反：導入成本必須與當前系統規模 N 成正比') END;
END;

INSERT INTO units (unit_id, created_tick) VALUES (1, 1), (2, 1), (3, 2), (4, 2), (5, 3);
INSERT INTO changes (tick, kind, unit_id, integration_cost) VALUES
    (4, 'create', 5, 0.0),      -- 新增：導入成本此處以 0 計，成本落在後續每次對帳
    (5, 'modify', 3, 0.05),     -- 修改：0.01 * 5 個既有單元 = 0.05，符合不變式二
    (6, 'modify', 1, 0.05);
-- 下列兩行任一解除註解都會中止腳本，錯誤訊息即不變式名稱：
--   INSERT INTO changes (tick, kind, unit_id, integration_cost) VALUES (7, 'modify', 99, 0.05);
--     Runtime error: 不變式違反：modify 必須指向既有單元
--   INSERT INTO changes (tick, kind, unit_id, integration_cost) VALUES (7, 'modify', 1, 0.01);
--     Runtime error: 不變式違反：導入成本必須與當前系統規模 N 成正比

-- 規模軌跡。單元數 N(t) = N0 + p*t，生產成本 O(1) 與規模無關。
CREATE TABLE trajectory AS
WITH RECURSIVE t(p, tick, n_units) AS (
    SELECT s.p, 1, (SELECT val FROM params WHERE key = 'N0') FROM scenarios s
  UNION ALL
    SELECT p, tick + 1, n_units + p FROM t WHERE tick < 400
)
SELECT p, tick, n_units FROM t;

-- 每 tick 的導入成本 O(N)、累計導入成本（對 t 的離散積分）、可修改半徑 R = min(1, B/(cN))。
CREATE VIEW cost_curve AS
SELECT
    tr.p,
    tr.tick,
    tr.n_units,
    (SELECT val FROM params WHERE key = 'c') * tr.n_units                         AS integration_cost,
    1.0                                                                           AS production_cost,
    MIN(1.0, (SELECT val FROM params WHERE key = 'B')
             / ((SELECT val FROM params WHERE key = 'c') * tr.n_units))           AS modifiable_radius,
    -- 繞過決策：當對帳成本超過另起新單元的固定成本，理性選擇是不動舊碼。
    CASE WHEN (SELECT val FROM params WHERE key = 'c') * tr.n_units
              > (SELECT val FROM params WHERE key = 'd')
         THEN 'create' ELSE 'modify' END                                          AS rational_action
FROM trajectory tr;

CREATE VIEW cumulative_cost AS
SELECT p, tick,
       (SELECT SUM(integration_cost) FROM cost_curve c2
         WHERE c2.p = c1.p AND c2.tick <= c1.tick) AS cum_integration,
       (SELECT SUM(production_cost) FROM cost_curve c3
         WHERE c3.p = c1.p AND c3.tick <= c1.tick) AS cum_production
FROM cost_curve c1;

-- 長期更新率：滾動窗口內「動到既有單元」的變更佔比。
CREATE VIEW long_term_update_rate AS
SELECT p,
       (tick / 50) * 50 AS window_start,
       AVG(CASE WHEN rational_action = 'modify' THEN 1.0 ELSE 0.0 END) AS ltu_rate
FROM cost_curve
GROUP BY p, tick / 50;

-- 跑道耗盡時點：可修改半徑首次跌破 R_min 的 tick。
CREATE VIEW runway AS
SELECT p, MIN(tick) AS exhaustion_tick
FROM cost_curve
WHERE modifiable_radius < (SELECT val FROM params WHERE key = 'R_min')
GROUP BY p;

-- ---- 不變式：任一條不成立，CHECK (ok = 1) 立即中止整個腳本 ----
CREATE TABLE assertions (
    name   TEXT PRIMARY KEY,
    ok     INTEGER NOT NULL CHECK (ok = 1),
    detail TEXT
);

-- 1. 導入成本對規模嚴格遞增，生產成本恆定：兩條曲線的形狀不同。
INSERT INTO assertions
SELECT 'integration_grows_production_flat',
       CASE WHEN MAX(integration_cost) > MIN(integration_cost) * 10
             AND MAX(production_cost) = MIN(production_cost) THEN 1 ELSE 0 END,
       'integration ' || ROUND(MIN(integration_cost), 4) || ' -> ' || ROUND(MAX(integration_cost), 4)
FROM cost_curve WHERE p = 6.0;

-- 2. 累計導入成本是二次的：tick 加倍時累計值約成四倍（線性者只成兩倍）。
INSERT INTO assertions
SELECT 'cumulative_integration_is_quadratic',
       CASE WHEN ratio BETWEEN 3.4 AND 4.2 THEN 1 ELSE 0 END,
       'cum(400)/cum(200) = ' || ROUND(ratio, 3)
FROM (SELECT (SELECT cum_integration FROM cumulative_cost WHERE p = 6.0 AND tick = 400)
           / (SELECT cum_integration FROM cumulative_cost WHERE p = 6.0 AND tick = 200) AS ratio);

-- 3. 累計生產成本是線性的：同一檢驗下比值約為 2。
INSERT INTO assertions
SELECT 'cumulative_production_is_linear',
       CASE WHEN ratio BETWEEN 1.9 AND 2.1 THEN 1 ELSE 0 END,
       'cum(400)/cum(200) = ' || ROUND(ratio, 3)
FROM (SELECT (SELECT cum_production FROM cumulative_cost WHERE p = 6.0 AND tick = 400)
           / (SELECT cum_production FROM cumulative_cost WHERE p = 6.0 AND tick = 200) AS ratio);

-- 4. 可修改半徑單調不增：跑道只會被消耗，不會自行恢復。
INSERT INTO assertions
SELECT 'radius_monotonically_shrinks',
       CASE WHEN COUNT(*) = 0 THEN 1 ELSE 0 END,
       'violating ticks = ' || COUNT(*)
FROM cost_curve a
JOIN cost_curve b ON b.p = a.p AND b.tick = a.tick + 1
WHERE b.modifiable_radius > a.modifiable_radius + 1e-12;

-- 5. 撞牆時間對產能近似反比：產能翻倍使耗盡時點約減半。
INSERT INTO assertions
SELECT 'runway_inversely_sensitive_to_throughput',
       CASE WHEN ratio BETWEEN 1.8 AND 2.2 THEN 1 ELSE 0 END,
       'T*(p=6)/T*(p=12) = ' || ROUND(ratio, 3)
FROM (SELECT CAST((SELECT exhaustion_tick FROM runway WHERE p = 6.0) AS REAL)
           / (SELECT exhaustion_tick FROM runway WHERE p = 12.0) AS ratio);

-- 6. 繞過行為：越過臨界規模後，長期更新率塌到近零——舊碼不是被維護，是被放棄。
INSERT INTO assertions
SELECT 'long_term_update_rate_collapses',
       CASE WHEN early > 0.9 AND late < 0.05 THEN 1 ELSE 0 END,
       'early=' || ROUND(early, 4) || ' late=' || ROUND(late, 4)
FROM (SELECT (SELECT ltu_rate FROM long_term_update_rate WHERE p = 6.0 AND window_start = 0)   AS early,
             (SELECT ltu_rate FROM long_term_update_rate WHERE p = 6.0 AND window_start = 350) AS late);

-- ---- 報表 ----
SELECT '--- 成本曲線抽樣（p = 6） ---';
SELECT tick, ROUND(n_units, 0) AS n, ROUND(production_cost, 3) AS 生產,
       ROUND(integration_cost, 3) AS 導入, ROUND(modifiable_radius, 4) AS 可修改半徑, rational_action AS 理性動作
FROM cost_curve WHERE p = 6.0 AND tick IN (1, 50, 100, 150, 200, 300, 400);

SELECT '--- 長期更新率（p = 6，每 50 tick 一窗） ---';
SELECT window_start, ROUND(ltu_rate, 4) AS ltu_rate FROM long_term_update_rate WHERE p = 6.0;

SELECT '--- 跑道耗盡時點 ---';
SELECT s.label, r.p, r.exhaustion_tick FROM runway r JOIN scenarios s ON s.p = r.p;

SELECT '--- 不變式 ---';
SELECT name, detail FROM assertions ORDER BY name;
SELECT '全部不變式通過（任一不成立會由 CHECK (ok = 1) 中止腳本）。';