{
  "case_id": "MG-C003",
  "version": "0.1.1",
  "items": [
    {"id":"CH03-D01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.constComponents"},{"file":"Main.lean","name":"Chapter3Fresh.identityComponents"},{"file":"Main.lean","name":"Chapter3Fresh.activeComponents"},{"file":"Main.lean","name":"Chapter3Fresh.components_partition"}],"representation":"按常值优先定义三类指标并证明互斥穷尽。","dependencies":[]},
    {"id":"CH03-D02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.fiber"},{"file":"Main.lean","name":"Chapter3Fresh.componentFiber"},{"file":"Main.lean","name":"Chapter3Fresh.subfamily_zero_iff"},{"file":"Main.lean","name":"Chapter3Fresh.fiber_singleton"}],"representation":"纤维是 U 中复合子族伪度量为零的点；证明单分量与各分量零距条件对应。","dependencies":[]},
    {"id":"CH03-D03","status":"incomplete","declarations":[],"representation":"点值关系、零距关系、像商和纤维预序未交付。","dependencies":[]},
    {"id":"CH03-D04","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.goodRadius"},{"file":"Main.lean","name":"Chapter3Fresh.pointRadius"},{"file":"Main.lean","name":"Chapter3Fresh.radius_ball_iff"}],"representation":"对有限正合法半径取上确界，合法性等价于受限球包含。","dependencies":[]},
    {"id":"CH03-D05","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.uniformRadius"},{"file":"Main.lean","name":"Chapter3Fresh.zeroMatrix"}],"representation":"对 A 的基点半径取下确界；矩阵参数 i、j 分别为输入列和输出行。","dependencies":["CH03-D04"]},
    {"id":"CH03-D06","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.ScaleFamily"},{"file":"Main.lean","name":"Chapter3Fresh.diameter"},{"file":"Main.lean","name":"Chapter3Fresh.diameter_mono"},{"file":"Main.lean","name":"Chapter3Fresh.diameterScales"},{"file":"Main.lean","name":"Chapter3Fresh.channelType"},{"file":"Main.lean","name":"Chapter3Fresh.threshold_correspondence"}],"representation":"非空集上单调尺度、直径和两个比较构成布尔通道类型。","dependencies":["CH03-D05"]},
    {"id":"CH03-D07","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.TotallyBoundedInternal"},{"file":"Main.lean","name":"Chapter3Fresh.internalNet_text"},{"file":"formal_oet/vol_01/ch_01_foundations/metric_entropy.lean","name":"formal_oet.vol_01.ch_01_foundations.InternalEpsilonNet"},{"file":"formal_oet/vol_01/ch_01_foundations/metric_entropy.lean","name":"formal_oet.vol_01.ch_01_foundations.covering_number"},{"file":"formal_oet/vol_01/ch_01_foundations/metric_entropy.lean","name":"formal_oet.vol_01.ch_01_foundations.covering_number_attained"},{"file":"formal_oet/vol_01/ch_01_foundations/metric_entropy.lean","name":"formal_oet.vol_01.ch_01_foundations.covering_number_eq_top_iff"},{"file":"formal_oet/vol_01/ch_01_foundations/metric_entropy.lean","name":"formal_oet.vol_01.ch_01_foundations.metric_entropy"},{"file":"formal_oet/vol_01/ch_01_foundations/metric_entropy.lean","name":"formal_oet.vol_01.ch_01_foundations.subfamily_pseudometric"},{"file":"formal_oet/vol_01/ch_01_foundations/metric_entropy.lean","name":"formal_oet.vol_01.ch_01_foundations.subfamily_metric_entropy"}],"representation":"使用冻结内覆盖数、熵和子族伪度量，证明球覆盖对应并定义有限正精度下全有界接口。","dependencies":[]},
    {"id":"CH03-D08","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.entropyDomain"},{"file":"Main.lean","name":"Chapter3Fresh.entropyDifference"}],"representation":"在非空域、非空子族、有限正精度及至少一端有限覆盖数下，定义输入熵减输出熵。","dependencies":["CH03-D07"]},
    {"id":"CH03-P01-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.const_zero_row"}],"representation":"常值输出与零行有限和均为零。","dependencies":["CH03-D01"]},
    {"id":"CH03-P01-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.const_colip_zero"}],"representation":"正输入距离与常值输出迫使相应 co-Lip 条目为零。","dependencies":["CH03-D01"]},
    {"id":"CH03-P01-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.identity_preserves_distance"}],"representation":"恒等分量下像点距离等于输入距离。","dependencies":["CH03-D01"]},
    {"id":"CH03-P02-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.active_comp"}],"representation":"两步有效分量包含，外步域为实际中间像。","dependencies":["CH03-D01","CH03-P01-03","CH03-P02-03","CH03-P04-01"]},
    {"id":"CH03-P02-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.seqOp"},{"file":"Main.lean","name":"Chapter3Fresh.seqActive"},{"file":"Main.lean","name":"Chapter3Fresh.seqOp_eq_reverse_prod"},{"file":"Main.lean","name":"Chapter3Fresh.identity_not_active"},{"file":"Main.lean","name":"Chapter3Fresh.active_seq"}],"representation":"列表顺序为作用顺序，递归实际像域并含零步。","dependencies":["CH03-D01","CH03-P02-01"]},
    {"id":"CH03-P02-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.identity_comp"}],"representation":"两步恒等分量保持且排除常值优先分支。","dependencies":["CH03-D01","CH03-P01-03"]},
    {"id":"CH03-P03-01","status":"incomplete","declarations":[],"representation":"两点换位反例未交付。","dependencies":[]},
    {"id":"CH03-P04-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.outer_const"}],"representation":"外侧在内侧像上常值推出复合常值。","dependencies":["CH03-D01"]},
    {"id":"CH03-P04-02","status":"incomplete","declarations":[],"representation":"七点双分量反例未交付。","dependencies":[]},
    {"id":"CH03-P05-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.inner_const_of_single_row"}],"representation":"单同分量行 Lip 界将内侧常值传给复合，允许无穷系数。","dependencies":["CH03-D01"]},
    {"id":"CH03-P06-01","status":"incomplete","declarations":[],"representation":"目标零距时纤维相等未交付。","dependencies":[]},
    {"id":"CH03-P06-02","status":"incomplete","declarations":[],"representation":"像目标纤维非空和覆盖未交付。","dependencies":[]},
    {"id":"CH03-P06-03","status":"incomplete","declarations":[],"representation":"纤维相等或不交及分划证明未交付。","dependencies":[]},
    {"id":"CH03-P06-04","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.fiber_intersection"}],"representation":"非空输出子族纤维是单分量纤维交集。","dependencies":["CH03-D02"]},
    {"id":"CH03-P06-05","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.fiber_antitone"}],"representation":"J 包含于 K 时 K 纤维包含于 J 纤维。","dependencies":["CH03-D02"]},
    {"id":"CH03-P06-06","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.fiber_singleton"},{"file":"Main.lean","name":"Chapter3Fresh.fiber_all_subset"}],"representation":"单指标子族等于对应分量，全指标纤维包含于每个分量。","dependencies":["CH03-D02","CH03-P06-05"]},
    {"id":"CH03-P06-07","status":"incomplete","declarations":[],"representation":"恒等分量的任意目标纤维公式未交付。","dependencies":[]},
    {"id":"CH03-P06-08","status":"incomplete","declarations":[],"representation":"常值分量的两种目标纤维结论未交付。","dependencies":[]},
    {"id":"CH03-P07-01","status":"incomplete","declarations":[],"representation":"点值因子化必要性未交付。","dependencies":[]},
    {"id":"CH03-P07-02","status":"incomplete","declarations":[],"representation":"点值因子化映射构造未交付。","dependencies":[]},
    {"id":"CH03-P07-03","status":"incomplete","declarations":[],"representation":"双向点值因子化判据未交付。","dependencies":[]},
    {"id":"CH03-P07-04","status":"incomplete","declarations":[],"representation":"实际像域上的标量 Lip 界未交付。","dependencies":[]},
    {"id":"CH03-P08-01","status":"incomplete","declarations":[],"representation":"单向零距商因子化未交付。","dependencies":[]},
    {"id":"CH03-P08-02","status":"incomplete","declarations":[],"representation":"双向零距商因子化未交付。","dependencies":[]},
    {"id":"CH03-P08-03","status":"incomplete","declarations":[],"representation":"像集分离下点值与商值判据对应未交付。","dependencies":[]},
    {"id":"CH03-P09-01","status":"incomplete","declarations":[],"representation":"纤维预序的自反性和传递性未交付。","dependencies":[]},
    {"id":"CH03-P09-02","status":"incomplete","declarations":[],"representation":"有限链任意两层的包含未交付。","dependencies":[]},
    {"id":"CH03-P09-03","status":"incomplete","declarations":[],"representation":"链中真包含推出端点真包含未交付。","dependencies":[]},
    {"id":"CH03-P10-01","status":"incomplete","declarations":[],"representation":"实线阶跃反例的合法结构未交付。","dependencies":[]},
    {"id":"CH03-P10-02","status":"incomplete","declarations":[],"representation":"阶跃反例点态半径计算未交付。","dependencies":[]},
    {"id":"CH03-P10-03","status":"incomplete","declarations":[],"representation":"阶跃反例统一半径为零未交付。","dependencies":[]},
    {"id":"CH03-P11-01","status":"incomplete","declarations":[],"representation":"常值子族像目标纤维公式未交付。","dependencies":[]},
    {"id":"CH03-P11-02","status":"incomplete","declarations":[],"representation":"常值子族的无穷半径结论未交付。","dependencies":[]},
    {"id":"CH03-P11-03","status":"incomplete","declarations":[],"representation":"两种通道情形的无穷输入距离反例未交付。","dependencies":[]},
    {"id":"CH03-P12-01","status":"incomplete","declarations":[],"representation":"恒等分量像目标纤维公式未交付。","dependencies":[]},
    {"id":"CH03-P12-02","status":"incomplete","declarations":[],"representation":"恒等分量点态半径下界未交付。","dependencies":[]},
    {"id":"CH03-P13-01","status":"incomplete","declarations":[],"representation":"点态半径的有限子族最小值公式未交付。","dependencies":[]},
    {"id":"CH03-P13-02","status":"incomplete","declarations":[],"representation":"统一半径的有限子族最小值公式未交付。","dependencies":[]},
    {"id":"CH03-P13-03","status":"incomplete","declarations":[],"representation":"统一半径关于输出子族的反单调性未交付。","dependencies":[]},
    {"id":"CH03-P14-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.fiber_forces_zero"}],"representation":"纤维成员给出输出零距及对称方向。","dependencies":["CH03-D02"]},
    {"id":"CH03-P14-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.point_radius_witness"},{"file":"Main.lean","name":"Chapter3Fresh.point_radius_component"}],"representation":"严格小于上确界时提取有限正合法半径并得到输出零距。","dependencies":["CH03-D04"]},
    {"id":"CH03-P14-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.composite_fiber_forces_zero"}],"representation":"代入两个中间像点与下游纤维成员。","dependencies":["CH03-D02","CH03-P14-01"]},
    {"id":"CH03-P15-01","status":"incomplete","declarations":[],"representation":"零距保持下的复合半径下界未交付。","dependencies":[]},
    {"id":"CH03-P15-02","status":"incomplete","declarations":[],"representation":"Lip 拉回的复合半径下界未交付。","dependencies":[]},
    {"id":"CH03-P16-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.threshold_cases"},{"file":"Main.lean","name":"Chapter3Fresh.threshold_correspondence"}],"representation":"布尔对四种情况穷尽，并分别对应四组互补不等式。","dependencies":["CH03-D06"]},
    {"id":"CH03-P16-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.scale_threshold_mono"}],"representation":"增大尺度阈值保留原来小于阈值的通道。","dependencies":["CH03-D06"]},
    {"id":"CH03-P16-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.zero_threshold_mono"}],"representation":"增大零化阈值后仍达标则原阈值也达标。","dependencies":["CH03-D06"]},
    {"id":"CH03-P17-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.scale_domain_mono"}],"representation":"非空子域上的单调尺度及尺度阈值结论。","dependencies":["CH03-D06"]},
    {"id":"CH03-P17-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.radius_subset"}],"representation":"缩小评估域时每个合法半径仍合法。","dependencies":["CH03-D04"]},
    {"id":"CH03-P17-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.uniform_subset"}],"representation":"同时缩小评估域与基点集合后统一半径不减。","dependencies":["CH03-D04","CH03-D05","CH03-P17-02"]},
    {"id":"CH03-P17-04","status":"incomplete","declarations":[],"representation":"直径尺度二点单点反例未交付。","dependencies":[]},
    {"id":"CH03-P18-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.zero_of_lt_uniformRadius"}],"representation":"小于统一半径的输入点对映到零距输出。","dependencies":["CH03-D04","CH03-D05","CH03-P14-02"]},
    {"id":"CH03-P18-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.positive_output_ge_uniform"}],"representation":"输出正距离迫使输入距离不小于统一半径。","dependencies":["CH03-D04","CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P18-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.radius_deficit_witness"}],"representation":"任何有限正 α 高于统一半径时产生两点和有限正 ε，含无穷输出距离。","dependencies":["CH03-D04","CH03-D05"]},
    {"id":"CH03-P19-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.threshold_ball_fiber"}],"representation":"低于统一阈值的输入球与域交集包含在纤维中。","dependencies":["CH03-D02","CH03-D04","CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P19-02","status":"incomplete","declarations":[],"representation":"任意子集的内部覆盖数约束未交付。","dependencies":[]},
    {"id":"CH03-P19-03","status":"incomplete","declarations":[],"representation":"覆盖数约束对应的熵不等式未交付。","dependencies":[]},
    {"id":"CH03-P20-01","status":"incomplete","declarations":[],"representation":"阶跃反例上的二点覆盖构造未交付。","dependencies":[]},
    {"id":"CH03-P21-01","status":"incomplete","declarations":[],"representation":"小直径下整体零化的双向判据未交付。","dependencies":[]},
    {"id":"CH03-P21-02","status":"incomplete","declarations":[],"representation":"整体零化时输出覆盖数为一未交付。","dependencies":[]},
    {"id":"CH03-P22-01","status":"incomplete","declarations":[],"representation":"有限非空集上的熵差良定性未交付。","dependencies":[]},
    {"id":"CH03-P23-01","status":"incomplete","declarations":[],"representation":"常值分量的覆盖数、熵和熵差结论未交付。","dependencies":[]},
    {"id":"CH03-P23-02","status":"incomplete","declarations":[],"representation":"恒等分量的双向覆盖数比较未交付。","dependencies":[]},
    {"id":"CH03-P23-03","status":"incomplete","declarations":[],"representation":"恒等分量在良定条件下熵差为零未交付。","dependencies":[]},
    {"id":"CH03-P24-01","status":"incomplete","declarations":[],"representation":"Lip 输入覆盖推到输出覆盖未交付。","dependencies":[]},
    {"id":"CH03-P24-02","status":"incomplete","declarations":[],"representation":"全有界条件下的熵差下界未交付。","dependencies":[]},
    {"id":"CH03-P25-01","status":"incomplete","declarations":[],"representation":"正有限 co-Lip 条目的覆盖数下界未交付。","dependencies":[]},
    {"id":"CH03-P25-02","status":"incomplete","declarations":[],"representation":"允许输出熵无穷的熵差上界未交付。","dependencies":[]},
    {"id":"CH03-P26-01","status":"incomplete","declarations":[],"representation":"习题 3.1 的结构、一次纤维和类型未交付。","dependencies":[]},
    {"id":"CH03-P26-02","status":"incomplete","declarations":[],"representation":"习题 3.1 的自复合纤维和类型未交付。","dependencies":[]},
    {"id":"CH03-P26-03","status":"incomplete","declarations":[],"representation":"点值常算子的自复合及吸收元分支未交付。","dependencies":[]},
    {"id":"CH03-P27-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.colip_no_point_gap"}],"representation":"正 co-Lip 条目可为无穷，并排除点态半径内的正输入距离。","dependencies":["CH03-D04","CH03-P14-02"]},
    {"id":"CH03-P27-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3Fresh.colip_gap_uniform"}],"representation":"对每个输入点对，距离为零或不小于统一半径。","dependencies":["CH03-D04","CH03-D05","CH03-P14-02"]},
    {"id":"CH03-P28-01","status":"incomplete","declarations":[],"representation":"习题 3.3 的两种纤维分划和结构未交付。","dependencies":[]},
    {"id":"CH03-P28-02","status":"incomplete","declarations":[],"representation":"习题 3.3 的覆盖数和熵差未交付。","dependencies":[]},
    {"id":"CH03-P29-01","status":"incomplete","declarations":[],"representation":"习题 3.4 第一个域的直径、半径和类型未交付。","dependencies":[]},
    {"id":"CH03-P29-02","status":"incomplete","declarations":[],"representation":"习题 3.4 第二个域的直径、半径和类型未交付。","dependencies":[]},
    {"id":"CH03-P29-03","status":"incomplete","declarations":[],"representation":"习题 3.4 第三个域的直径、半径和类型未交付。","dependencies":[]},
    {"id":"CH03-P29-04","status":"incomplete","declarations":[],"representation":"习题 3.4 第四个域的直径、半径和类型未交付。","dependencies":[]},
    {"id":"CH03-P29-05","status":"incomplete","declarations":[],"representation":"习题 3.4 无直径条件的反例未交付。","dependencies":[]},
    {"id":"CH03-P30-01","status":"incomplete","declarations":[],"representation":"四点集全部精度和端点的内部覆盖数未交付。","dependencies":[]},
    {"id":"CH03-P30-02","status":"incomplete","declarations":[],"representation":"两个像集及全部精度的覆盖数和熵差未交付。","dependencies":[]},
    {"id":"CH03-P30-03","status":"incomplete","declarations":[],"representation":"两个最优标量 Lip 常数及必要下界未交付。","dependencies":[]},
    {"id":"CH03-P30-04","status":"incomplete","declarations":[],"representation":"精度 7/4 时一般覆盖界和真实值的比较未交付。","dependencies":[]}
  ]
}