{
  "case_id": "MG-C003",
  "version": "0.1.1",
  "items": [
    {
      "id": "CH03-D01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComponentPartition.lean",
          "name": "OperatorLocalDegeneracy.I_const"
        },
        {
          "file": "OperatorLocalDegeneracy/ComponentPartition.lean",
          "name": "OperatorLocalDegeneracy.I_id"
        },
        {
          "file": "OperatorLocalDegeneracy/ComponentPartition.lean",
          "name": "OperatorLocalDegeneracy.I_act"
        }
      ],
      "representation": "常值、恒等与有效分量构成的指标集分划定义",
      "dependencies": []
    },
    {
      "id": "CH03-D02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.Fib"
        }
      ],
      "representation": "算子在受限子集关于规范子族的计算纤维定义",
      "dependencies": []
    },
    {
      "id": "CH03-D03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.R_eq"
        },
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.R_zero"
        },
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.fiber_preorder"
        }
      ],
      "representation": "点对相等关系、全分量零距关系及纤维预序定义",
      "dependencies": []
    },
    {
      "id": "CH03-D04",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.r_null"
        }
      ],
      "representation": "给定输入与输出伪度量下的基点点态零化内切半径定义",
      "dependencies": []
    },
    {
      "id": "CH03-D05",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.r_null_uniform"
        },
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.nullification_matrix_entry"
        }
      ],
      "representation": "评估域上统一零化半径以及单分量通道构成的零化矩阵定义",
      "dependencies": [
        "CH03-D04"
      ]
    },
    {
      "id": "CH03-D06",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ThresholdClassification.lean",
          "name": "OperatorLocalDegeneracy.diam"
        },
        {
          "file": "OperatorLocalDegeneracy/ThresholdClassification.lean",
          "name": "OperatorLocalDegeneracy.IsMonotoneScale"
        },
        {
          "file": "OperatorLocalDegeneracy/ThresholdClassification.lean",
          "name": "OperatorLocalDegeneracy.classify_channel"
        }
      ],
      "representation": "单调输入尺度函数族与二元阈值分类定义",
      "dependencies": [
        "CH03-D05"
      ]
    },
    {
      "id": "CH03-D07",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.IsTotallyBounded"
        }
      ],
      "representation": "内部覆盖数、度量熵及全有界性接口",
      "dependencies": []
    },
    {
      "id": "CH03-D08",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.entropy_diff"
        }
      ],
      "representation": "源子集与像子集的度量熵之差（映射熵差）定义",
      "dependencies": [
        "CH03-D07"
      ]
    },
    {
      "id": "CH03-P01-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComponentPartition.lean",
          "name": "OperatorLocalDegeneracy.prop_3_1_i"
        }
      ],
      "representation": "常值分量输出距离为零且满足零行上界求和",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P01-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComponentPartition.lean",
          "name": "OperatorLocalDegeneracy.prop_3_1_ii"
        }
      ],
      "representation": "常值分量且存在正输入距离时，对应co-Lip矩阵条目必为零",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P01-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComponentPartition.lean",
          "name": "OperatorLocalDegeneracy.prop_3_1_iii"
        }
      ],
      "representation": "恒等分量在评估域内严格保持分量伪度量距离",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P02-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComponentPartition.lean",
          "name": "OperatorLocalDegeneracy.prop_3_2_i"
        }
      ],
      "representation": "两步复合算子的有效分量包含于内侧有效分量与外侧像集有效分量之并",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P02-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComponentPartition.lean",
          "name": "OperatorLocalDegeneracy.prop_3_2_ii"
        }
      ],
      "representation": "有限复合链的有效分量包含于各单步在对应中间像域上有效分量之并",
      "dependencies": [
        "CH03-D01",
        "CH03-P02-01"
      ]
    },
    {
      "id": "CH03-P02-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComponentPartition.lean",
          "name": "OperatorLocalDegeneracy.prop_3_2_iii"
        }
      ],
      "representation": "外侧与内侧恒等分量的交集保留为复合算子的恒等分量",
      "dependencies": [
        "CH03-D01",
        "CH03-P01-03"
      ]
    },
    {
      "id": "CH03-P03-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComponentPartition.lean",
          "name": "OperatorLocalDegeneracy.remark_3_2_counterexample"
        }
      ],
      "representation": "两点换位算子反例，同时否定有效分量包含与恒等分量保留的逆向包含",
      "dependencies": [
        "CH03-D01",
        "CH03-P02-01",
        "CH03-P02-03"
      ]
    },
    {
      "id": "CH03-P04-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComponentPartition.lean",
          "name": "OperatorLocalDegeneracy.prop_3_3_i"
        }
      ],
      "representation": "外侧算子在内侧像域上为常值分量则复合算子同为常值分量",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P04-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComponentPartition.lean",
          "name": "OperatorLocalDegeneracy.prop_3_3_ii_counterexample"
        }
      ],
      "representation": "七点双分量合法规范空间反例，内侧常值分量复合后不再常值",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P05-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComponentPartition.lean",
          "name": "OperatorLocalDegeneracy.cor_3_4"
        }
      ],
      "representation": "外侧具有仅含同分量Lip行时，内侧常值分量在复合中得以保持",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P06-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_5_i"
        }
      ],
      "representation": "子族零距目标点对应的计算纤维严格相等",
      "dependencies": [
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P06-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_5_ii_a"
        }
      ],
      "representation": "像目标计算纤维非空且覆盖评估域U",
      "dependencies": [
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P06-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_5_ii_b"
        }
      ],
      "representation": "像目标计算纤维两两相等或不交，去重后构成U的分划",
      "dependencies": [
        "CH03-D02",
        "CH03-P06-01"
      ]
    },
    {
      "id": "CH03-P06-04",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_5_iii"
        }
      ],
      "representation": "子族计算纤维等于其各分量单纤维之交集",
      "dependencies": [
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P06-05",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_5_iv"
        }
      ],
      "representation": "指标子族扩大时计算纤维关于集合包含反向单调",
      "dependencies": [
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P06-06",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_5_v"
        }
      ],
      "representation": "单分量纤维等式及全族计算纤维包含于任一单分量纤维",
      "dependencies": [
        "CH03-D02",
        "CH03-P06-05"
      ]
    },
    {
      "id": "CH03-P06-07",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_5_vi_a"
        }
      ],
      "representation": "恒等分量单纤维等于目标在输入域内的零距类",
      "dependencies": [
        "CH03-D01",
        "CH03-D02",
        "CH03-P06-06"
      ]
    },
    {
      "id": "CH03-P06-08",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_5_vi_b"
        }
      ],
      "representation": "常值分量在像目标的纤维为全域U，正距离目标的纤维为空集",
      "dependencies": [
        "CH03-D01",
        "CH03-D02",
        "CH03-P06-06"
      ]
    },
    {
      "id": "CH03-P07-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_6_i_nec"
        }
      ],
      "representation": "点值像因子映射存在蕴含相等点对关系包含",
      "dependencies": [
        "CH03-D03"
      ]
    },
    {
      "id": "CH03-P07-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_6_i_suff"
        }
      ],
      "representation": "由相等关系包含实际构造像因子化映射并验证复合等式",
      "dependencies": [
        "CH03-D03"
      ]
    },
    {
      "id": "CH03-P07-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_6_ii"
        }
      ],
      "representation": "双向点值像因子映射存在当且仅当相等点对关系相等",
      "dependencies": [
        "CH03-D03",
        "CH03-P07-01",
        "CH03-P07-02"
      ]
    },
    {
      "id": "CH03-P07-04",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_6_iii"
        }
      ],
      "representation": "单分量有限正KA与有限LB下，因子映射在像域满足LB/KA的Lipschitz界",
      "dependencies": [
        "CH03-D03"
      ]
    },
    {
      "id": "CH03-P08-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_7_one_way"
        }
      ],
      "representation": "零距商空间单向良定义映射存在当且仅当零距点对关系包含",
      "dependencies": [
        "CH03-D03"
      ]
    },
    {
      "id": "CH03-P08-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_7_two_way"
        }
      ],
      "representation": "零距商空间双向良定义映射存在当且仅当零距点对关系相等",
      "dependencies": [
        "CH03-D03",
        "CH03-P08-01"
      ]
    },
    {
      "id": "CH03-P08-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_7_separating"
        }
      ],
      "representation": "规范族在实际像集上分离时，零距关系与相等关系重合，商判据转回点值判据",
      "dependencies": [
        "CH03-D03"
      ]
    },
    {
      "id": "CH03-P09-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_9_refl_trans"
        }
      ],
      "representation": "固定公共评估域上的纤维预序满足自反性与传递性",
      "dependencies": [
        "CH03-D03"
      ]
    },
    {
      "id": "CH03-P09-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_9_chain"
        }
      ],
      "representation": "有限算子链各相邻步单调纤维预序推出任意两层间的包含关系",
      "dependencies": [
        "CH03-D03",
        "CH03-P09-01"
      ]
    },
    {
      "id": "CH03-P09-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ComputationalFibers.lean",
          "name": "OperatorLocalDegeneracy.prop_3_9_strict"
        }
      ],
      "representation": "算子链中任一步严格包含推出端点严格包含，并给出差集见证点",
      "dependencies": [
        "CH03-D03",
        "CH03-P09-01"
      ]
    },
    {
      "id": "CH03-P10-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.step_op"
        }
      ],
      "representation": "带吸收元的实直线上阶跃算子与去心区间合法域构造",
      "dependencies": [
        "CH03-D04",
        "CH03-D05"
      ]
    },
    {
      "id": "CH03-P10-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.step_op_pointwise_pos"
        }
      ],
      "representation": "阶跃算子在评估域上每个基点的合法正半径恰为(0,|y|]，点态零化半径恒正",
      "dependencies": [
        "CH03-D04",
        "CH03-P10-01"
      ]
    },
    {
      "id": "CH03-P10-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.prop_3_16_counterexample"
        }
      ],
      "representation": "阶跃算子在固定评估域上的统一零化半径为0",
      "dependencies": [
        "CH03-D05",
        "CH03-P10-01"
      ]
    },
    {
      "id": "CH03-P11-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_8_i_a"
        }
      ],
      "representation": "输出子族常值时，像目标对应的子族计算纤维恒等于全域U",
      "dependencies": [
        "CH03-D01",
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P11-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_8_i_b_ptwise"
        },
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_8_i_b_uniform"
        }
      ],
      "representation": "输出子族常值时，任意输入分量的点态与统一零化半径均为正无穷",
      "dependencies": [
        "CH03-D01",
        "CH03-D04",
        "CH03-D05"
      ]
    },
    {
      "id": "CH03-P11-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_8_ii_counterexample"
        }
      ],
      "representation": "恒等算子与无穷输入距离两点反例，统一零化半径为无穷但不属于常值分量",
      "dependencies": [
        "CH03-D01",
        "CH03-D05"
      ]
    },
    {
      "id": "CH03-P12-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_9_i"
        }
      ],
      "representation": "恒等分量像目标计算纤维等于输入域内的零距类",
      "dependencies": [
        "CH03-D01",
        "CH03-D02",
        "CH03-P06-07"
      ]
    },
    {
      "id": "CH03-P12-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_9_ii"
        }
      ],
      "representation": "恒等分量在开球仅含输入零距点时，点态零化半径不小于球半径r0",
      "dependencies": [
        "CH03-D01",
        "CH03-D04"
      ]
    },
    {
      "id": "CH03-P13-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_10_01"
        }
      ],
      "representation": "有限非空输出子族对应的点态零化半径等于单分量点态半径之最小值",
      "dependencies": [
        "CH03-D04",
        "CH03-P06-04"
      ]
    },
    {
      "id": "CH03-P13-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_10_02"
        }
      ],
      "representation": "交换基点下确界与有限最小值，得到子族统一零化半径的矩阵行极小值公式",
      "dependencies": [
        "CH03-D05",
        "CH03-P13-01"
      ]
    },
    {
      "id": "CH03-P13-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_10_03"
        }
      ],
      "representation": "目标子族包含J⊆K时，统一零化半径关于子族集合包含反向单调",
      "dependencies": [
        "CH03-D05"
      ]
    },
    {
      "id": "CH03-P14-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_11_fiber_zero"
        }
      ],
      "representation": "计算纤维成员条件推出输出分量零距",
      "dependencies": [
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P14-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_11_lt_sSup"
        }
      ],
      "representation": "输入距离严格小于点态零化半径时推出输出分量零距",
      "dependencies": [
        "CH03-D04"
      ]
    },
    {
      "id": "CH03-P14-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_11_compose_inst"
        }
      ],
      "representation": "复合算子下游纤维截断单步判据实例",
      "dependencies": [
        "CH03-D02",
        "CH03-P14-01"
      ]
    },
    {
      "id": "CH03-P15-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_12_i"
        }
      ],
      "representation": "下游在实际像集上保持零距时，全复合统一零化半径的下界传递",
      "dependencies": [
        "CH03-D05",
        "CH03-P14-02"
      ]
    },
    {
      "id": "CH03-P15-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_12_ii"
        }
      ],
      "representation": "经正有限Lipschitz界拉回时，下游统一零化半径除以L作为全复合统一半径下界",
      "dependencies": [
        "CH03-D05",
        "CH03-P14-02"
      ]
    },
    {
      "id": "CH03-P16-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ThresholdClassification.lean",
          "name": "OperatorLocalDegeneracy.lemma_3_13_exhaustive"
        },
        {
          "file": "OperatorLocalDegeneracy/ThresholdClassification.lean",
          "name": "OperatorLocalDegeneracy.lemma_3_13_exclusive"
        }
      ],
      "representation": "四种阈值分类状态互斥且穷尽",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P16-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ThresholdClassification.lean",
          "name": "OperatorLocalDegeneracy.lemma_3_13_i"
        }
      ],
      "representation": "输入尺度阈值增大时，第一项为1的通道集合单调不减",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P16-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ThresholdClassification.lean",
          "name": "OperatorLocalDegeneracy.lemma_3_13_ii"
        }
      ],
      "representation": "零化阈值增大时，第二项为1的通道集合单调不增",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P17-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ThresholdClassification.lean",
          "name": "OperatorLocalDegeneracy.prop_3_14_i"
        }
      ],
      "representation": "评估域缩小下单调尺度函数的取值单调不增及阈值推论",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P17-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ThresholdClassification.lean",
          "name": "OperatorLocalDegeneracy.prop_3_14_ii_a"
        }
      ],
      "representation": "固定基点属于缩小域时，评估域缩小使点态零化半径单调不减",
      "dependencies": [
        "CH03-D04"
      ]
    },
    {
      "id": "CH03-P17-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ThresholdClassification.lean",
          "name": "OperatorLocalDegeneracy.prop_3_14_ii_b"
        }
      ],
      "representation": "同时缩小评估域与取下确界基点集，统一零化半径单调不减",
      "dependencies": [
        "CH03-D05",
        "CH03-P17-02"
      ]
    },
    {
      "id": "CH03-P17-04",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/ThresholdClassification.lean",
          "name": "OperatorLocalDegeneracy.prop_3_17_counterexample"
        }
      ],
      "representation": "两点与单点评估域直径尺度反例，否定反向尺度判断",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P18-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_15_i"
        }
      ],
      "representation": "输入距离严格低于统一零化半径时，输出分量必然零距",
      "dependencies": [
        "CH03-D05",
        "CH03-P14-02"
      ]
    },
    {
      "id": "CH03-P18-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_15_ii"
        }
      ],
      "representation": "输出分量正分离推出输入距离不小于统一零化半径",
      "dependencies": [
        "CH03-D05",
        "CH03-P18-01"
      ]
    },
    {
      "id": "CH03-P18-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_15_iii"
        }
      ],
      "representation": "统一零化半径低于阈值时，对介于二者间的α提取正分离点对见证",
      "dependencies": [
        "CH03-D05"
      ]
    },
    {
      "id": "CH03-P19-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.prop_3_16_i"
        }
      ],
      "representation": "统一零化半径达到阈值时，开球全包含于计算纤维",
      "dependencies": [
        "CH03-D02",
        "CH03-D05",
        "CH03-P18-01"
      ]
    },
    {
      "id": "CH03-P19-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.prop_3_16_ii_a"
        }
      ],
      "representation": "统一零化半径达阈值时，输出ε覆盖数受控于输入τ_N内覆盖数",
      "dependencies": [
        "CH03-D07",
        "CH03-P19-01"
      ]
    },
    {
      "id": "CH03-P19-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.prop_3_16_ii_b"
        }
      ],
      "representation": "非空子集覆盖数单调性推出度量熵不等式",
      "dependencies": [
        "CH03-D07",
        "CH03-P19-02"
      ]
    },
    {
      "id": "CH03-P20-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.prop_3_16_counterexample"
        }
      ],
      "representation": "阶跃算子反例：点态正半径无法给出全局覆盖数控制",
      "dependencies": [
        "CH03-D07",
        "CH03-P10-02",
        "CH03-P10-03"
      ]
    },
    {
      "id": "CH03-P21-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.cor_3_17_i"
        }
      ],
      "representation": "小输入域上统一零化半径达阈值当且仅当全域像两两零距",
      "dependencies": [
        "CH03-D05",
        "CH03-P18-01"
      ]
    },
    {
      "id": "CH03-P21-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.cor_3_17_ii"
        }
      ],
      "representation": "整体零化等价条件成立时，输出内部覆盖数严格等于1",
      "dependencies": [
        "CH03-D07",
        "CH03-P21-01"
      ]
    },
    {
      "id": "CH03-P22-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.remark_entropy_diff_well_defined"
        }
      ],
      "representation": "非空有限集上输入与输出覆盖熵均为有限实数，映射熵差良定",
      "dependencies": [
        "CH03-D07",
        "CH03-D08"
      ]
    },
    {
      "id": "CH03-P23-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.prop_3_18_i"
        }
      ],
      "representation": "常值分量输出覆盖数为1、熵为0、映射熵差严格等于输入熵",
      "dependencies": [
        "CH03-D01",
        "CH03-D08",
        "CH03-P21-02"
      ]
    },
    {
      "id": "CH03-P23-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.prop_3_18_ii_a"
        }
      ],
      "representation": "恒等分量保持内部覆盖数与度量熵",
      "dependencies": [
        "CH03-D01",
        "CH03-D07",
        "CH03-P01-03"
      ]
    },
    {
      "id": "CH03-P23-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.prop_3_18_ii_b"
        }
      ],
      "representation": "恒等分量在熵差良定时严格等于0",
      "dependencies": [
        "CH03-D08",
        "CH03-P23-02"
      ]
    },
    {
      "id": "CH03-P24-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.prop_3_19_i"
        }
      ],
      "representation": "有限正Lipschitz常数L将ε/L内覆盖中心推到ε像覆盖，覆盖数单调不增",
      "dependencies": [
        "CH03-D07"
      ]
    },
    {
      "id": "CH03-P24-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.prop_3_19_ii"
        }
      ],
      "representation": "输入域全有界时，映射熵差满足由L放缩给出的下界",
      "dependencies": [
        "CH03-D08",
        "CH03-P24-01"
      ]
    },
    {
      "id": "CH03-P25-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.prop_3_20_i"
        }
      ],
      "representation": "有限正co-Lipschitz条目将输出中心原像拉回为ε/K覆盖，给出覆盖数下界",
      "dependencies": [
        "CH03-D07"
      ]
    },
    {
      "id": "CH03-P25-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/CoveringEntropy.lean",
          "name": "OperatorLocalDegeneracy.prop_3_20_ii"
        }
      ],
      "representation": "输入域全有界时，映射熵差满足由co-Lip系数给出的上界",
      "dependencies": [
        "CH03-D08",
        "CH03-P25-01"
      ]
    },
    {
      "id": "CH03-P26-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex_3_1_i_a_extended"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex_3_1_i_a_fiber"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex_3_1_i_a_const"
        }
      ],
      "representation": "习题 3.1 (i-a) 绝对值读数伪度量合法性、算子单步计算纤维与常值分量判定",
      "dependencies": [
        "CH03-D01",
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P26-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex_3_1_i_b_fiber"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex_3_1_i_b_act"
        }
      ],
      "representation": "习题 3.1 (i-b) 自复合计算纤维收缩为单点及有效分量判定",
      "dependencies": [
        "CH03-D01",
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P26-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex_3_1_ii"
        }
      ],
      "representation": "习题 3.1 (ii) 域上常值算子自复合后计算纤维仍无法区分两点",
      "dependencies": [
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P27-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.ex_3_2_i"
        }
      ],
      "representation": "习题 3.2 (i) 正co-Lip通道与点态零化判据排除开区间(0,rN)内的一切输入距离",
      "dependencies": [
        "CH03-D04",
        "CH03-P14-02"
      ]
    },
    {
      "id": "CH03-P27-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/NullificationRadius.lean",
          "name": "OperatorLocalDegeneracy.ex_3_2_ii"
        }
      ],
      "representation": "习题 3.2 (ii) 正co-Lip下输入距离必为零或不小于统一零化半径",
      "dependencies": [
        "CH03-D05",
        "CH03-P27-01"
      ]
    },
    {
      "id": "CH03-P28-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex_3_3_i_id_fiber"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex_3_3_i_trans_fiber"
        }
      ],
      "representation": "习题 3.3 (i) 四点集上恒等算子与平移算子的计算纤维分划",
      "dependencies": [
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P28-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex_3_3_cov_U"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex_3_3_cov_phi_U"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex_3_3_entropy_diff"
        }
      ],
      "representation": "习题 3.3 (ii) 在ε=3/2下精确计算输入与像集覆盖数及映射熵差",
      "dependencies": [
        "CH03-D07",
        "CH03-D08"
      ]
    },
    {
      "id": "CH03-P29-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.diam_Da"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.r_null_unif_Da"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.type_Da"
        }
      ],
      "representation": "习题 3.4 (i-a) Da=[0,1/2]的直径、统一零化半径与(1,1)分类",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P29-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.diam_Db"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.r_null_unif_Db"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.type_Db"
        }
      ],
      "representation": "习题 3.4 (i-b) Db=[9/10,11/10]的直径、统一零化半径与(1,0)分类",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P29-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.diam_Dc"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.r_null_unif_Dc"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.type_Dc"
        }
      ],
      "representation": "习题 3.4 (i-c) Dc={0,2}的直径、统一零化半径与(0,1)分类",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P29-04",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.diam_Dd"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.r_null_unif_Dd"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.type_Dd"
        }
      ],
      "representation": "习题 3.4 (i-d) Dd=[0,2]的直径、统一零化半径与(0,0)分类",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P29-05",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex_3_4_ii_counterexample"
        }
      ],
      "representation": "习题 3.4 (ii) 利用Dc反例否定无直径条件下统一半径≥1即整体零化",
      "dependencies": [
        "CH03-D05",
        "CH03-P29-03"
      ]
    },
    {
      "id": "CH03-P30-01",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_cov_gt_2"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_cov_1_to_2"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_cov_le_1"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_center_3_2_not_in_U"
        }
      ],
      "representation": "习题 3.5 (i) 四点集内部覆盖数完整分段，说明3/2非内部中心",
      "dependencies": [
        "CH03-D07"
      ]
    },
    {
      "id": "CH03-P30-02",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_f_image"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_g_image"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_cov_f_image"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_cov_g_image"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_entropy_diff_f"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_entropy_diff_g"
        }
      ],
      "representation": "习题 3.5 (ii) 算子f与g的像集、覆盖数及映射熵差为0",
      "dependencies": [
        "CH03-D07",
        "CH03-D08",
        "CH03-P30-01"
      ]
    },
    {
      "id": "CH03-P30-03",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_f_lip"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_f_lip_lower"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_g_lip"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_g_lip_lower"
        }
      ],
      "representation": "习题 3.5 (iii-a) 算子f的最优标量Lipschitz界为1，g的最优标量Lipschitz界为2",
      "dependencies": []
    },
    {
      "id": "CH03-P30-04",
      "status": "complete",
      "declarations": [
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_cov_at_7_4"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_bound_f_at_7_4"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_bound_g_at_7_4"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_compare_f"
        },
        {
          "file": "OperatorLocalDegeneracy/Exercises.lean",
          "name": "OperatorLocalDegeneracy.ex35_compare_g"
        }
      ],
      "representation": "习题 3.5 (iii-b) 在ε=7/4下应用一般上界并与真实覆盖数进行比较（f取等，g严格小于）",
      "dependencies": [
        "CH03-P24-01",
        "CH03-P30-01",
        "CH03-P30-02",
        "CH03-P30-03"
      ]
    }
  ]
}