{
  "case_id": "MG-C003",
  "version": "0.1.1",
  "items": [
    {"id":"CH03-D01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Const"},{"file":"Main.lean","name":"MG.Ident"},{"file":"Main.lean","name":"MG.Active"},{"file":"Main.lean","name":"MG.component_partition"}],"representation":"以任意函数推广算子作用；代入Operator.func及U⊆dom即为正文。Ident显式排除Const，证明三集合覆盖且两两不交。","dependencies":[]},
    {"id":"CH03-D02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Fiber"},{"file":"Main.lean","name":"MG.fiber_representation"},{"file":"Main.lean","name":"MG.subfamily_zero"}],"representation":"Fiber使用各j∈J输出零距的合取；证明与冻结d_J上确界的零距定义相等，任意目标及空纤维均保留。","dependencies":[]},
    {"id":"CH03-D03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.EqRel"},{"file":"Main.lean","name":"MG.ZeroRel"},{"file":"Main.lean","name":"MG.imageSetoid"},{"file":"Main.lean","name":"MG.ImageQuotient"},{"file":"Main.lean","name":"MG.FiberLE"},{"file":"Main.lean","name":"MG.relation_fiber"}],"representation":"点对集包含两点属于U；像商是实际像集子类型上的Quotient，零距等价性由规范公理证明；预序为零距点对集包含。","dependencies":["CH03-D02"]},
    {"id":"CH03-D04","status":"complete","declarations":[{"file":"Main.lean","name":"MG.radius"},{"file":"Main.lean","name":"MG.LegalRadius"},{"file":"Main.lean","name":"MG.radius_sup"},{"file":"Main.lean","name":"MG.legal_ball"}],"representation":"先取输出非零距输入点的输入距离下确界，再证明恰等于全部有限正合法开球半径的上确界；空上确界为0，无上界可为top。","dependencies":[]},
    {"id":"CH03-D05","status":"complete","declarations":[{"file":"Main.lean","name":"MG.uniform"},{"file":"Main.lean","name":"MG.nullMatrix"}],"representation":"uniform对A中的基点取点态半径下确界，U独立指定评估域；nullMatrix的参数顺序为输出行j、输入列i。","dependencies":["CH03-D04"]},
    {"id":"CH03-D06","status":"complete","declarations":[{"file":"Main.lean","name":"MG.InputScale"},{"file":"Main.lean","name":"MG.scaleFromNonempty"},{"file":"Main.lean","name":"MG.scaleFromNonempty_eq"},{"file":"Main.lean","name":"MG.diameter"},{"file":"Main.lean","name":"MG.diameterScale"},{"file":"Main.lean","name":"MG.threshold"},{"file":"Main.lean","name":"MG.channelType"},{"file":"Main.lean","name":"MG.threshold_cases"}],"representation":"尺度在非空集合上的单调性为数据条件；给出从原文非空集合子类型到本表示的扩展及对应等式；Bool对表示两项0/1指标。","dependencies":["CH03-D05"]},
    {"id":"CH03-D07","status":"complete","declarations":[{"file":"Main.lean","name":"MG.TotallyBounded"},{"file":"Main.lean","name":"MG.internal_ball_iff"},{"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_metric_entropy"}],"representation":"直接采用冻结内部覆盖数和以2为底的EReal熵；internal_ball_iff证明有限内网等于内部开球覆盖，全有界量化所有有限正半径。","dependencies":[]},
    {"id":"CH03-D08","status":"complete","declarations":[{"file":"Main.lean","name":"MG.DeltaDefined"},{"file":"Main.lean","name":"MG.delta"},{"file":"Main.lean","name":"MG.subfamilyDelta"},{"file":"Main.lean","name":"MG.subfamilyDelta_eq"},{"file":"Main.lean","name":"MG.entropy_top_iff"},{"file":"Main.lean","name":"MG.delta_infinite_input"},{"file":"Main.lean","name":"MG.delta_infinite_output"}],"representation":"熵差要求至少一端覆盖数有限的证明参数；子族表示等于原文两熵相减，并证明单端无穷时分别为正、负无穷。","dependencies":["CH03-D07","CH03-P22-01"]},
    {"id":"CH03-P01-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.const_zero_row"}],"representation":"常值输出为0，任意有限指标集的零行求和为0。","dependencies":["CH03-D01"]},
    {"id":"CH03-P01-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.const_colip"}],"representation":"在U中的正输入距离见证上应用冻结co-Lip单条目零值引理，系数允许无穷。","dependencies":["CH03-D01"]},
    {"id":"CH03-P01-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.ident_isometry"},{"file":"Main.lean","name":"MG.zero_transport"}],"representation":"由输出与输入逐点零距和双向三角不等式证明每个点对距离相等。","dependencies":["CH03-D01"]},
    {"id":"CH03-P02-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.active_comp"}],"representation":"两步复合的有效集合包含于内步U及外步f(U)的有效集合之并；逐一处理常值/恒等分支。","dependencies":["CH03-D01","CH03-P01-03","CH03-P02-03","CH03-P04-01"]},
    {"id":"CH03-P02-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.run"},{"file":"Main.lean","name":"MG.stepActive"},{"file":"Main.lean","name":"MG.LegalChain"},{"file":"Main.lean","name":"MG.chain_domains"},{"file":"Main.lean","name":"MG.active_chain"}],"representation":"列表按实际执行顺序表示任意有限链；递归像域，证明全部中间域合法以及有效集合包含，空列表是恒等且有效集合为空。","dependencies":["CH03-D01","CH03-P02-01"]},
    {"id":"CH03-P02-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.ident_comp"}],"representation":"输出到输入的零距由传递性得到，借外侧保距排除复合常值，保留常值优先规则。","dependencies":["CH03-D01","CH03-P01-03"]},
    {"id":"CH03-P03-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Swap.legal"},{"file":"Main.lean","name":"MG.Swap.data"},{"file":"Main.lean","name":"MG.Swap.reverse_inclusions_fail"}],"representation":"Option Bool编码bot,a,b；合法离散扩展距离、两步换位及像域U，完整计算分量集合并证明两条反向包含均失败。","dependencies":["CH03-D01"]},
    {"id":"CH03-P04-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.outer_const"}],"representation":"对两个U中输入，外侧常值条件直接用于实际像域中的像点。","dependencies":["CH03-D01"]},
    {"id":"CH03-P04-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Seven.legal"},{"file":"Main.lean","name":"MG.Seven.data"}],"representation":"Option(Fin 6)编码七点；false分量只合并p=2,q=3，true为离散分量，验证复合域、内侧常值、复合非恒零及另一分量可区分。","dependencies":["CH03-D01"]},
    {"id":"CH03-P05-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.inner_const_lip"}],"representation":"实际像域上的Lip矩阵指定行仅含对角输入；通过冻结单行化简及ENNReal乘零，允许无限系数。","dependencies":["CH03-D01"]},
    {"id":"CH03-P06-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.fiber_target"},{"file":"Main.lean","name":"MG.subfamily_zero"}],"representation":"任意目标在d_J下零距等价于全部J分量零距，双向传递得到纤维相等。","dependencies":["CH03-D02"]},
    {"id":"CH03-P06-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.fiber_nonempty"},{"file":"Main.lean","name":"MG.fiber_cover"}],"representation":"像点作为目标的纤维含相应原像，全部这些纤维之并恰为U，包括U空集。","dependencies":["CH03-D02"]},
    {"id":"CH03-P06-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.fiber_equal_or_disjoint"},{"file":"Main.lean","name":"MG.fiber_nonempty"},{"file":"Main.lean","name":"MG.fiber_cover"}],"representation":"交点使两个目标在J中零距，故相等，否则不交；加上非空与覆盖构成去重后的分划。","dependencies":["CH03-D02","CH03-P06-01"]},
    {"id":"CH03-P06-04","status":"complete","declarations":[{"file":"Main.lean","name":"MG.fiber_inter"}],"representation":"J非空保证交集中仍包含U条件，得到单分量纤维交集等式；适用于有限非空子族。","dependencies":["CH03-D02"]},
    {"id":"CH03-P06-05","status":"complete","declarations":[{"file":"Main.lean","name":"MG.fiber_antitone"}],"representation":"从K中的各分量零距限制到J⊆K，得到反向纤维包含。","dependencies":["CH03-D02"]},
    {"id":"CH03-P06-06","status":"complete","declarations":[{"file":"Main.lean","name":"MG.fiber_singleton"},{"file":"Main.lean","name":"MG.fiber_full"}],"representation":"证明singleton子族的原始距离集合公式及全子族向每个单分量的包含。","dependencies":["CH03-D02","CH03-P06-05"]},
    {"id":"CH03-P06-07","status":"complete","declarations":[{"file":"Main.lean","name":"MG.fiber_ident"}],"representation":"对任意目标，用恒等分量的逐点零距证明输出零距等价于输入零距。","dependencies":["CH03-D01","CH03-D02","CH03-P01-03","CH03-P06-06"]},
    {"id":"CH03-P06-08","status":"complete","declarations":[{"file":"Main.lean","name":"MG.fiber_const"}],"representation":"像目标的纤维为U；距该目标严格为正的任意目标纤维为空，涵盖无限正距离。","dependencies":["CH03-D01","CH03-D02","CH03-P06-06"]},
    {"id":"CH03-P07-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.factors_iff"}],"representation":"Factors是实际像子类型到X的函数满足规定赋值；必要性由同一函数保相等得到。","dependencies":["CH03-D03","CH03-P07-02"]},
    {"id":"CH03-P07-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.factor_surjective"},{"file":"Main.lean","name":"MG.imageMap"},{"file":"Main.lean","name":"MG.imageMap_surjective"},{"file":"Main.lean","name":"MG.factors_iff"}],"representation":"从像映射的满射性选择原像，关系包含保证赋值与代表元无关；无Nonempty U假设，空像也构造函数。","dependencies":["CH03-D03"]},
    {"id":"CH03-P07-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.factors_both"}],"representation":"两个方向分别应用构造判据，再用集合反对称性得到关系相等充要条件。","dependencies":["CH03-D03","CH03-P07-01","CH03-P07-02"]},
    {"id":"CH03-P07-04","status":"complete","declarations":[{"file":"Main.lean","name":"MG.factor_lip"}],"representation":"T取实际像子类型为定义域，任取两像点选原像；正有限K可除，有限非负L给出L/K的像域Lip界。","dependencies":["CH03-P07-02"]},
    {"id":"CH03-P08-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.quotientMap"},{"file":"Main.lean","name":"MG.quotientMap_surjective"},{"file":"Main.lean","name":"MG.quotient_factors_iff"}],"representation":"在实际像零距商中构造满射并应用选代表元的因子化；Quotient.sound/exact证明规定赋值与关系包含的双向等价。","dependencies":["CH03-D03","CH03-P07-02"]},
    {"id":"CH03-P08-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.quotient_factors_both"}],"representation":"双向商映射的规定公式存在当且仅当两个零距点对集相等。","dependencies":["CH03-D03","CH03-P08-01"]},
    {"id":"CH03-P08-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.separated_relations"},{"file":"Main.lean","name":"MG.separated_criteria"}],"representation":"只要求f(U)、g(U)各自在规范族中分离；证明各自点值关系等于零距关系以及单、双向判据一致。","dependencies":["CH03-D03","CH03-P07-01","CH03-P07-02","CH03-P07-03","CH03-P08-01","CH03-P08-02"]},
    {"id":"CH03-P09-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.fiberLE_refl"},{"file":"Main.lean","name":"MG.fiberLE_trans"}],"representation":"固定同一U，零距点对集包含的自反性与传递性。","dependencies":["CH03-D03"]},
    {"id":"CH03-P09-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.relation_chain"}],"representation":"对任意有限长度m及0≤a≤b≤m证明逐步集合包含传至R_a⊆R_b；取R_k=ZeroRel即原文。","dependencies":[]},
    {"id":"CH03-P09-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.relation_chain_strict"}],"representation":"任一步严格包含的差集点传至R_m\\R_0，同时证明端点严格包含；有限链长度和步号均量化。","dependencies":["CH03-P09-02"]},
    {"id":"CH03-P10-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Step.f"},{"file":"Main.lean","name":"MG.Step.U"},{"file":"Main.lean","name":"MG.Step.legal"},{"file":"Main.lean","name":"MG.Step.domain"}],"representation":"Option ℝ表示带吸收元实线；阶跃函数保持none，证明U等于原文两个半开区间的像、非空且属于定义域。","dependencies":["CH03-P17-04"]},
    {"id":"CH03-P10-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Step.point"},{"file":"Main.lean","name":"MG.Step.legal_radii"}],"representation":"对同一U每个some y，证明半径=ofReal|y|且正，合法有限正r恰满足r≤|y|；上界用异号且接近零的显式点。","dependencies":["CH03-D04","CH03-P10-01","CH03-P14-02"]},
    {"id":"CH03-P10-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Step.uniform_zero"}],"representation":"选择min(1,r/2)的趋零正基点，利用点态半径公式证明固定U上的下确界为0。","dependencies":["CH03-D04","CH03-D05","CH03-P10-01","CH03-P10-02","CH03-P18-01"]},
    {"id":"CH03-P11-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.fiber_const_family"}],"representation":"J中每个输出分量常值时，对每个y∈U证明以f(y)为目标的J纤维等于U。","dependencies":["CH03-D01","CH03-D02"]},
    {"id":"CH03-P11-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.const_family_radius"},{"file":"Main.lean","name":"MG.radius_top"},{"file":"Main.lean","name":"MG.uniform_top"}],"representation":"全部输出零距使所有有限正半径合法；任意输入分量的每点半径和统一半径均为top。","dependencies":["CH03-D01","CH03-D02","CH03-D04","CH03-D05"]},
    {"id":"CH03-P11-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Infinite.legal"},{"file":"Main.lean","name":"MG.Infinite.data"}],"representation":"合法Option Bool两点域：输入false分量距离top，输出j=false或true分别覆盖i=j与i≠j；恒等算子统一半径top而非常值。","dependencies":["CH03-D01","CH03-D04","CH03-D05"]},
    {"id":"CH03-P12-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.fiber_ident_image"}],"representation":"恒等分量保距给出像目标纤维正是基点的输入零距类。","dependencies":["CH03-D01","CH03-D02","CH03-P01-03","CH03-P06-06"]},
    {"id":"CH03-P12-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.ident_radius_lower"}],"representation":"原文有限正r及受限球包含输入零距类，结合保距，证明r≤点态零化半径并保留r>0。","dependencies":["CH03-D01","CH03-D04","CH03-P01-03"]},
    {"id":"CH03-P13-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.radius_family"},{"file":"Main.lean","name":"MG.finite_inf_min"}],"representation":"证明子族点态半径等于各单分量半径的下确界，有限非空J上该值由某个分量取得，因此是最小值。","dependencies":["CH03-D02","CH03-D04","CH03-P14-02"]},
    {"id":"CH03-P13-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.uniform_family"},{"file":"Main.lean","name":"MG.finite_inf_min"},{"file":"Main.lean","name":"MG.nullMatrix"}],"representation":"证明基点与输出子族两重下确界可交换，并用有限非空最小值的取得性对应零化矩阵指定列的最小条目。","dependencies":["CH03-D02","CH03-D04","CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P13-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.uniform_family_antitone"}],"representation":"由统一子族公式，对更大输出指标集取下确界不会增大。","dependencies":["CH03-D05","CH03-P13-02"]},
    {"id":"CH03-P14-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.fiber_truncation"}],"representation":"纤维成员的输出反向零距经对称性得到所需顺序的输出零距。","dependencies":["CH03-D02","CH03-D04","CH03-P14-02"]},
    {"id":"CH03-P14-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.extract_legal_radius"},{"file":"Main.lean","name":"MG.radius_zero"},{"file":"Main.lean","name":"MG.fiber_truncation"}],"representation":"严格小于点态半径时选取夹在其间的有限NNReal半径，验证合法，再由球包含及输入/输出对称性得到零距。","dependencies":["CH03-D02","CH03-D04"]},
    {"id":"CH03-P14-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.composite_truncation"}],"representation":"保留上游定义域及两像点属于指定下游U的条件，在复合算子中代入单分量纤维判据。","dependencies":["CH03-D02"]},
    {"id":"CH03-P15-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.uniform_comp_zero"}],"representation":"下游零距保持只量化实际像f(U)，统一半径以下的上游零距传至复合，得到原文下界。","dependencies":["CH03-D04","CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P15-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.uniform_comp_lip"}],"representation":"正有限ENNReal L下直接证明所有严格低于下游统一半径/L的输入对零化；0与top右端由同一有序代数证明涵盖。","dependencies":["CH03-D04","CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P16-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.threshold_cases"},{"file":"Main.lean","name":"MG.threshold_exhaustive"}],"representation":"给出Bool×Bool四个值与原文四组互补不等式的充要条件及分类值唯一性。","dependencies":["CH03-D06"]},
    {"id":"CH03-P16-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.scale_threshold_mono"}],"representation":"对所有s及τ≤τ′证明s<τ推出s<τ′，逐通道给出第一项为1的集合单调不减。","dependencies":[]},
    {"id":"CH03-P16-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.null_threshold_antitone"}],"representation":"对所有r及τ≤τ′证明τ′≤r推出τ≤r，逐通道给出第二项为1的集合单调不增。","dependencies":[]},
    {"id":"CH03-P17-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.scale_restrict"}],"representation":"任意输入尺度族，在非空B⊆A时尺度不增并传递严格阈值判断。","dependencies":["CH03-D06"]},
    {"id":"CH03-P17-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.radius_restrict"}],"representation":"固定任意基点，A上每个零化输入球在B⊆A上仍零化，证明点态半径不减；特别涵盖基点在B。","dependencies":["CH03-D04","CH03-P14-02"]},
    {"id":"CH03-P17-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.uniform_restrict"}],"representation":"同时缩小评估域及基点集合，由严格阈值的零距刻画证明统一半径不减。","dependencies":["CH03-D04","CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P17-04","status":"complete","declarations":[{"file":"Main.lean","name":"MG.realD_legal"},{"file":"Main.lean","name":"MG.scale_reverse_counterexample"},{"file":"Main.lean","name":"MG.scale_reverse_domain"}],"representation":"合法带吸收元实线上，B={0}⊆A={0,1}的直径分别为0、1，阈值1/2否定反向判断；恒等算子的作用不影响该尺度计算。","dependencies":["CH03-D06"]},
    {"id":"CH03-P18-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.uniform_zero"},{"file":"Main.lean","name":"MG.uniform_le_point"}],"representation":"统一下确界不超过指定基点半径，因此严格低于统一半径的输入距离对应输出零距。","dependencies":["CH03-D04","CH03-D05","CH03-P14-02"]},
    {"id":"CH03-P18-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.separation_lower"}],"representation":"输出严格正距离与零距结论矛盾，推出输入距离至少为统一半径。","dependencies":["CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P18-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.separation_witness"}],"representation":"每个α大于统一半径即存在违反零距球条件的两点，再在0与正输出距离间选有限NNReal ε，涵盖输出top。","dependencies":["CH03-D04","CH03-D05"]},
    {"id":"CH03-P19-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.threshold_fiber"}],"representation":"对y∈A及半径τ≤统一半径，严格输入球与A的交集逐点属于以f(y)为目标的单分量纤维。","dependencies":["CH03-D02","CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P19-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.net_push"},{"file":"Main.lean","name":"MG.cover_push"},{"file":"Main.lean","name":"MG.threshold_cover"}],"representation":"任意B⊆A的有限内部中心S推至f(S)，证明合法输出内覆盖及card不增，取下确界统一包含B空集和无有限输入覆盖。","dependencies":["CH03-D05","CH03-D07","CH03-P18-01"]},
    {"id":"CH03-P19-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.log_mono"},{"file":"Main.lean","name":"MG.entropy_mono"},{"file":"Main.lean","name":"MG.threshold_entropy"}],"representation":"证明扩展log2单调，由阈值覆盖数不等式推出原文熵不等式，特别适用于非空B。","dependencies":["CH03-D05","CH03-D07","CH03-P19-02"]},
    {"id":"CH03-P20-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Step.cover_counterexample"}],"representation":"对每个正有限τ显式选择a=min(1,r/4)，同一阶跃U内B={-a,a}满足2a<τ；内部输入覆盖数恰1，输出在1/2处恰2。","dependencies":["CH03-D07","CH03-P10-01","CH03-P17-04"]},
    {"id":"CH03-P21-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.small_domain_iff"}],"representation":"精确使用diam(A)<τs≤τn；统一半径阈值推出所有输出零距，反向证明半径top，结论双向。","dependencies":["CH03-D05","CH03-D06","CH03-P11-02","CH03-P18-01"]},
    {"id":"CH03-P21-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.const_cover"},{"file":"Main.lean","name":"MG.cover_one"}],"representation":"对非空像集构造单点内部中心及非空覆盖数下界；将等价条件的输出零距代入，任意正ε覆盖数为1。","dependencies":["CH03-D07"]},
    {"id":"CH03-P22-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.finite_cover"},{"file":"Main.lean","name":"MG.entropy_finite"},{"file":"Main.lean","name":"MG.finite_delta"}],"representation":"非空有限集及像集由自身中心覆盖；证明覆盖数≥1且有限、两熵为实数及差值等于实数差，复合子族伪度量自距零后即可代入。","dependencies":["CH03-D07","CH03-D08"]},
    {"id":"CH03-P23-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.const_entropy_delta"}],"representation":"输出常值分量以1个内部中心覆盖，输出熵0，差值定义前提自动成立且差值等于任意有限或无穷输入熵。","dependencies":["CH03-D07","CH03-D08","CH03-P21-02"]},
    {"id":"CH03-P23-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.ident_isometry"},{"file":"Main.lean","name":"MG.net_push"},{"file":"Main.lean","name":"MG.net_pull"},{"file":"Main.lean","name":"MG.isometry_cover"}],"representation":"恒等分量先导出点对保距；前向推中心，反向逐输出中心选原像，得到两覆盖数及熵相等。","dependencies":["CH03-D01","CH03-D07","CH03-P01-03","CH03-P19-02"]},
    {"id":"CH03-P23-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.isometry_delta"}],"representation":"在DeltaDefined前提下，覆盖数相等迫使两端均有限；用实数表示证明差0，不采用top-top。","dependencies":["CH03-D07","CH03-D08","CH03-P22-01","CH03-P23-02"]},
    {"id":"CH03-P24-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.lip_cover"},{"file":"Main.lean","name":"MG.net_push"}],"representation":"正有限L保证距离<ε/L推出像距<ε；内部中心的像给出输出覆盖且基数不增，得到原文覆盖数上界。","dependencies":["CH03-D07","CH03-P19-02"]},
    {"id":"CH03-P24-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.lip_delta"},{"file":"Main.lean","name":"MG.entropy_finite"}],"representation":"全有界保证ε及ε/L输入覆盖数有限，Lip覆盖界保证输出有限；扩展实数减法单调性给出原文熵差下界。","dependencies":["CH03-D07","CH03-D08","CH03-P19-03","CH03-P24-01"]},
    {"id":"CH03-P25-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.matrix_colip_cover"},{"file":"Main.lean","name":"MG.colip_cover"},{"file":"Main.lean","name":"MG.net_pull"}],"representation":"从合法co-Lip矩阵取指定单项下界，正有限条目允许除法；选每个输出内中心的输入代表元，证明输入覆盖及基数不增。","dependencies":["CH03-D07"]},
    {"id":"CH03-P25-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.matrix_colip_delta"},{"file":"Main.lean","name":"MG.colip_delta"},{"file":"Main.lean","name":"MG.entropy_finite"}],"representation":"输入全有界保证定义熵差所需的有限输入端；允许输出top，原文上界由覆盖数下界和EReal减法单调性推出。","dependencies":["CH03-D07","CH03-D08","CH03-P19-03","CH03-P25-01"]},
    {"id":"CH03-P26-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Affine.legal"},{"file":"Main.lean","name":"MG.Affine.first"},{"file":"Main.lean","name":"MG.realD_apply"}],"representation":"Option ℝ和绝对值读数的合法扩展伪度量；φ(x)=2x-1，原U={0,1}内首步目标纤维为U且分量常值。","dependencies":["CH03-D01","CH03-D02","CH03-P06-08","CH03-P17-04"]},
    {"id":"CH03-P26-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Affine.second"}],"representation":"仍在原U={0,1}上，φ²(0)目标纤维为{0}，两个输出读数为3与1，分量为有效；证明复合域合法。","dependencies":["CH03-D01","CH03-D02"]},
    {"id":"CH03-P26-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.point_constant_square"}],"representation":"对任意在U点值恒为非吸收c的算子，自复合统一取f(c)；若f(c)非吸收则U仍合法，若吸收则U与复合定义域不交。","dependencies":[]},
    {"id":"CH03-P27-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.colip_point_gap"}],"representation":"正co-Lip条目反射输出零距，与点态半径以下归零合用，排除任何严格介于0与点态半径的输入距离；K允许top。","dependencies":["CH03-D04","CH03-P14-02"]},
    {"id":"CH03-P27-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.colip_uniform_gap"}],"representation":"任意输入点对距离为0或至少统一半径；由点态间隙及统一半径≤每点半径证明，特别适用正统一半径。","dependencies":["CH03-D04","CH03-D05","CH03-P18-01","CH03-P27-01"]},
    {"id":"CH03-P28-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Translation.legal"},{"file":"Main.lean","name":"MG.Translation.domain"},{"file":"Main.lean","name":"MG.Translation.fibers"},{"file":"Main.lean","name":"MG.realD_apply"}],"representation":"合法绝对值读数实线与平移x+1；完整去重纤维分划分别为{-3},{-2,2},{0}和{-3},{-2,0},{2}。","dependencies":["CH03-D02","CH03-P17-04"]},
    {"id":"CH03-P28-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Translation.covers"},{"file":"Main.lean","name":"MG.Translation.entropy"}],"representation":"精确3/2处输入内部覆盖数2、输出1；构造中心及逐中心不能单覆盖的下界，熵差为1。","dependencies":["CH03-D07","CH03-D08"]},
    {"id":"CH03-P29-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Floor.legal"},{"file":"Main.lean","name":"MG.Floor.domain"},{"file":"Main.lean","name":"MG.Floor.first"}],"representation":"合法通常实线与取整算子，[0,1/2]直径1/2、统一半径top，分类(true,true)=(1,1)。","dependencies":["CH03-D05","CH03-D06","CH03-P11-02","CH03-P17-04"]},
    {"id":"CH03-P29-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Floor.legal"},{"file":"Main.lean","name":"MG.Floor.domain"},{"file":"Main.lean","name":"MG.Floor.second"}],"representation":"[9/10,11/10]直径1/5；从1左侧趋近的跨取整点对使统一半径0，分类(1,0)。","dependencies":["CH03-D05","CH03-D06","CH03-P17-04","CH03-P18-01"]},
    {"id":"CH03-P29-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Floor.legal"},{"file":"Main.lean","name":"MG.Floor.domain"},{"file":"Main.lean","name":"MG.Floor.third"}],"representation":"{0,2}直径2，正输入距离间隙给统一半径下界2，实际非零输出点对给上界2，分类(0,1)。","dependencies":["CH03-D04","CH03-D05","CH03-D06","CH03-P17-04","CH03-P18-01"]},
    {"id":"CH03-P29-04","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Floor.legal"},{"file":"Main.lean","name":"MG.Floor.domain"},{"file":"Main.lean","name":"MG.Floor.fourth"}],"representation":"[0,2]直径2；跨整数1的任意小距离点对使统一半径0，分类(0,0)。","dependencies":["CH03-D05","CH03-D06","CH03-P17-04","CH03-P18-01"]},
    {"id":"CH03-P29-05","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Floor.counterexample"},{"file":"Main.lean","name":"MG.Floor.third"}],"representation":"非空合法域{0,2}具有半径2≥1而输出0、2不零距；third的下界证明展示输入距离间隙是正半径来源。","dependencies":["CH03-D04","CH03-D05","CH03-D06","CH03-P18-01"]},
    {"id":"CH03-P30-01","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Four.legal"},{"file":"Main.lean","name":"MG.Four.cover"},{"file":"Main.lean","name":"MG.Four.external_center"}],"representation":"所有正ε的内部覆盖数：ε≤1为4，1<ε≤2为2，ε>2为1；包含开球端点，并证明3/2不属于U故不能作为内部中心。","dependencies":["CH03-D07","CH03-P17-04","CH03-P30-02"]},
    {"id":"CH03-P30-02","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Four.data"},{"file":"Main.lean","name":"MG.Four.same_images"}],"representation":"构造原文两张取值表，域外均吸收，验证两像集均为U；全部正精度覆盖数相同且两熵差均0。","dependencies":["CH03-D07","CH03-D08","CH03-P22-01","CH03-P30-01"]},
    {"id":"CH03-P30-03","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Four.lips"}],"representation":"逐点验证f,g的标量Lip界1、3，再用0与1这对输入分别证明任意合法L≥1、L≥3，得到最优值。","dependencies":[]},
    {"id":"CH03-P30-04","status":"complete","declarations":[{"file":"Main.lean","name":"MG.Four.estimates"}],"representation":"在7/4将通用lip_cover分别代入L=1与3，真实两输出覆盖数均2；输入上界分别2与4，故前者取等，后者严格宽松。","dependencies":["CH03-D07","CH03-P24-01","CH03-P30-01","CH03-P30-02","CH03-P30-03"]}
  ]
}