{"case_id":"MG-C003","version":"0.1.1","items":[
{"id":"CH03-D01","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.constComp"},{"file":"Chapter3/Core.lean","name":"Chapter3.idComp"},{"file":"Chapter3/Core.lean","name":"Chapter3.activeComp"},{"file":"Chapter3/Core.lean","name":"Chapter3.component_partition"}],"representation":"按常值优先定义三个指标集合，证明覆盖全指标集且两两不交；全域取U=dom。","dependencies":[]},
{"id":"CH03-D02","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.fiber"},{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_representation"},{"file":"Chapter3/Core.lean","name":"Chapter3.subfamily_zero"}],"representation":"计算纤维用所有j∈J的零距合取表示，证明等价于冻结复合伪度量为零；允许任意目标。","dependencies":["CH03-D07"]},
{"id":"CH03-D03","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.eqRel"},{"file":"Chapter3/Core.lean","name":"Chapter3.zeroRel"},{"file":"Chapter3/Core.lean","name":"Chapter3.imageSetoid"},{"file":"Chapter3/Core.lean","name":"Chapter3.ImageQuotient"},{"file":"Chapter3/Core.lean","name":"Chapter3.quotientPoint"},{"file":"Chapter3/Core.lean","name":"Chapter3.fiberPreorder"},{"file":"Chapter3/Core.lean","name":"Chapter3.zeroRel_fiber"}],"representation":"点对集合保留两点属于U；像商是实际像集子类型上的Quotient；证明零距点对与全纤维成员对应。","dependencies":["CH03-D02"]},
{"id":"CH03-D04","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.GoodRadius"},{"file":"Chapter3/Radius.lean","name":"Chapter3.radius"},{"file":"Chapter3/Radius.lean","name":"Chapter3.radius_representation"},{"file":"Chapter3/Radius.lean","name":"Chapter3.goodRadius_iff"}],"representation":"点态半径为全部有限正合法半径的sSup，球与评估域相交；证明集合包含表述对应。","dependencies":["CH03-P14-02"]},
{"id":"CH03-D05","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.uniformRadius"},{"file":"Chapter3/Radius.lean","name":"Chapter3.nullMatrix"}],"representation":"任意基点集A上的双重iInf；矩阵参数顺序为输出j、输入i，取A=U。","dependencies":["CH03-D04"]},
{"id":"CH03-D06","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.InputScale"},{"file":"Chapter3/Radius.lean","name":"Chapter3.diameter"},{"file":"Chapter3/Radius.lean","name":"Chapter3.diameterScale"},{"file":"Chapter3/Radius.lean","name":"Chapter3.channelType"},{"file":"Chapter3/Radius.lean","name":"Chapter3.threshold_cases"},{"file":"Chapter3/Radius.lean","name":"Chapter3.diameter_mono"},{"file":"Chapter3/Radius.lean","name":"Chapter3.thresholdType"}],"representation":"尺度定义在非空集合子类型上并要求包含单调；直径为点对上确界；Bool对精确编码两项阈值。","dependencies":["CH03-D05"]},
{"id":"CH03-D07","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.TotallyBoundedAt"},{"file":"Chapter3/Cover.lean","name":"Chapter3.covering_interface"},{"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"},{"file":"formal_oet/vol_01/ch_01_foundations/metric_entropy.lean","name":"formal_oet.vol_01.ch_01_foundations.subfamily_metric_entropy_eq_metric_entropy"},{"file":"Chapter3/Cover.lean","name":"Chapter3.entropy_finite"}],"representation":"直接导入冻结内部覆盖数与熵；证明最小中心数取得及无有限覆盖等价于无穷，全有界量化所有有限正半径。","dependencies":[]},
{"id":"CH03-D08","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.EntropyDefined"},{"file":"Chapter3/Cover.lean","name":"Chapter3.entropyDifference"},{"file":"Chapter3/Cover.lean","name":"Chapter3.entropy_difference_infinite"},{"file":"Chapter3/Correspondence.lean","name":"Chapter3.subfamilyEntropyDifference"},{"file":"Chapter3/Correspondence.lean","name":"Chapter3.subfamily_difference_representation"},{"file":"Chapter3/Correspondence.lean","name":"Chapter3.entropy_difference_finite"},{"file":"Chapter3/Correspondence.lean","name":"Chapter3.entropy_difference_signs"}],"representation":"熵差需一端覆盖数有限的证明参数；输入输出可取任意复合子族度量；证明有限值、两种无穷分支及符号解释。","dependencies":["CH03-D07"]},
{"id":"CH03-P01-01","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.const_zero_row"}],"representation":"常值输出距离等于零，有限指标求和的零行也等于零。","dependencies":["CH03-D01"]},
{"id":"CH03-P01-02","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.const_colip_zero"}],"representation":"任意源k和正输入距离见证，调用冻结co-Lip单项退化定理推出K k i=0。","dependencies":["CH03-D01"]},
{"id":"CH03-P01-03","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.id_distance"}],"representation":"输出与输入逐点零距，利用两次零距换端点证明输出点对距离等于输入距离。","dependencies":["CH03-D01"]},
{"id":"CH03-P02-01","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.compose_active"}],"representation":"在实际像域f(U)上分类外算子，四种非有效组合推出复合非有效。","dependencies":["CH03-D01","CH03-P01-03","CH03-P02-03","CH03-P04-01"]},
{"id":"CH03-P02-02","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.run"},{"file":"Chapter3/Core.lean","name":"Chapter3.stageActive"},{"file":"Chapter3/Core.lean","name":"Chapter3.run_active"},{"file":"Chapter3/Core.lean","name":"Chapter3.run_domains"},{"file":"Chapter3/Completion.lean","name":"Chapter3.StagesValid"},{"file":"Chapter3/Completion.lean","name":"Chapter3.run_stages_valid"}],"representation":"列表按作用顺序递归复合；stageActive递归使用每一步实际像域，空列表有效集为空，并证明域递推合法。另以递归StagesValid证明全部阶段的实际域合法性。","dependencies":["CH03-D01","CH03-P02-01"]},
{"id":"CH03-P02-03","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.compose_id"}],"representation":"逐点零距传递，且用外层保距排除复合常值分支。","dependencies":["CH03-D01","CH03-P01-03"]},
{"id":"CH03-P03-01","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.two"},{"file":"Chapter3/Examples.lean","name":"Chapter3.twoD"},{"file":"Chapter3/Examples.lean","name":"Chapter3.swap"},{"file":"Chapter3/Examples.lean","name":"Chapter3.swap_example"},{"file":"Chapter3/Correspondence.lean","name":"Chapter3.swap_nonreverse"}],"representation":"Option Bool编码吸收元和两点，验证扩展伪度量、域和像，计算两步有效与复合恒等，并明确否定两条逆包含。","dependencies":["CH03-D01"]},
{"id":"CH03-P04-01","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.outer_const"}],"representation":"将U中两点的像代入外算子在实际像集上的常值条件。","dependencies":["CH03-D01"]},
{"id":"CH03-P04-02","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.sevenGauge"},{"file":"Chapter3/Examples.lean","name":"Chapter3.sevenPhi"},{"file":"Chapter3/Examples.lean","name":"Chapter3.sevenPsi"},{"file":"Chapter3/Examples.lean","name":"Chapter3.seven_example"}],"representation":"Option(Fin 6)编码原七点；Bool给两分量，第一分量仅合并p,q；证明合法度量、复合域及内常值而复合非常值。","dependencies":["CH03-D01"]},
{"id":"CH03-P05-01","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.const_diagonal"}],"representation":"使用冻结单输入行化简；L可为无穷，ENNReal的乘零律给复合常值。","dependencies":["CH03-D01"]},
{"id":"CH03-P06-01","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_target"}],"representation":"任意目标在J中零距时，用三角不等式双向传递得到纤维相等。","dependencies":["CH03-D02"]},
{"id":"CH03-P06-02","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_cover"}],"representation":"每个像目标纤维含一个原像，所有像目标纤维的并等于U，含空域。","dependencies":["CH03-D02"]},
{"id":"CH03-P06-03","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_disjoint"},{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_cover"}],"representation":"任意两纤维有交点则目标零距并使纤维相等；结合非空及覆盖给去重分划。","dependencies":["CH03-D02","CH03-P06-01"]},
{"id":"CH03-P06-04","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_inter"}],"representation":"对非空J证明纤维等于所有单分量纤维之交，非空性用于恢复U条件。","dependencies":["CH03-D02"]},
{"id":"CH03-P06-05","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_antitone"}],"representation":"J包含于K时，K的全部零距条件蕴含J的条件。","dependencies":["CH03-D02"]},
{"id":"CH03-P06-06","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_singleton"},{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_full"}],"representation":"单元素纤维化为相应距离等于零；全指标纤维包含每个单分量纤维。","dependencies":["CH03-D02","CH03-P06-05"]},
{"id":"CH03-P06-07","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_id"}],"representation":"对任意目标y，恒等分量的输出零距条件等价于输入点与y零距。","dependencies":["CH03-D01","CH03-D02","CH03-P06-06"]},
{"id":"CH03-P06-08","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_const"},{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_const_empty"}],"representation":"像目标纤维等于U；与该目标正距离的目标纤维为空。","dependencies":["CH03-D01","CH03-D02"]},
{"id":"CH03-P07-01","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.Factors"},{"file":"Chapter3/Core.lean","name":"Chapter3.factor_iff"}],"representation":"实际像集到X的映射满足逐输入赋值公式时，输入等像关系包含于另一关系。","dependencies":["CH03-D03"]},
{"id":"CH03-P07-02","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.Factors"},{"file":"Chapter3/Core.lean","name":"Chapter3.factor_iff"}],"representation":"按实际像点存在的原像作选择并用关系包含证明赋值公式；空U无需选择任何点。","dependencies":["CH03-D03"]},
{"id":"CH03-P07-03","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.factors_both"}],"representation":"双向映射存在等价于双向关系包含，再由反对称性得到关系相等。","dependencies":["CH03-D03","CH03-P07-01"]},
{"id":"CH03-P07-04","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.scalar_factor_lip"}],"representation":"对实际像子类型的任意两点选原像，用正有限K的除法和L上界得到L/K；结论还允许L无穷。","dependencies":[]},
{"id":"CH03-P08-01","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.QuotientFactors"},{"file":"Chapter3/Core.lean","name":"Chapter3.quotient_factor_iff"}],"representation":"实际像集上的零距Setoid商；用Quotient.lift构造代表元无关映射，证明规定公式及必要性，包含空域。","dependencies":["CH03-D03"]},
{"id":"CH03-P08-02","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.quotient_factors_both"}],"representation":"双向商映射等价于两个零距关系集合相等。","dependencies":["CH03-D03","CH03-P08-01"]},
{"id":"CH03-P08-03","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.separated_rel"},{"file":"Chapter3/Core.lean","name":"Chapter3.separated_criteria"}],"representation":"分别仅假定两个实际像集上分离，证明点值关系等于零距关系并得到单向和双向判据一致。","dependencies":["CH03-D03","CH03-P07-01","CH03-P08-01"]},
{"id":"CH03-P09-01","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_preorder_refl"},{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_preorder_trans"}],"representation":"固定U的零距关系包含具有自反性和传递性。","dependencies":["CH03-D03"]},
{"id":"CH03-P09-02","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.relation_chain"}],"representation":"对任意有限m、a≤b≤m，从逐步集合包含归纳得到任意两层包含；实例R为各算子的zeroRel。","dependencies":[]},
{"id":"CH03-P09-03","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.relation_chain_strict"}],"representation":"从某一步真包含提取差集点，证明它在末层而不在首层，得到端点真包含。","dependencies":["CH03-P09-02"]},
{"id":"CH03-P10-01","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.realGauge"},{"file":"Chapter3/Examples.lean","name":"Chapter3.realGauge_valid"},{"file":"Chapter3/Examples.lean","name":"Chapter3.liftOperator_domain"},{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.step"},{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.stepDomain"},{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.step_valid"}],"representation":"Option实数编码吸收元，通常距离为ofReal绝对差，阶跃保持吸收元；原U非空且包含于定义域。","dependencies":[]},
{"id":"CH03-P10-02","status":"complete","declarations":[{"file":"Chapter3/Completion.lean","name":"Chapter3.step_near"},{"file":"Chapter3/Completion.lean","name":"Chapter3.step_radius"},{"file":"Chapter3/Completion.lean","name":"Chapter3.step_good_radius"}],"representation":"原固定U上每个实基点y的合法半径恰为0<r<∞且r≤|y|；证明点态半径=ofReal|y|>0，覆盖两个符号分支。","dependencies":["CH03-D04","CH03-P10-01","CH03-P14-02"]},
{"id":"CH03-P10-03","status":"complete","declarations":[{"file":"Chapter3/Completion.lean","name":"Chapter3.step_uniform_zero"}],"representation":"在同一固定阶跃评估域内，构造趋近零的异号点对；任意正尺度内输出距离仍为1，故统一半径为0。","dependencies":["CH03-D05","CH03-P10-01","CH03-P18-02"]},
{"id":"CH03-P11-01","status":"complete","declarations":[{"file":"Chapter3/Core.lean","name":"Chapter3.fiber_const"}],"representation":"任意输出子族包含于常值分量时，每个像目标的子族纤维等于U。","dependencies":["CH03-D01","CH03-D02"]},
{"id":"CH03-P11-02","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.constant_radii"},{"file":"Chapter3/Radius.lean","name":"Chapter3.constant_subfamily_radii"}],"representation":"所有输出点对零距使任意有限正半径合法，从上确界得到点态无穷和统一无穷。","dependencies":["CH03-D01","CH03-D02","CH03-D04","CH03-D05","CH03-D07","CH03-P14-02"]},
{"id":"CH03-P11-03","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.infiniteGauge"},{"file":"Chapter3/Examples.lean","name":"Chapter3.infinite_radius_example"}],"representation":"任意指定i,j的Option Bool例；输入i的异点距离无穷，其余分量距离1，含i=j和i≠j；恒等算子统一半径无穷但输出分量非常值。","dependencies":["CH03-D01","CH03-D04","CH03-D05","CH03-P03-01","CH03-P14-02"]},
{"id":"CH03-P12-01","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.id_image_fiber"}],"representation":"基点y在U，用恒等分量点对保距证明以f(y)为目标的纤维等于输入零距类。","dependencies":["CH03-D01","CH03-D02","CH03-P01-03","CH03-P06-06"]},
{"id":"CH03-P12-02","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.id_radius_lower"}],"representation":"有限正r的输入球内只有输入零距点时，证明r合法并得到半径≥r>0。","dependencies":["CH03-D01","CH03-D04","CH03-P01-03","CH03-P14-02"]},
{"id":"CH03-P13-01","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.radius_subfamily"},{"file":"Chapter3/Correspondence.lean","name":"Chapter3.radius_min_attained"}],"representation":"证明子族点态半径等于分量半径iInf，并在有限非空J上证明某个分量取得该最小值。","dependencies":["CH03-D02","CH03-D04","CH03-D07","CH03-P14-02"]},
{"id":"CH03-P13-02","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.uniform_subfamily"},{"file":"Chapter3/Correspondence.lean","name":"Chapter3.uniform_min_attained"}],"representation":"通过任意下界的等价式交换基点与分量量词，得到统一半径iInf公式并证明有限非空最小值取得。","dependencies":["CH03-D02","CH03-D04","CH03-D05","CH03-D07","CH03-P14-02"]},
{"id":"CH03-P13-03","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.uniform_subfamily_antitone"}],"representation":"对扩大后的输出子族取更多下确界，统一半径不增。","dependencies":["CH03-D05","CH03-D07","CH03-P13-02"]},
{"id":"CH03-P14-01","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.fiber_truncation"}],"representation":"纤维成员条件给反向输出零距，再以对称性改为原文方向。","dependencies":["CH03-D02"]},
{"id":"CH03-P14-02","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.radius_witness"},{"file":"Chapter3/Radius.lean","name":"Chapter3.below_radius"},{"file":"Chapter3/Radius.lean","name":"Chapter3.radius_truncation"}],"representation":"严格小于sSup时实际提取大于输入距离的有限正合法半径，应用其球包含条件和对称性。","dependencies":["CH03-D04"]},
{"id":"CH03-P14-03","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.composition_truncation"}],"representation":"显式保留输入属于上游定义域、两像点属于下游域；将像点代入纤维判据。","dependencies":["CH03-D02","CH03-P14-01"]},
{"id":"CH03-P15-01","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.compose_radius_zero"}],"representation":"下游零距保持仅在实际像域要求；以所有严格小于上游统一半径的点对归零推出复合下界。","dependencies":["CH03-D04","CH03-D05","CH03-P14-02","CH03-P18-01"]},
{"id":"CH03-P15-02","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.compose_radius_lip"}],"representation":"有限非零L的标量上界与ENNReal严格除法不等式拉回下游实际像域半径，统一涵盖右端零及无穷。","dependencies":["CH03-D04","CH03-D05","CH03-P14-02","CH03-P18-01"]},
{"id":"CH03-P16-01","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.thresholdType"},{"file":"Chapter3/Radius.lean","name":"Chapter3.threshold_cases"}],"representation":"Bool对取四个不同值，逐个证明值与原文四组互补不等式等价。","dependencies":[]},
{"id":"CH03-P16-02","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.threshold_scale_mono"}],"representation":"尺度小于旧阈值且旧阈值不大于新阈值，推出小于新阈值。","dependencies":[]},
{"id":"CH03-P16-03","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.threshold_null_antitone"}],"representation":"新零化阈值不大于半径时，旧阈值也不大于半径。","dependencies":[]},
{"id":"CH03-P17-01","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.scale_domain_mono"}],"representation":"任意InputScale的包含单调公理推出缩域尺度不增及严格阈值结论。","dependencies":["CH03-D06"]},
{"id":"CH03-P17-02","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.radius_domain_mono"}],"representation":"固定基点时，将大域上每个严格半径内零距条件限制到小域，证明点态半径不减。","dependencies":["CH03-D04","CH03-P14-02"]},
{"id":"CH03-P17-03","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.uniform_domain_mono"}],"representation":"同时将两点量词从A限制到B，得到基点集和评估域同时缩小的统一下界。","dependencies":["CH03-D04","CH03-D05","CH03-P14-02","CH03-P18-01"]},
{"id":"CH03-P17-04","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.realGauge_valid"},{"file":"Chapter3/Examples.lean","name":"Chapter3.real_diameter_pair"},{"file":"Chapter3/Examples.lean","name":"Chapter3.scale_counterexample"},{"file":"Chapter3/Completion.lean","name":"Chapter3.scale_counterexample_domain"}],"representation":"带吸收元实线上A={0,1}、B={0}，直径分别1和0，阈值1/2，且B包含于A。","dependencies":["CH03-D06","CH03-P10-01"]},
{"id":"CH03-P18-01","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.uniform_le_point"},{"file":"Chapter3/Radius.lean","name":"Chapter3.uniform_zero"}],"representation":"统一下确界不大于每个基点半径，严格输入距离条件推出输出零距。","dependencies":["CH03-D04","CH03-D05","CH03-P14-02"]},
{"id":"CH03-P18-02","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.output_separation"}],"representation":"取严格低于统一半径必归零的逆否，得到正输出分离的输入距离下界。","dependencies":["CH03-D05","CH03-P18-01"]},
{"id":"CH03-P18-03","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.separation_witness"}],"representation":"对每个大于统一半径的alpha提取失败点对；取epsilon=min(1,输出距离)，证明有限正且不超过输出距离，包括无穷输出。","dependencies":["CH03-D04","CH03-D05","CH03-P14-02"]},
{"id":"CH03-P19-01","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.threshold_fiber"}],"representation":"统一半径大于等于阈值时，将开球成员的严格距离代入统一归零判据。","dependencies":["CH03-D02","CH03-D05","CH03-P18-01"]},
{"id":"CH03-P19-02","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.cover_push"},{"file":"Chapter3/Cover.lean","name":"Chapter3.threshold_cover"}],"representation":"将每个内部有限中心集S映为f(S)，证明仍为内部中心且基数不增；对所有S取iInf，覆盖空集和无有限覆盖。","dependencies":["CH03-D05","CH03-D07","CH03-P18-01"]},
{"id":"CH03-P19-03","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.log2_mono"},{"file":"Chapter3/Cover.lean","name":"Chapter3.threshold_entropy"}],"representation":"证明冻结扩展log2单调，再应用覆盖数不等式；非空B为其特例。","dependencies":["CH03-D05","CH03-D07","CH03-P19-02"]},
{"id":"CH03-P20-01","status":"complete","declarations":[{"file":"Chapter3/Completion.lean","name":"Chapter3.step_cover_counterexample"}],"representation":"对每个有限正τ取a=min(1/2,τ.toReal/4)，证明0<a≤1、2a<τ、B={-a,a}包含于原U；内部输入覆盖数为1，输出在1/2尺度的内部覆盖数为2。","dependencies":["CH03-D07","CH03-P10-01","CH03-P28-02"]},
{"id":"CH03-P21-01","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.small_domain_iff"}],"representation":"精确保留diam<tauS≤tauN；正向以直径控制每对距离，反向由所有输出零距得到统一半径无穷。","dependencies":["CH03-D04","CH03-D05","CH03-D06","CH03-P11-02","CH03-P18-01"]},
{"id":"CH03-P21-02","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.cover_zero_class"},{"file":"Chapter3/Cover.lean","name":"Chapter3.constant_cover"},{"file":"Chapter3/Correspondence.lean","name":"Chapter3.small_domain_cover"}],"representation":"非空像集用单内部中心覆盖，配合非空覆盖数至少1，得到任意正精度覆盖数恰为1。","dependencies":["CH03-D05","CH03-D06","CH03-D07","CH03-P21-01"]},
{"id":"CH03-P22-01","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.finite_cover"},{"file":"Chapter3/Cover.lean","name":"Chapter3.finite_entropy_difference"}],"representation":"有限集合以自身作内部中心；两端子族覆盖数≥1且有限，熵为实数嵌入并给实数差值。","dependencies":["CH03-D02","CH03-D07","CH03-D08"]},
{"id":"CH03-P23-01","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.const_entropy"}],"representation":"常值输出内部覆盖数1、熵0，输出有限保证差值定义，差等于输入熵且允许其无穷。","dependencies":["CH03-D07","CH03-D08","CH03-P21-02"]},
{"id":"CH03-P23-02","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.cover_push"},{"file":"Chapter3/Cover.lean","name":"Chapter3.cover_pull"},{"file":"Chapter3/Cover.lean","name":"Chapter3.isometric_cover"},{"file":"Chapter3/Cover.lean","name":"Chapter3.id_entropy"}],"representation":"前向映射内部中心，反向为输出中心选择原像，证明恒等分量两端覆盖数及熵相等。","dependencies":["CH03-D01","CH03-D07","CH03-P01-03"]},
{"id":"CH03-P23-03","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.id_entropy_difference"}],"representation":"假定差值定义且U非空，由两端覆盖数相等推出有限，消去有限自差得到0。","dependencies":["CH03-D01","CH03-D07","CH03-D08","CH03-P23-02"]},
{"id":"CH03-P24-01","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.cover_push"},{"file":"Chapter3/Cover.lean","name":"Chapter3.lip_cover"}],"representation":"有限正L将epsilon/L输入内覆盖推为epsilon输出内覆盖，Finset.image基数不增。","dependencies":["CH03-D07"]},
{"id":"CH03-P24-02","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.lip_entropy_bound"},{"file":"Chapter3/Cover.lean","name":"Chapter3.entropy_finite"}],"representation":"全有界给两输入精度的有限覆盖，像覆盖也有限；扩展实数减法单调给所述熵差下界。","dependencies":["CH03-D07","CH03-D08","CH03-P19-03","CH03-P24-01"]},
{"id":"CH03-P25-01","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.cover_pull"},{"file":"Chapter3/Cover.lean","name":"Chapter3.colip_cover"}],"representation":"选取每个内部输出中心的原像，co-Lip求和单项下界和正有限K除法给输入内覆盖；无输出有限覆盖也适用。","dependencies":["CH03-D07"]},
{"id":"CH03-P25-02","status":"complete","declarations":[{"file":"Chapter3/Cover.lean","name":"Chapter3.colip_entropy_bound"}],"representation":"输入全有界提供差值定义，输出熵可无穷；扩展实数减法单调推出熵差上界。","dependencies":["CH03-D07","CH03-D08","CH03-P19-03","CH03-P25-01"]},
{"id":"CH03-P26-01","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.realGauge_valid"},{"file":"Chapter3/Examples.lean","name":"Chapter3.absGauge"},{"file":"Chapter3/Examples.lean","name":"Chapter3.affine"},{"file":"Chapter3/Examples.lean","name":"Chapter3.affine_example"}],"representation":"Option实数上绝对值读数伪度量和仿射算子合法；U={0,1}上phi的指定纤维为U，分量为常值。","dependencies":["CH03-D01","CH03-D02","CH03-P10-01"]},
{"id":"CH03-P26-02","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.affine_example"}],"representation":"同一U上phi平方的指定纤维为{0}，分量为有效，且U属于复合定义域。","dependencies":["CH03-D01","CH03-D02","CH03-P10-01","CH03-P26-01"]},
{"id":"CH03-P26-03","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.point_constant_iteration"},{"file":"Chapter3/Completion.lean","name":"Chapter3.point_constant_fibers"}],"representation":"若f在U点值常为c，则平方在U常为f(c)；f(c)非吸收时U仍合法，为吸收时U与复合定义域不交。明确证明平方算子的每个像目标子族纤维均为U，并区分定义域合法与再次输出吸收元分支。","dependencies":["CH03-D02","CH03-P06-08"]},
{"id":"CH03-P27-01","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.colip_point_gap"}],"representation":"正co-Lip条目反射输出零距，故输入正距离不可能严格小于点态半径；不要求系数有限。","dependencies":["CH03-D04","CH03-P14-02"]},
{"id":"CH03-P27-02","status":"complete","declarations":[{"file":"Chapter3/Radius.lean","name":"Chapter3.colip_uniform_gap"}],"representation":"每个输入距离为零，或不小于统一半径；下确界与点态间隙给出二择。","dependencies":["CH03-D04","CH03-D05","CH03-P18-01","CH03-P27-01"]},
{"id":"CH03-P28-01","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.realGauge_valid"},{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.translate"},{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.translateDomain"},{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.translate_fibers"}],"representation":"完整按四个输入代表列出恒等和平移纤维，包含重复块去重对应；证明平移域条件。","dependencies":["CH03-D02","CH03-P10-01","CH03-P26-01"]},
{"id":"CH03-P28-02","status":"complete","declarations":[{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.translate_image"},{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.cover_two_lower"},{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.translate_cover"}],"representation":"精确半径3/2时用双内部中心及排除单中心证明输入覆盖数2，单内部中心证明输出覆盖数1，熵差1。","dependencies":["CH03-D07","CH03-D08","CH03-P10-01","CH03-P28-01"]},
{"id":"CH03-P29-01","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.realGauge_valid"},{"file":"Chapter3/Completion.lean","name":"Chapter3.floor_intervals_valid"},{"file":"Chapter3/Completion.lean","name":"Chapter3.floor_interval_small"}],"representation":"原带吸收元实线及取整算子；非空合法域[0,1/2]的直径1/2，输出常值，统一半径∞，阈值(1,1)得到(true,true)。","dependencies":["CH03-D04","CH03-D05","CH03-D06","CH03-P10-01","CH03-P11-02","CH03-P29-03"]},
{"id":"CH03-P29-02","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.realGauge_valid"},{"file":"Chapter3/Completion.lean","name":"Chapter3.floor_intervals_valid"},{"file":"Chapter3/Completion.lean","name":"Chapter3.floor_interval_cross"}],"representation":"非空合法域[9/10,11/10]的直径1/5；在1附近构造任意近且输出不同的点对，统一半径0，类型(true,false)。","dependencies":["CH03-D05","CH03-D06","CH03-P10-01","CH03-P18-02","CH03-P29-03"]},
{"id":"CH03-P29-03","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.realGauge_valid"},{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.floorOperator"},{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.floorPair"},{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.uniform_pair"},{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.floor_pair"}],"representation":"通常实线取整算子在D={0,2}上合法；直径2、统一半径2、阈值类型(false,true)，半径来自输入两点间隙。","dependencies":["CH03-D04","CH03-D05","CH03-D06","CH03-P10-01","CH03-P14-02","CH03-P17-04","CH03-P18-02"]},
{"id":"CH03-P29-04","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.realGauge_valid"},{"file":"Chapter3/Completion.lean","name":"Chapter3.floor_intervals_valid"},{"file":"Chapter3/Completion.lean","name":"Chapter3.floor_interval_large"}],"representation":"非空合法域[0,2]的直径2；由跨越1的小区间包含及统一半径域单调性证明半径0，类型(false,false)。","dependencies":["CH03-D05","CH03-D06","CH03-P10-01","CH03-P17-03","CH03-P29-02","CH03-P29-03"]},
{"id":"CH03-P29-05","status":"complete","declarations":[{"file":"Chapter3/MoreExamples.lean","name":"Chapter3.floor_pair"}],"representation":"同一合法二点D具有半径2≥1但输出0和2仍正分离，否定无直径条件的整体零化蕴含。","dependencies":["CH03-D05","CH03-D06","CH03-P10-01","CH03-P17-04","CH03-P29-03"]},
{"id":"CH03-P30-01","status":"complete","declarations":[{"file":"Chapter3/Examples.lean","name":"Chapter3.realGauge_valid"},{"file":"Chapter3/FourPoint.lean","name":"Chapter3.fourU"},{"file":"Chapter3/FourPoint.lean","name":"Chapter3.four_cover"},{"file":"Chapter3/FourPoint.lean","name":"Chapter3.four_center_exclusion"}],"representation":"原四点实集U={0,1,2,3}，任意ε>0的内部覆盖数：ε≤1时4，1<ε≤2时2，ε>2时1；分别证明上下界，包含两个开球端点；3/2不属于U，不能充当内部中心。","dependencies":["CH03-D07","CH03-P10-01","CH03-P28-02"]},
{"id":"CH03-P30-02","status":"complete","declarations":[{"file":"Chapter3/FourPoint.lean","name":"Chapter3.fourF"},{"file":"Chapter3/FourPoint.lean","name":"Chapter3.fourG"},{"file":"Chapter3/FourPoint.lean","name":"Chapter3.four_operators"},{"file":"Chapter3/FourPoint.lean","name":"Chapter3.four_entropy"}],"representation":"两个算子按题表取值并在U外为吸收元，证明定义域及像均为U；任意正精度像覆盖数同于输入的完整分段，有限熵差为0。","dependencies":["CH03-D07","CH03-D08","CH03-P10-01","CH03-P22-01","CH03-P30-01"]},
{"id":"CH03-P30-03","status":"complete","declarations":[{"file":"Chapter3/FourPoint.lean","name":"Chapter3.four_operators"},{"file":"Chapter3/FourPoint.lean","name":"Chapter3.ScalarBound"},{"file":"Chapter3/FourPoint.lean","name":"Chapter3.four_lip_bounds"},{"file":"Chapter3/FourPoint.lean","name":"Chapter3.four_lip_optimal"}],"representation":"逐对证明f的标量Lip界1与g的界3；由输入点0和1推出任意合法系数分别≥1和≥3，故最优值为1和3。","dependencies":["CH03-P10-01","CH03-P30-01","CH03-P30-02"]},
{"id":"CH03-P30-04","status":"complete","declarations":[{"file":"Chapter3/FourPoint.lean","name":"Chapter3.four_lip_cover_comparison"}],"representation":"实际调用一般Lip覆盖上界，在ε=7/4用常数1、3；右侧输入覆盖数分别2、4，两算子真实输出覆盖数均为2，故第一界取等、第二界宽松。","dependencies":["CH03-D07","CH03-P10-01","CH03-P24-01","CH03-P30-01","CH03-P30-02","CH03-P30-03"]}
]}