{
  "case_id": "MG-C003",
  "version": "0.1.1",
  "items": [
    {"id":"CH03-D01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Const"},{"file":"Main.lean","name":"Chapter3.Ident"},{"file":"Main.lean","name":"Chapter3.Active"},{"file":"Main.lean","name":"Chapter3.component_partition"}],"representation":"任意分量按常值优先定义三类；证明互斥及覆盖。","dependencies":[]},
    {"id":"CH03-D02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Fiber"},{"file":"Main.lean","name":"Chapter3.SingleFiber"},{"file":"Main.lean","name":"Chapter3.subfamily_zero"},{"file":"Main.lean","name":"Chapter3.fiber_representation"}],"representation":"子族逐分量零距定义纤维；证明等价于复合伪度量零距。","dependencies":[]},
    {"id":"CH03-D03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.PointRel"},{"file":"Main.lean","name":"Chapter3.ZeroRel"},{"file":"Main.lean","name":"Chapter3.imageSetoid"},{"file":"Main.lean","name":"Chapter3.ImageQuotient"},{"file":"Main.lean","name":"Chapter3.imageClass"},{"file":"Main.lean","name":"Chapter3.FiberLE"},{"file":"Main.lean","name":"Chapter3.zeroRel_fiber"}],"representation":"点对关系限于U×U；实际像集取零距商；预序为关系包含，并证明纤维对应。","dependencies":["CH03-D02"]},
    {"id":"CH03-D04","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Legal"},{"file":"Main.lean","name":"Chapter3.radius"},{"file":"Main.lean","name":"Chapter3.legal_ball"},{"file":"Main.lean","name":"Chapter3.le_radius_iff"}],"representation":"半径为合法有限正半径的上确界；球包含与逐点公式等价。","dependencies":[]},
    {"id":"CH03-D05","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.uniform"},{"file":"Main.lean","name":"Chapter3.N"}],"representation":"uniform在指定基点集合取下确界；N的首指标为输出行。","dependencies":["CH03-D04"]},
    {"id":"CH03-D06","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Scale"},{"file":"Main.lean","name":"Chapter3.diameter"},{"file":"Main.lean","name":"Chapter3.diameterScale"},{"file":"Main.lean","name":"Chapter3.thresholdType"},{"file":"Main.lean","name":"Chapter3.channelType"},{"file":"Main.lean","name":"Chapter3.threshold_bits"}],"representation":"尺度定义在非空集合且单调；默认直径；Bool对精确表示两个阈值判断。","dependencies":["CH03-D05"]},
    {"id":"CH03-D07","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.TotallyBoundedFor"},{"file":"Main.lean","name":"Chapter3.covering_representation"},{"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.metric_entropy"}],"representation":"冻结内部覆盖数以内部有限中心及开球定义；covering_representation证明球并集等价及无有限覆盖边界，covering_number_attained证明有限时取得最小中心数；冻结metric_entropy为其log2，TotallyBoundedFor遍历全部有限正精度。","dependencies":[]},
    {"id":"CH03-D08","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.DeltaDefined"},{"file":"Main.lean","name":"Chapter3.delta"},{"file":"Main.lean","name":"Chapter3.delta_guard"},{"file":"Main.lean","name":"Chapter3.finite_delta"},{"file":"Main.lean","name":"Chapter3.delta_infinite_cases"}],"representation":"两端至少一覆盖数有限才定义EReal熵差；证明排除双无穷及有限实数差对应；输入熵无穷而输出有限时差为正无穷，反向为负无穷。","dependencies":["CH03-D07"]},
    {"id":"CH03-P01-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.const_zero_row"}],"representation":"常值条件给全部点对零行求和上界。","dependencies":["CH03-D01"]},
    {"id":"CH03-P01-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.const_colip_zero"}],"representation":"任意正输入距离见证迫使指定co-Lip条目为零。","dependencies":["CH03-D01"]},
    {"id":"CH03-P01-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.ident_distance"}],"representation":"由逐点零距双向传递证明所有输入点对保距。","dependencies":["CH03-D01"]},
    {"id":"CH03-P02-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.compose_active"}],"representation":"在实际中间像域证明两步有效分量包含。","dependencies":["CH03-D01","CH03-P01-03","CH03-P02-03","CH03-P04-01"]},
    {"id":"CH03-P02-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.chain"},{"file":"Main.lean","name":"Chapter3.activeSteps"},{"file":"Main.lean","name":"Chapter3.chain_active"},{"file":"Main.lean","name":"Chapter3.ValidChain"},{"file":"Main.lean","name":"Chapter3.chain_domains"}],"representation":"列表按时间顺序复合；递推实际像域，证明全部域合法及任意长度包含，含零步。","dependencies":["CH03-D01","CH03-P02-01"]},
    {"id":"CH03-P02-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.compose_ident"}],"representation":"复合逐点零距且排除常值优先分支。","dependencies":["CH03-D01","CH03-P01-03"]},
    {"id":"CH03-P03-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Swap.d"},{"file":"Main.lean","name":"Chapter3.Swap.f"},{"file":"Main.lean","name":"Chapter3.Swap.U"},{"file":"Main.lean","name":"Chapter3.Swap.valid"},{"file":"Main.lean","name":"Chapter3.Swap.domain"},{"file":"Main.lean","name":"Chapter3.Swap.image"},{"file":"Main.lean","name":"Chapter3.Swap.active"},{"file":"Main.lean","name":"Chapter3.Swap.composite"},{"file":"Main.lean","name":"Chapter3.Swap.reverse_failures"}],"representation":"Option(Fin2)表示三点空间；完整验证换位及两条逆包含失败。","dependencies":["CH03-D01"]},
    {"id":"CH03-P04-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.outer_const"}],"representation":"外侧在实际像域常值，代入像点得复合常值。","dependencies":["CH03-D01"]},
    {"id":"CH03-P04-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Seven.d"},{"file":"Main.lean","name":"Chapter3.Seven.f"},{"file":"Main.lean","name":"Chapter3.Seven.g"},{"file":"Main.lean","name":"Chapter3.Seven.U"},{"file":"Main.lean","name":"Chapter3.Seven.valid"},{"file":"Main.lean","name":"Chapter3.Seven.domain"},{"file":"Main.lean","name":"Chapter3.Seven.inner"},{"file":"Main.lean","name":"Chapter3.Seven.outer_fails"}],"representation":"Option(Fin6)表示七点；0,1为a,b，2,3为p,q，4,5为r,s；双分量合法并给出反例。","dependencies":["CH03-D01"]},
    {"id":"CH03-P05-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.inner_const_lip"}],"representation":"指定输出行仅同分量输入时内侧常值传给复合；不要求系数有限。","dependencies":["CH03-D01"]},
    {"id":"CH03-P06-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.fiber_target"}],"representation":"任意零距目标对应的子族纤维相等。","dependencies":["CH03-D02"]},
    {"id":"CH03-P06-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.fiber_cover"}],"representation":"证明每个像目标纤维非空且纤维并集恰为U。","dependencies":["CH03-D02"]},
    {"id":"CH03-P06-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.fiber_equal_or_disjoint"},{"file":"Main.lean","name":"Chapter3.fiber_cover"}],"representation":"全部纤维相等或不交；连同非空和覆盖给出去重分划。","dependencies":["CH03-D02","CH03-P06-01"]},
    {"id":"CH03-P06-04","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.fiber_intersection"}],"representation":"非空子族纤维等于全部单分量纤维的交。","dependencies":["CH03-D02"]},
    {"id":"CH03-P06-05","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.fiber_antitone"}],"representation":"更多输出分量要求给出更小纤维。","dependencies":["CH03-D02"]},
    {"id":"CH03-P06-06","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.fiber_singleton"},{"file":"Main.lean","name":"Chapter3.fiber_all_subset"}],"representation":"单元素子族等式及全子族向每分量的包含。","dependencies":["CH03-D02"]},
    {"id":"CH03-P06-07","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.ident_fiber"}],"representation":"恒等分量对任意目标的纤维等于输入零距类。","dependencies":["CH03-D01","CH03-D02"]},
    {"id":"CH03-P06-08","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.const_fiber"},{"file":"Main.lean","name":"Chapter3.const_fiber_empty"}],"representation":"像内目标纤维为U；与之正距离的任意目标纤维为空。","dependencies":["CH03-D01","CH03-D02"]},
    {"id":"CH03-P07-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Factors"},{"file":"Main.lean","name":"Chapter3.factors_iff"}],"representation":"实际像域上的因子映射存在推出点值关系包含。","dependencies":["CH03-D03"]},
    {"id":"CH03-P07-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Factors"},{"file":"Main.lean","name":"Chapter3.factors_iff"}],"representation":"从实际像点选择输入代表元构造因子映射并验证公式；空像域也适用。","dependencies":["CH03-D03"]},
    {"id":"CH03-P07-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.factors_both"}],"representation":"双向点值变换等价于点值关系相等。","dependencies":["CH03-D03","CH03-P07-01","CH03-P07-02"]},
    {"id":"CH03-P07-04","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.factor_lip"}],"representation":"在实际像域证明任意规定T的L/K界；K正有限且L有限。","dependencies":["CH03-D03"]},
    {"id":"CH03-P08-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.QuotientFactors"},{"file":"Main.lean","name":"Chapter3.quotient_factors_iff"}],"representation":"实际像零距商；构造代表元无关的Quotient.lift并双向验证规定公式。","dependencies":["CH03-D03"]},
    {"id":"CH03-P08-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.quotient_factors_both"}],"representation":"双向规定商映射等价于零距关系相等。","dependencies":["CH03-D03","CH03-P08-01"]},
    {"id":"CH03-P08-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.SeparatesOn"},{"file":"Main.lean","name":"Chapter3.relations_equal_on_separated_image"},{"file":"Main.lean","name":"Chapter3.separated_factor_criteria"}],"representation":"分别假设两个实际像集分离，证明两种关系及单向、双向判据一致。","dependencies":["CH03-D03","CH03-P07-01","CH03-P07-02","CH03-P08-01"]},
    {"id":"CH03-P09-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.fiberLE_refl"},{"file":"Main.lean","name":"Chapter3.fiberLE_trans"}],"representation":"固定U，关系包含给出预序的自反及传递。","dependencies":["CH03-D03"]},
    {"id":"CH03-P09-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.relation_chain"}],"representation":"对任意自然数端点a≤b归纳证明逐步包含的复合；适用于任意有限截断。","dependencies":[]},
    {"id":"CH03-P09-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.relation_chain_strict"}],"representation":"任一步真包含给端点真包含，并实际给出端点差集元素。","dependencies":["CH03-P09-02"]},
    {"id":"CH03-P10-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.realGauge"},{"file":"Main.lean","name":"Chapter3.realOp"},{"file":"Main.lean","name":"Chapter3.realSet"},{"file":"Main.lean","name":"Chapter3.Step.a"},{"file":"Main.lean","name":"Chapter3.Step.f"},{"file":"Main.lean","name":"Chapter3.Step.U"},{"file":"Main.lean","name":"Chapter3.Step.valid"},{"file":"Main.lean","name":"Chapter3.Step.domain"}],"representation":"Option实线以none为吸收元；通常距离及阶跃算子；验证固定U非空且在定义域内。","dependencies":[]},
    {"id":"CH03-P10-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Step.point_radius"},{"file":"Main.lean","name":"Chapter3.Step.legal_radii"}],"representation":"固定U中每个实基点，合法有限正半径恰满足r≤|y|，上确界等于|y|且正。","dependencies":["CH03-D04","CH03-P10-01"]},
    {"id":"CH03-P10-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Step.uniform_zero"}],"representation":"在同一固定U构造任意接近零的异号基点，证明统一半径为零。","dependencies":["CH03-D04","CH03-D05","CH03-P10-01","CH03-P18-02"]},
    {"id":"CH03-P11-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.const_subfamily_fiber"}],"representation":"子族各分量常值时任一输入基点的像目标纤维为U。","dependencies":["CH03-D01","CH03-D02"]},
    {"id":"CH03-P11-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.const_subfamily_radius"}],"representation":"子族输出两两零距，证明所有基点及统一半径均为无穷。","dependencies":["CH03-D01","CH03-D04","CH03-D05","CH03-D02"]},
    {"id":"CH03-P11-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Infinite.d"},{"file":"Main.lean","name":"Chapter3.Infinite.U"},{"file":"Main.lean","name":"Chapter3.Infinite.valid"},{"file":"Main.lean","name":"Chapter3.Infinite.domain"},{"file":"Main.lean","name":"Chapter3.Infinite.uniform_infinite"},{"file":"Main.lean","name":"Chapter3.Infinite.not_const"}],"representation":"合法两点无穷输入距离模型；输入0、输出j遍历Fin2，涵盖同分量与异分量两分支。","dependencies":["CH03-D01","CH03-D04","CH03-D05"]},
    {"id":"CH03-P12-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.ident_image_fiber"}],"representation":"利用恒等分量保距，像目标纤维恰为输入基点零距类。","dependencies":["CH03-D01","CH03-D02","CH03-P01-03"]},
    {"id":"CH03-P12-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.ident_radius_lower"}],"representation":"有限正r的球中只有输入零距点时，证明r是合法半径并给出下界。","dependencies":["CH03-D01","CH03-D04","CH03-P01-03"]},
    {"id":"CH03-P13-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.radius_subfamily"},{"file":"Main.lean","name":"Chapter3.finite_inf_attained"}],"representation":"点态子族半径为各单分量半径下确界；有限非空时证明最小值取得。","dependencies":["CH03-D02","CH03-D04"]},
    {"id":"CH03-P13-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.uniform_subfamily"},{"file":"Main.lean","name":"Chapter3.finite_inf_attained"}],"representation":"交换基点和分量下确界，结合最小值取得给出统一半径最小值公式。","dependencies":["CH03-D04","CH03-D05","CH03-P13-01"]},
    {"id":"CH03-P13-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.uniform_subfamily_antitone"}],"representation":"子族包含经分量下确界公式推出统一半径反单调。","dependencies":["CH03-D05","CH03-P13-02"]},
    {"id":"CH03-P14-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.fiber_truncate"}],"representation":"纤维成员的输出零距由对称性转为原文方向。","dependencies":["CH03-D02"]},
    {"id":"CH03-P14-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.below_radius"}],"representation":"严格小于上确界时从合法集提取更大的有限正半径，再应用球内条件。","dependencies":["CH03-D04"]},
    {"id":"CH03-P14-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.composite_truncate"}],"representation":"显式保留上游定义域、两像点在下游域及纤维条件，证明复合输出零距。","dependencies":["CH03-D02","CH03-P14-01"]},
    {"id":"CH03-P15-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.radius_compose"}],"representation":"下游在实际像域保持零距时，给出复合统一半径下界。","dependencies":["CH03-D04","CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P15-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.radius_compose_lip"}],"representation":"有限正L拉回下游实际像域的统一半径；扩展数除法涵盖右端0及无穷。","dependencies":["CH03-D04","CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P16-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.threshold_cases"},{"file":"Main.lean","name":"Chapter3.threshold_bits"}],"representation":"四种Bool组合逐一等价于互补不等式，故互斥且穷尽。","dependencies":["CH03-D06"]},
    {"id":"CH03-P16-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.threshold_scale_mono"}],"representation":"尺度严格小于阈值的判断随尺度阈值增大保持。","dependencies":[]},
    {"id":"CH03-P16-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.threshold_radius_antitone"}],"representation":"半径大于等于阈值的判断随零化阈值增大反单调。","dependencies":[]},
    {"id":"CH03-P17-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.scale_restrict"}],"representation":"任意单调尺度在非空域缩小时不增，并保留严格阈值判断。","dependencies":["CH03-D06"]},
    {"id":"CH03-P17-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.radius_restrict"}],"representation":"固定任意基点，限制评估域使合法半径上确界不减。","dependencies":["CH03-D04"]},
    {"id":"CH03-P17-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.uniform_restrict"}],"representation":"同时缩小评估域及下确界基点集合，统一半径不减。","dependencies":["CH03-D04","CH03-D05","CH03-P17-02"]},
    {"id":"CH03-P17-04","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.scale_reverse_counterexample"}],"representation":"带吸收元通常实线，A={0,1}、B={0}及阈值1/2，证明域条件、两直径及反向失败。","dependencies":["CH03-D06"]},
    {"id":"CH03-P18-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.below_uniform"}],"representation":"输入距离严格小于统一下确界则小于该基点半径，输出归零。","dependencies":["CH03-D04","CH03-D05","CH03-P14-02"]},
    {"id":"CH03-P18-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.separated_input"}],"representation":"由正输出距离及单步判据逆否得到输入距离下界。","dependencies":["CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P18-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.separation_witness"}],"representation":"每个规定有限正α，从下确界及非法球提取两点，再取有限正ε；输出无穷亦适用。","dependencies":["CH03-D04","CH03-D05"]},
    {"id":"CH03-P19-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.threshold_fiber"}],"representation":"统一半径达到阈值时，任意基点的阈值球交评估域包含在纤维中。","dependencies":["CH03-D02","CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P19-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.push_net"},{"file":"Main.lean","name":"Chapter3.push_cover"},{"file":"Main.lean","name":"Chapter3.threshold_cover"}],"representation":"任意B子集的内部输入中心映到内部输出中心且基数不增；下确界证明涵盖空集及无有限覆盖。","dependencies":["CH03-D07","CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P19-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.log2_mono"},{"file":"Main.lean","name":"Chapter3.entropy_mono_cover"},{"file":"Main.lean","name":"Chapter3.threshold_entropy"}],"representation":"非空B下证明扩展对数单调，从覆盖数界得到熵界，允许无穷。","dependencies":["CH03-D07","CH03-P19-02"]},
    {"id":"CH03-P20-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Step.cover_counterexample"}],"representation":"在同一固定阶跃U中，对每个有限正τ取0<t≤1且2t<τ；内部二点B的输入覆盖数为1，像在1/2下覆盖数为2。","dependencies":["CH03-D07","CH03-P10-01"]},
    {"id":"CH03-P21-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.small_domain"}],"representation":"精确直径<τσ≤τN条件下，双向证明半径阈值与整体输出零距等价。","dependencies":["CH03-D04","CH03-D05","CH03-D06","CH03-P18-01"]},
    {"id":"CH03-P21-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.zero_cover_one"},{"file":"Main.lean","name":"Chapter3.small_domain_cover"}],"representation":"非空像域以一个内部中心覆盖；非空覆盖数下界给出恰为1。","dependencies":["CH03-D07","CH03-P21-01"]},
    {"id":"CH03-P22-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.finite_cover"},{"file":"Main.lean","name":"Chapter3.finite_entropy"},{"file":"Main.lean","name":"Chapter3.delta_defined_finite"},{"file":"Main.lean","name":"Chapter3.finite_delta"}],"representation":"非空有限输入及实际像，任意两端非空子族的覆盖数有限且由非空性至少为1；熵及其差表示为实数。","dependencies":["CH03-D07","CH03-D08"]},
    {"id":"CH03-P23-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.const_entropy"}],"representation":"常值分量像覆盖数1、熵0，存在合法熵差且等于输入熵，输入允许无穷。","dependencies":["CH03-D01","CH03-D07","CH03-D08","CH03-P21-02"]},
    {"id":"CH03-P23-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.ident_cover"},{"file":"Main.lean","name":"Chapter3.push_net"},{"file":"Main.lean","name":"Chapter3.pull_net"}],"representation":"恒等分量通过前向映中心与反向选代表元证明内部覆盖数和熵相等。","dependencies":["CH03-D01","CH03-D07","CH03-P01-03"]},
    {"id":"CH03-P23-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.ident_delta"}],"representation":"显式要求熵差良定；由覆盖数相等推出有限并证明熵差0。","dependencies":["CH03-D08","CH03-P23-02"]},
    {"id":"CH03-P24-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.push_net"},{"file":"Main.lean","name":"Chapter3.lip_cover"}],"representation":"有限正L将ε/L内部中心映为ε输出内部中心，基数不增。","dependencies":["CH03-D07"]},
    {"id":"CH03-P24-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.lip_delta"}],"representation":"输入全有界给两端有限实熵及良定熵差，再由覆盖数界证明原文下界。","dependencies":["CH03-D07","CH03-D08","CH03-P24-01","CH03-P19-03"]},
    {"id":"CH03-P25-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.pull_net"},{"file":"Main.lean","name":"Chapter3.colip_cover"}],"representation":"正有限co-Lip单条目将内部输出中心的代表元拉回为ε/K输入覆盖，中心数不增。","dependencies":["CH03-D07"]},
    {"id":"CH03-P25-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.colip_delta"}],"representation":"全有界输入保证熵差良定；允许输出无穷，用扩展实数减法单调性证明原文上界。","dependencies":["CH03-D07","CH03-D08","CH03-P25-01","CH03-P19-03"]},
    {"id":"CH03-P26-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Affine.d"},{"file":"Main.lean","name":"Chapter3.Affine.f"},{"file":"Main.lean","name":"Chapter3.Affine.U"},{"file":"Main.lean","name":"Chapter3.Affine.valid"},{"file":"Main.lean","name":"Chapter3.Affine.domain"},{"file":"Main.lean","name":"Chapter3.Affine.first_fiber"},{"file":"Main.lean","name":"Chapter3.Affine.first_const"}],"representation":"绝对值读数伪度量及2x-1算子合法；U={0,1}，第一纤维为U且分量常值。","dependencies":["CH03-D01","CH03-D02"]},
    {"id":"CH03-P26-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Affine.second_fiber"},{"file":"Main.lean","name":"Chapter3.Affine.second_active"}],"representation":"精确保留U={0,1}，自复合指定纤维={0}，分量有效。","dependencies":["CH03-D01","CH03-D02"]},
    {"id":"CH03-P26-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.point_constant_square"}],"representation":"U上点值常算子的自复合仍点值常；域合法等价于U为空或再次像不是吸收元。","dependencies":[]},
    {"id":"CH03-P27-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.colip_radius_gap"}],"representation":"正co-Lip通道和点态零化判据排除(0,rN)内输入距离；K可无穷。","dependencies":["CH03-D04","CH03-P14-02"]},
    {"id":"CH03-P27-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.colip_uniform_gap"}],"representation":"全部输入点对要么零距要么达到统一半径；无需额外假设K有限。","dependencies":["CH03-D05","CH03-P18-01"]},
    {"id":"CH03-P28-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Translation.d"},{"file":"Main.lean","name":"Chapter3.Translation.f"},{"file":"Main.lean","name":"Chapter3.Translation.U"},{"file":"Main.lean","name":"Chapter3.Translation.valid"},{"file":"Main.lean","name":"Chapter3.Translation.domain"},{"file":"Main.lean","name":"Chapter3.Translation.fibers"}],"representation":"Option实线的绝对值读数规范与平移合法；逐一计算所有输入点对应纤维：恒等分划为{-3},{-2,2},{0}，平移分划为{-3},{-2,0},{2}。","dependencies":["CH03-D02"]},
    {"id":"CH03-P28-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Translation.image"},{"file":"Main.lean","name":"Chapter3.Translation.covers"},{"file":"Main.lean","name":"Chapter3.Translation.entropy_difference"}],"representation":"精确3/2开球下，以内部中心构造上界并排除单中心得到输入覆盖数2；像覆盖数1，合法熵差1。","dependencies":["CH03-D07","CH03-D08","CH03-P28-01"]},
    {"id":"CH03-P29-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Floor.a"},{"file":"Main.lean","name":"Chapter3.Floor.f"},{"file":"Main.lean","name":"Chapter3.Floor.D₁"},{"file":"Main.lean","name":"Chapter3.Floor.D₂"},{"file":"Main.lean","name":"Chapter3.Floor.D₃"},{"file":"Main.lean","name":"Chapter3.Floor.D₄"},{"file":"Main.lean","name":"Chapter3.Floor.valid"},{"file":"Main.lean","name":"Chapter3.Floor.domains"},{"file":"Main.lean","name":"Chapter3.Floor.first"}],"representation":"通常实线及取整算子合法，四域非空且属于定义域；[0,1/2]的直径1/2、统一半径无穷、阈值类型(1,1)。","dependencies":["CH03-D04","CH03-D05","CH03-D06"]},
    {"id":"CH03-P29-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Floor.second_radius"},{"file":"Main.lean","name":"Chapter3.Floor.second"}],"representation":"[9/10,11/10]的直径1/5；用1左右任意接近的点证明统一半径0，类型(1,0)。","dependencies":["CH03-D05","CH03-D06","CH03-P18-02","CH03-P29-01"]},
    {"id":"CH03-P29-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Floor.third"}],"representation":"{0,2}的直径2；小于2的输入距离只连接同一点，并以两点正输出距离给出统一半径上界2，类型(0,1)。","dependencies":["CH03-D04","CH03-D05","CH03-D06","CH03-P18-02","CH03-P29-01"]},
    {"id":"CH03-P29-04","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Floor.fourth"}],"representation":"[0,2]的直径2，包含第二域使统一半径≤0，因此半径0、类型(0,0)。","dependencies":["CH03-D05","CH03-D06","CH03-P17-03","CH03-P29-02"]},
    {"id":"CH03-P29-05","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Floor.counterexample"}],"representation":"合法域{0,2}统一半径2≥1但输出不零距；同时证明小于2的距离只连接同一点，说明正半径来自输入间隙。","dependencies":["CH03-D05","CH03-P29-03"]},
    {"id":"CH03-P30-01","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Four.a"},{"file":"Main.lean","name":"Chapter3.Four.U"},{"file":"Main.lean","name":"Chapter3.Four.valid"},{"file":"Main.lean","name":"Chapter3.Four.covers"},{"file":"Main.lean","name":"Chapter3.Four.center_illegal"}],"representation":"对全部正ε证明内部覆盖数：0<ε≤1为4，1<ε≤2为2，2<ε为1；各上界均给内部中心，下界排除较少中心；3/2不属于U，不能作为内部中心。","dependencies":["CH03-D07"]},
    {"id":"CH03-P30-02","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Four.f"},{"file":"Main.lean","name":"Chapter3.Four.g"},{"file":"Main.lean","name":"Chapter3.Four.data"},{"file":"Main.lean","name":"Chapter3.Four.image_covers"},{"file":"Main.lean","name":"Chapter3.Four.deltas"}],"representation":"按原表定义两算子且U外均为吸收元；定义域与两像集均为U，各精度像覆盖数等于输入覆盖数，合法映射熵差均为0。","dependencies":["CH03-D07","CH03-D08","CH03-P30-01"]},
    {"id":"CH03-P30-03","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Four.Bound"},{"file":"Main.lean","name":"Chapter3.Four.optimal"}],"representation":"对全部扩展非负系数L证明f的标量界当且仅当L≥1，g的标量界当且仅当L≥3；包含有限表穷举上界与点对(0,1)必要下界。","dependencies":["CH03-P30-02"]},
    {"id":"CH03-P30-04","status":"complete","declarations":[{"file":"Main.lean","name":"Chapter3.Four.bounds_at_precision"}],"representation":"在7/4处实际调用一般Lip覆盖上界；f给2≤2，g给2≤4；证明两真实覆盖数及两输入缩放尺度的覆盖数。","dependencies":["CH03-P24-01","CH03-P30-01","CH03-P30-02","CH03-P30-03"]}
  ]
}