{"case_id":"MG-C003","version":"0.1.1","items":[
{"id":"CH03-D01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Iconst"},{"file":"Main.lean","name":"MGC003.Iid"},{"file":"Main.lean","name":"MGC003.Iact"},{"file":"Main.lean","name":"MGC003.mem_Iact"},{"file":"Main.lean","name":"MGC003.not_mem_Iact"}],"representation":"Iconst/Iid/Iact 为 Set I：常值=∀x,y∈U 输出零距；恒等=∉Iconst 且 ∀x∈U d_i(ϕx,x)=0（常值优先）；有效=I∖(Iconst∪Iid)；mem_Iact/not_mem_Iact 给出‘有效 ⇔ 非常值且非恒等’的成员刻画；U 为显式参数，全域分划取 U=dom ϕ；U⊆dom ϕ 在各命题中作为假设给出。","dependencies":[]},
{"id":"CH03-D02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Fib"},{"file":"Main.lean","name":"MGC003.mem_Fib"},{"file":"Main.lean","name":"MGC003.mem_Fib_singleton"},{"file":"Main.lean","name":"MGC003.subfam_eq_zero_iff"},{"file":"Main.lean","name":"MGC003.subfam_self"},{"file":"Main.lean","name":"MGC003.subfamily_pseudometric_eq_max"},{"file":"Main.lean","name":"MGC003.ball_subfamily_eq"}],"representation":"Fib d ϕ J y U={x∈U | d_J(ϕx,y)=0}，d_J 即冻结背景 subfamily_pseudometric（sup）；mem_Fib/subfam_eq_zero_iff 给出逐分量刻画（d_J=0 ⇔ 各 d_j=0），subfam_self 给出 d_J(x,x)=0；J={i} 为单分量，U=dom ϕ 为全域纤维；定义本身不预设 J 非空或 U⊆dom ϕ，这些前提在各命题中显式给出；subfamily_pseudometric_eq_max / ball_subfamily_eq 证明冻结背景以上确界实现的 d_J 就是正文的最大值 max_{j∈J} d_j（J 有限非空：d_J 不小于每个分量且恰好等于某个分量；B_J(x₀,r)=⋂_{j∈J}B_j(x₀,r)）。","dependencies":[]},
{"id":"CH03-D03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Req"},{"file":"Main.lean","name":"MGC003.Rsim"},{"file":"Main.lean","name":"MGC003.FiberGe"},{"file":"Main.lean","name":"MGC003.gaugeSetoid"},{"file":"Main.lean","name":"MGC003.imageSetoid"},{"file":"Main.lean","name":"MGC003.HasQuotientMap"},{"file":"Main.lean","name":"MGC003.Factors"},{"file":"Main.lean","name":"MGC003.SepOn"},{"file":"Main.lean","name":"MGC003.Rsim_iff_mem_Fib"},{"file":"Main.lean","name":"MGC003.fiberGe_iff_fiber_subset"}],"representation":"Req/Rsim 为 U×U 中 ϕ(x)=ϕ(y) 与 ϕ(x)∼_G ϕ(y)（GaugeZeroRelated）的点对集；FiberGe 为 Rsim 包含（零测距纤维预序）；gaugeSetoid/imageSetoid 为 ∼_G（引理 1.1，冻结背景 gauge_zero_related_equivalence）及其在像集 ϕ(U) 上的商；HasQuotientMap 为带规定赋值公式 T̄([ϕA x])=[ϕB x] 的商映射存在；Factors 为 T∘ϕA=ϕB；SepOn 为像集上的分离性；Rsim_iff_mem_Fib 给出 (x,y)∈R_∼ ⇔ y∈Fib_{ϕ,I}(ϕ(x)|U)；fiberGe_iff_fiber_subset 给出纤维预序的逐点纤维包含表述 Fib_{ϕA,I}(ϕA x|U)⊆Fib_{ϕB,I}(ϕB x|U)（分划细化）；其与商映射存在的等价见 CH03-P08-01 的 fiberGe_iff_hasQuotientMap。","dependencies":["CH03-D02"]},
{"id":"CH03-D04","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.NullAdm"},{"file":"Main.lean","name":"MGC003.nullRadius"},{"file":"Main.lean","name":"MGC003.nullRadiusJ"},{"file":"Main.lean","name":"MGC003.nullRadiusJ_singleton"},{"file":"Main.lean","name":"MGC003.NullAdm_intro"},{"file":"Main.lean","name":"MGC003.nullAdm_downward"},{"file":"Main.lean","name":"MGC003.le_nullRadius_of_mem"},{"file":"Main.lean","name":"MGC003.le_nullRadius_of_forall"},{"file":"Main.lean","name":"MGC003.nullRadius_eq_top_of_zero"},{"file":"Main.lean","name":"MGC003.mem_nullAdm_of_lt_nullRadius"},{"file":"Main.lean","name":"MGC003.nullRadius_eq_zero_iff"},{"file":"Main.lean","name":"MGC003.nullRadius_eq_top_iff"},{"file":"Main.lean","name":"MGC003.nullAdm_subfamily_eq_fib"},{"file":"Main.lean","name":"MGC003.nullRadiusJ_eq_sSup_fiber"}],"representation":"NullAdm 为合法有限正半径集 {r∈(0,∞) | B_in(y,r)∩U ⊆ {x∈U | d_out(ϕx,ϕy)=0}}（B_in 为冻结背景 ball）；nullRadius=sSup NullAdm（sSup ∅=0，可取 ⊤）；nullRadiusJ 取 d_out=d_J；NullAdm_intro/nullAdm_downward/le_nullRadius_of_mem/le_nullRadius_of_forall/nullRadius_eq_top_of_zero 为 sSup 刻画的基本引理（合法半径向下封闭、任一合法半径不超过零化半径、所有输出零距时半径为 ⊤）；mem_nullAdm_of_lt_nullRadius（严格小于 r^N 的有限正半径本身合法）、nullRadius_eq_zero_iff（约定 sup ∅=0：r^N=0 ⇔ 无合法半径）、nullRadius_eq_top_iff（r^N=+∞ ⇔ 任意有限正半径均合法）证明 sSup 表示与正文一致；nullAdm_subfamily_eq_fib / nullRadiusJ_eq_sSup_fiber 给出输出取 d_J 时输出零测距集合就是计算纤维 Fib_{ϕ,J}(ϕ(y)|U)。","dependencies":["CH03-D02"]},
{"id":"CH03-D05","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.uniformNullRadius"},{"file":"Main.lean","name":"MGC003.uniformNullRadiusJ"},{"file":"Main.lean","name":"MGC003.nullMatrix"},{"file":"Main.lean","name":"MGC003.uniformNullRadiusJ_singleton"},{"file":"Main.lean","name":"MGC003.uniformNullRadius_le"},{"file":"Main.lean","name":"MGC003.le_uniformNullRadius"},{"file":"Main.lean","name":"MGC003.nullMatrix_le"}],"representation":"uniformNullRadius=⨅_{y∈A} nullRadius（评估域 U，基点集 A）；uniformNullRadiusJ 为输出取 d_J 且 A=U；nullMatrix d ϕ U j i（行 j 输出、列 i 输入）=r̲^N_{ϕ,i,j}|_U；uniformNullRadius_le/le_uniformNullRadius/nullMatrix_le 为 inf 刻画的基本引理。","dependencies":["CH03-D04"]},
{"id":"CH03-D06","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.IsInputScale"},{"file":"Main.lean","name":"MGC003.diamScale"},{"file":"Main.lean","name":"MGC003.diamScale_isInputScale"},{"file":"Main.lean","name":"MGC003.thresholdType"}],"representation":"IsInputScale：对非空 A₁⊆A₂ 单调的族 σ_i；diamScale 为默认直径尺度 sup_{x,y∈A} d_i；thresholdType=(σ_i(A)<τσ, τN≤r̲^N_{f,i,j}|_A) 以 Bool×Bool 表示","dependencies":["CH03-D05"]},
{"id":"CH03-D07","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.TotallyBoundedIn"},{"file":"Main.lean","name":"MGC003.subfamilyCoveringNumber"},{"file":"Main.lean","name":"MGC003.internalEpsilonNet_iff"},{"file":"Main.lean","name":"MGC003.covering_number_textbook"},{"file":"Main.lean","name":"MGC003.metric_entropy_textbook"},{"file":"Main.lean","name":"MGC003.subfamily_singleton_agree"},{"file":"Main.lean","name":"MGC003.totallyBoundedIn_iff"},{"file":"Main.lean","name":"MGC003.totallyBoundedIn_entropy_real"},{"file":"Main.lean","name":"MGC003.covering_number_le_card"},{"file":"Main.lean","name":"MGC003.le_covering_number_of_forall"},{"file":"Main.lean","name":"MGC003.covering_number_le_of_transfer"},{"file":"Main.lean","name":"MGC003.covering_number_lt_top_of_net"},{"file":"Main.lean","name":"MGC003.covering_number_eq_card"},{"file":"Main.lean","name":"MGC003.two_le_card_of_net"},{"file":"Main.lean","name":"MGC003.subset_of_net_of_separated"},{"file":"Main.lean","name":"MGC003.cov_image_le"},{"file":"Main.lean","name":"MGC003.cov_preimage_le"},{"file":"Main.lean","name":"MGC003.cov_finite"},{"file":"Main.lean","name":"MGC003.cov_one_of_zero"},{"file":"Main.lean","name":"MGC003.log2_ereal_mono"},{"file":"Main.lean","name":"MGC003.log2_ereal_one"},{"file":"Main.lean","name":"MGC003.log2_ereal_eq_coe"},{"file":"Main.lean","name":"MGC003.log2_ereal_ne_top"},{"file":"Main.lean","name":"MGC003.entropy_real"},{"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.InternalEpsilonNet"},{"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"},{"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.covering_number_empty"},{"file":"formal_oet/vol_01/ch_01_foundations/metric_entropy.lean","name":"formal_oet.vol_01.ch_01_foundations.metric_entropy_nonneg"},{"file":"formal_oet/vol_01/ch_01_foundations/metric_entropy.lean","name":"formal_oet.vol_01.ch_01_foundations.metric_entropy_empty"},{"file":"formal_oet/vol_01/ch_01_foundations/metric_entropy.lean","name":"formal_oet.vol_01.ch_01_foundations.one_le_covering_number_of_nonempty"},{"file":"formal_oet/vol_01/ch_01_foundations/metric_entropy.lean","name":"formal_oet.vol_01.ch_01_foundations.log2_ereal"},{"file":"Main.lean","name":"MGC003.subfamily_pseudometric_eq_max"},{"file":"Main.lean","name":"MGC003.ball_subfamily_eq"},{"file":"Main.lean","name":"MGC003.internalEpsilonNet_subfamily_iff"},{"file":"Main.lean","name":"MGC003.subfamily_metric_entropy_eq_log2"}],"representation":"覆盖数/熵沿用冻结背景 covering_number、InternalEpsilonNet、metric_entropy、subfamily_metric_entropy 及其基本引理；internalEpsilonNet_iff、covering_number_textbook、metric_entropy_textbook 证明其与正文一致（内覆盖=S⊆U 且 U⊆⋃B(s,ε)；无有限内覆盖时为 +∞，空集为 0；E=log₂𝒩，非空集合 E∈[0,+∞]，空集为 −∞）；subfamilyCoveringNumber 为子族覆盖数（度量取冻结背景的子族复合伪度量），subfamily_singleton_agree 给出 J={i} 退化为单分量；TotallyBoundedIn 为‘∀有限正 r，𝒩_i(r,U)<∞’，totallyBoundedIn_iff 给出其等价的内覆盖存在形式；其余为覆盖数比较与熵单调的接口引理（cov_image_le、cov_preimage_le、cov_finite、cov_one_of_zero、log2_ereal_mono 等）；子族部分：subfamily_pseudometric_eq_max / ball_subfamily_eq 证明冻结背景的 d_J（上确界）即正文的最大值；internalEpsilonNet_subfamily_iff 给出子族内覆盖的逐分量刻画（中心取自 U，且每个 x∈U 在某中心 c 处对所有 j∈J 有 d_j(x,c)<ε）；subfamily_metric_entropy_eq_log2 给出 E_{ε,J}=log₂𝒩_J。","dependencies":[]},
{"id":"CH03-D08","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.mapEntropyDiff"},{"file":"Main.lean","name":"MGC003.MapEntropyDiffDefined"},{"file":"Main.lean","name":"MGC003.mapEntropyDiff_cases"},{"file":"Main.lean","name":"MGC003.mapEntropyDiff_singleton"},{"file":"Main.lean","name":"MGC003.defined_singleton"}],"representation":"mapEntropyDiff=E_{ε,Jin}(U)−E_{ε,Jout}(ϕ(U)) 取值 EReal，使用 subfamily_metric_entropy；MapEntropyDiffDefined 为良定前提；mapEntropyDiff_cases 给出 ⊤/⊥/实数各情形并排除 ∞−∞","dependencies":["CH03-D07"]},
{"id":"CH03-P01-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_1_i"}],"representation":"i∈Iconst(ϕ|U) 时对 x,y∈U 有 d_i(ϕx,ϕy)≤∑_k 0·d_k(x,y)=0；并证明：任一 U 上的 Lip 矩阵 L 把输出分量 i 对应的整行（条目 L_{k→i}，k∈I）置零后仍是合法 Lip 矩阵（‘输出行取零行’）。","dependencies":["CH03-D01"]},
{"id":"CH03-P01-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_1_ii"}],"representation":"i∈Iconst、K 为 U 上 co-Lip 矩阵，若某 x,y∈U 使 d_k(x,y)>0 则 K k i=0（经冻结背景 colip_entry_eq_zero_of_output_zero_input_pos）。","dependencies":["CH03-D01"]},
{"id":"CH03-P01-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_1_iii"}],"representation":"i∈Iid 时对 x,y∈U 有 d_i(ϕx,ϕy)=d_i(x,y)（三角不等式双向，经 epm_eq）。","dependencies":["CH03-D01"]},
{"id":"CH03-P02-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_2_i"},{"file":"Main.lean","name":"MGC003.not_Iact_comp"},{"file":"Main.lean","name":"MGC003.Iid_comp"}],"representation":"U⊆dom(ϕ₂∘ϕ₁) 时 Iact(ϕ₂∘ϕ₁|U)⊆Iact(ϕ₁|U)∪Iact(ϕ₂|ϕ₁(U))，第二步在实际中间像域 ϕ₁(U) 上；逐分量按 (a)–(d) 四种情形证明。","dependencies":["CH03-D01","CH03-P01-03"]},
{"id":"CH03-P02-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_2_ii"},{"file":"Main.lean","name":"MGC003.chainComp"},{"file":"Main.lean","name":"MGC003.chainComp_stage"},{"file":"Main.lean","name":"MGC003.dom_mul_subset"},{"file":"Main.lean","name":"MGC003.chainComp_zero"},{"file":"Main.lean","name":"MGC003.chainComp_succ"},{"file":"Main.lean","name":"MGC003.chainComp_eq_prod"}],"representation":"chainComp ϕ n=ϕ_n∘⋯∘ϕ_1（n=0 为 id）；U 1⊆dom c_n，U(m+1)=ϕ_m(U m)；对 n 归纳（零步基例 Iact=∅）得 Iact(c_n|U₁)⊆⋃_{m=1}^n Iact(ϕ_m|U_m)；chainComp_zero / chainComp_succ / chainComp_eq_prod 给出 c_0=id、c_{k+1}=ϕ_{k+1}∘c_k，以及 c_n 作为幺半群 𝒳_op 中乘积 ϕ_n·⋯·ϕ_1 的对应。","dependencies":["CH03-D01","CH03-P02-01"]},
{"id":"CH03-P02-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_2_iii"},{"file":"Main.lean","name":"MGC003.Iid_comp"}],"representation":"Iid(ϕ₁|U)∩Iid(ϕ₂|ϕ₁(U))⊆Iid(ϕ₂∘ϕ₁|U)，含证明复合输出不两两零距（排除常值优先分支）与逐点零距。","dependencies":["CH03-D01","CH03-P01-03"]},
{"id":"CH03-P03-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Swap.note_converse_fails"},{"file":"Main.lean","name":"MGC003.Swap.swap_distances"},{"file":"Main.lean","name":"MGC003.Swap.swap_step_classes"},{"file":"Main.lean","name":"MGC003.Swap.swap_comp_classes"},{"file":"Main.lean","name":"MGC003.Swap.Sp"},{"file":"Main.lean","name":"MGC003.Swap.d0"},{"file":"Main.lean","name":"MGC003.Swap.dS"},{"file":"Main.lean","name":"MGC003.Swap.Uab"},{"file":"Main.lean","name":"MGC003.Swap.swapOp"},{"file":"Main.lean","name":"MGC003.Swap.dS_gauge"},{"file":"Main.lean","name":"MGC003.Swap.swapOp_image"},{"file":"Main.lean","name":"MGC003.Swap.swap_legal"},{"file":"Main.lean","name":"MGC003.Swap.Uab_dom"},{"file":"Main.lean","name":"MGC003.Swap.none_not_mem_Uab"},{"file":"Main.lean","name":"MGC003.Swap.converse_i_not_general"},{"file":"Main.lean","name":"MGC003.Swap.converse_iii_not_general"}],"representation":"合法结构：三点空间 Option Bool（⊥=none，a=some false，b=some true），单分量 0/1 离散度量、⊥ 孤立（Swap.dS_gauge 证明 ExtendedPseudoMetric，含非吸收点与吸收元隔离），U={a,b}，换位算子 swapOp（φ(⊥)=⊥ 由 Operator 结构保证），swapOp_image 证明 φ(U)=U；完整计算：swap_distances（d(φa,φb)=1，d(φa,a)=1，复合把 a,b 映回自身且输出距离仍为 1）、swap_step_classes（两步均 Iact={i}、非常值非恒等）、swap_comp_classes（复合 Iid={i}、Iact=∅）；note_converse_fails 同时给出两条严格包含并否定两个反向包含；Swap.swap_legal 汇总构造合法性：规范结构合法、算子保持 ⊥、⊥∉U、U⊆dom φ₁ 且 U⊆dom(φ₂∘φ₁)（命题 3.2 的前提成立）；Swap.converse_i_not_general / Swap.converse_iii_not_general 把‘两条逆向包含一般不成立’写成对一切有限非空指标集、扩展规范族与算子的全称命题的否定（由本例给出反例）。","dependencies":["CH03-D01"]},
{"id":"CH03-P04-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_3_i"}],"representation":"Iconst(ψ|ϕ(U))⊆Iconst(ψ∘ϕ|U)（外侧在实际像域 ϕ(U) 上常值）。","dependencies":["CH03-D01"]},
{"id":"CH03-P04-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.SevenPt.prop3_3_ii_example"},{"file":"Main.lean","name":"MGC003.SevenPt.Sp"},{"file":"Main.lean","name":"MGC003.SevenPt.ci"},{"file":"Main.lean","name":"MGC003.SevenPt.dI"},{"file":"Main.lean","name":"MGC003.SevenPt.dI_gauge"},{"file":"Main.lean","name":"MGC003.SevenPt.phi"},{"file":"Main.lean","name":"MGC003.SevenPt.psi"},{"file":"Main.lean","name":"MGC003.SevenPt.U"},{"file":"Main.lean","name":"MGC003.SevenPt.U_dom"},{"file":"Main.lean","name":"MGC003.SevenPt.seven_legal"},{"file":"Main.lean","name":"MGC003.SevenPt.U_dom_phi"},{"file":"Main.lean","name":"MGC003.SevenPt.image_dom_psi"},{"file":"Main.lean","name":"MGC003.SevenPt.none_not_mem_U"},{"file":"Main.lean","name":"MGC003.SevenPt.prop3_3_ii_not_general"}],"representation":"七点空间 Option (Fin 6)（⊥=none；p,q,r,s,a,b=some 0,…,some 5）、指标集 Bool={i,m}；dI_gauge 验证两个分量均为合法扩展伪度量（d_i 合并 p,q，其余异点距离 1；d_m 离散）；phi(a)=p,phi(b)=q，psi(p)=r,psi(q)=s，其余处 ⊥；U_dom 验证 U={a,b}⊆dom(ψ∘ϕ)；prop3_3_ii_example 汇总：d_m(p,q)=1、复合输出 d_i(r,s)=1、i∈Iconst(ϕ|U)、i∉Iconst(ψ∘ϕ|U)；SevenPt.seven_legal 汇总构造合法性：两个分量均为合法扩展伪度量、φ 与 ψ 保持 ⊥、⊥∉U、U⊆dom φ、φ(U)={p,q}⊆dom ψ、U⊆dom(ψ∘φ)；SevenPt.prop3_3_ii_not_general 把‘i∈I_const(ϕ|U) 未必推出 i∈I_const(ψ∘ϕ|U)’写成全称命题的否定。","dependencies":["CH03-D01"]},
{"id":"CH03-P05-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.cor3_4"}],"representation":"j∈Iconst(ϕ|U)，L 为 ψ 在 ϕ(U) 上的 Lip 矩阵且 L k j=0（k≠j）则 j∈Iconst(ψ∘ϕ|U)；L j j 可为 ⊤（乘 0 得 0）","dependencies":["CH03-D01"]},
{"id":"CH03-P06-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_5_i"}],"representation":"d_J(y,y')=0 时 Fib_J(y|U)=Fib_J(y'|U)（J 非空，d_J 为扩展伪度量）。","dependencies":["CH03-D02"]},
{"id":"CH03-P06-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_5_ii_a"}],"representation":"∀y∈ϕ(U) 纤维非空，且 U⊆⋃_{y∈ϕ(U)} Fib_J(y|U)。","dependencies":["CH03-D02"]},
{"id":"CH03-P06-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_5_ii_b"},{"file":"Main.lean","name":"MGC003.IsPartitionOf"}],"representation":"像目标纤维相等或不交；去重后的族 {Fib(y|U)} 构成 U 的分划（非空、两两不交、并为 U）。","dependencies":["CH03-D02","CH03-P06-01","CH03-P06-02"]},
{"id":"CH03-P06-04","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_5_iii"}],"representation":"J 非空时 Fib_J=⋂_{j∈J}Fib_{j}。","dependencies":["CH03-D02"]},
{"id":"CH03-P06-05","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_5_iv"}],"representation":"J⊆K 时 Fib_K(y|U)⊆Fib_J(y|U)。","dependencies":["CH03-D02"]},
{"id":"CH03-P06-06","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_5_v"}],"representation":"Fib_{i}(y|U)={x∈U|d_i(ϕx,y)=0}；Fib_{univ}⊆各单分量纤维。","dependencies":["CH03-D02"]},
{"id":"CH03-P06-07","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_5_vi_a"}],"representation":"j∈Iid(ϕ|U) 时，对任意目标 y，Fib_{j}(y|U)={x∈U|d_j(x,y)=0}。","dependencies":["CH03-D01","CH03-D02"]},
{"id":"CH03-P06-08","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_5_vi_b"}],"representation":"j∈Iconst(ϕ|U) 时，y₀∈ϕ(U) 的纤维为 U，且 d_j(y,y₀)>0 时 Fib_{j}(y|U)=∅。","dependencies":["CH03-D01","CH03-D02"]},
{"id":"CH03-P07-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_6_i_nec"}],"representation":"若 T:ϕA(U)→X 满足 T∘ϕA=ϕB，则 Req(ϕA|U)⊆Req(ϕB|U)。","dependencies":["CH03-D03"]},
{"id":"CH03-P07-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_6_i_suff"},{"file":"Main.lean","name":"MGC003.prop3_6_i"}],"representation":"由 Req 包含用 Classical.choose 构造 T 并验证 T∘ϕA=ϕB（U=∅ 时像为空子类型，亦成立）；prop3_6_i 为双向等价。","dependencies":["CH03-D03","CH03-P07-01"]},
{"id":"CH03-P07-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_6_ii"}],"representation":"两个方向的点值变换都存在 ⇔ Req(ϕA|U)=Req(ϕB|U)。","dependencies":["CH03-D03","CH03-P07-02"]},
{"id":"CH03-P07-04","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_6_iii"},{"file":"Main.lean","name":"MGC003.prop3_6_iii_scalar"},{"file":"Main.lean","name":"MGC003.HasScalarCoLipBound"}],"representation":"KA∈(0,∞)、LB<∞，co-Lip 与 Lip 标量界在 U 上成立，T 存在时在像域 ϕA(U) 上 d(Tp,Tq)≤(LB/KA)·d(p,q)；scalar 版本使用背景 HasScalarLipBound 及对应的 HasScalarCoLipBound","dependencies":["CH03-D03"]},
{"id":"CH03-P08-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_7_i"},{"file":"Main.lean","name":"MGC003.fiberGe_iff_hasQuotientMap"}],"representation":"HasQuotientMap（带规定赋值公式的 Quotient 映射）存在 ⇔ Rsim(ϕA|U)⊆Rsim(ϕB|U)；充分性用 Quotient.lift 构造代表元无关映射并验证公式；fiberGe_iff_hasQuotientMap 把它重述为‘零测距纤维预序 FiberGe ⇔ 存在商映射’。","dependencies":["CH03-D03"]},
{"id":"CH03-P08-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_7_ii"}],"representation":"双向商映射存在 ⇔ Rsim(ϕA|U)=Rsim(ϕB|U)。","dependencies":["CH03-D03","CH03-P08-01"]},
{"id":"CH03-P08-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_7_iii"},{"file":"Main.lean","name":"MGC003.Req_subset_Rsim"}],"representation":"两个实际像集 ϕA(U)、ϕB(U) 各自 SepOn 分离时，Req=Rsim，点值判据与商值判据（单向、双向）等价。","dependencies":["CH03-D03","CH03-P07-02","CH03-P07-03","CH03-P08-01","CH03-P08-02"]},
{"id":"CH03-P09-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.note_fiber_preorder"},{"file":"Main.lean","name":"MGC003.prop_fiber_refl"},{"file":"Main.lean","name":"MGC003.prop_fiber_trans"}],"representation":"FiberGe 自反、传递（Rsim 包含）。","dependencies":["CH03-D03"]},
{"id":"CH03-P09-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.note_fiber_chain"}],"representation":"公共域 U 上链 ϕ₀⪰⋯⪰ϕ_m：任意 a≤b≤m 有 ϕ_a⪰ϕ_b。","dependencies":["CH03-D03","CH03-P09-01"]},
{"id":"CH03-P09-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.note_fiber_strict"}],"representation":"链中某步 Rsim 真包含则 Rsim(ϕ₀)⊂Rsim(ϕ_m)，并给出差集见证 p∈R_{r+1}∖R_r 且 p∈R_m∖R_0。","dependencies":["CH03-D03","CH03-P09-02"]},
{"id":"CH03-P10-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.RealLine.dR"},{"file":"Main.lean","name":"MGC003.RealLine.dR_gauge"},{"file":"Main.lean","name":"MGC003.RealLine.dR_some"},{"file":"Main.lean","name":"MGC003.RealLine.dR_zero_iff"},{"file":"Main.lean","name":"MGC003.RealLine.stepFn"},{"file":"Main.lean","name":"MGC003.RealLine.stepOp"},{"file":"Main.lean","name":"MGC003.RealLine.stepOp_some"},{"file":"Main.lean","name":"MGC003.RealLine.Ustep"},{"file":"Main.lean","name":"MGC003.RealLine.Ustep_mem"},{"file":"Main.lean","name":"MGC003.RealLine.Ustep_sub_dom"},{"file":"Main.lean","name":"MGC003.RealLine.none_not_mem_Ustep"}],"representation":"带吸收元实线 R=Option ℝ（⊥=none），dR=extPM(通常距离)，dR_gauge 验证其为合法扩展伪度量；阶跃算子 stepOp(x)=0(x<0)/1(x≥0)（stepOp(⊥)=⊥ 由 Operator 结构保证）；U=Ustep=[-1,0)∪(0,1]，Ustep_sub_dom 验证 U⊆dom stepOp，none_not_mem_Ustep 验证 ⊥∉U，Ustep_mem 给出 U 的元素刻画。","dependencies":[]},
{"id":"CH03-P10-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.RealLine.step_nullAdm"},{"file":"Main.lean","name":"MGC003.RealLine.step_nullRadius"},{"file":"Main.lean","name":"MGC003.RealLine.same_sign"},{"file":"Main.lean","name":"MGC003.RealLine.stepFn_eq_iff"}],"representation":"每个 y∈U 的合法有限正半径集恰为 (0,|y|]，故点态零化半径=|y|>0。","dependencies":["CH03-D04","CH03-P10-01"]},
{"id":"CH03-P10-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.RealLine.step_uniform_zero"},{"file":"Main.lean","name":"MGC003.RealLine.counterexample3_1"},{"file":"Main.lean","name":"MGC003.RealLine.counterexample3_1_not_general"}],"representation":"step_uniform_zero：取趋零基点 t=min(1,ε) 得 uniformNullRadius=0；counterexample3_1 汇总：合法规范、stepOp(⊥)=⊥、U⊆dom、⊥∉U、每个 y∈U 的点态半径为 |y|>0、统一半径为 0；RealLine.counterexample3_1_not_general 把‘处处正的点态零化半径未必有正的统一下界’写成对一切单分量空间、算子与评估域的全称命题的否定。","dependencies":["CH03-D04","CH03-D05","CH03-P10-01","CH03-P10-02"]},
{"id":"CH03-P11-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_8_i_a"}],"representation":"J⊆Iconst(ϕ|U) 时 ∀y∈U，Fib_J(ϕ y|U)=U。","dependencies":["CH03-D01","CH03-D02"]},
{"id":"CH03-P11-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_8_i_b"}],"representation":"J⊆Iconst 时对任意输入分量 i，点态半径 nullRadiusJ=⊤ 且统一半径 uniformNullRadiusJ=⊤。","dependencies":["CH03-D01","CH03-D02","CH03-D04","CH03-D05"]},
{"id":"CH03-P11-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.TwoPt.prop3_8_ii_example"},{"file":"Main.lean","name":"MGC003.TwoPt.constPM"},{"file":"Main.lean","name":"MGC003.TwoPt.constPM_epm"},{"file":"Main.lean","name":"MGC003.TwoPt.cc"},{"file":"Main.lean","name":"MGC003.TwoPt.dd"},{"file":"Main.lean","name":"MGC003.TwoPt.dd_gauge"},{"file":"Main.lean","name":"MGC003.TwoPt.Uab"},{"file":"Main.lean","name":"MGC003.TwoPt.prop3_8_ii_example_eq"},{"file":"Main.lean","name":"MGC003.TwoPt.prop3_8_ii_example_ne"},{"file":"Main.lean","name":"MGC003.TwoPt.dd_values"},{"file":"Main.lean","name":"MGC003.TwoPt.Uab_dom"},{"file":"Main.lean","name":"MGC003.TwoPt.none_not_mem_Uab"},{"file":"Main.lean","name":"MGC003.TwoPt.prop3_8_ii_not_general"},{"file":"Main.lean","name":"MGC003.TwoPt.prop3_8_ii_not_general_ne"}],"representation":"两点空间 Option Bool、恒等算子；任意指标类型 I（DecidableEq）与任意 i,j：分量 i 上 d(a,b)=⊤，j≠i 时 d_j(a,b)=1，其余分量 0（TwoPt.cc/dd，dd_gauge 验证每个分量均为合法扩展伪度量，⊥ 孤立）；prop3_8_ii_example 证明对每个 y∈U 点态半径为 ⊤、nullMatrix j i=⊤，而 j∉Iconst（含 i=j 分支，此时 d_j(a,b)=⊤≠0）；prop3_8_ii_example_eq / prop3_8_ii_example_ne 分别显式给出 i=j 与 i≠j 两个分支（TwoPt.dd_values：d_i(a,b)=⊤，i≠j 时 d_j(a,b)=1），并包含 U⊆dom id、⊥∉U 的合法性；TwoPt.prop3_8_ii_not_general（i=j 分支）与 TwoPt.prop3_8_ii_not_general_ne（i≠j 分支）把‘[N(ϕ)|_U]_{ji}=+∞ 一般不推出 j∈I_const(ϕ|U)’写成全称命题的否定。","dependencies":["CH03-D01","CH03-D04","CH03-D05"]},
{"id":"CH03-P12-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_9_i"}],"representation":"i∈Iid(ϕ|U)、y∈U 时 Fib_{i}(ϕ y|U)={x∈U|d_i(x,y)=0}。","dependencies":["CH03-D01","CH03-D02","CH03-P01-03"]},
{"id":"CH03-P12-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_9_ii"}],"representation":"有限正 r₀ 使 B_i(y,r₀)∩U⊆输入零距类时，nullRadius(d_i,d_i)(y|U)≥r₀>0。","dependencies":["CH03-D01","CH03-D04","CH03-P01-03"]},
{"id":"CH03-P13-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_10_pointwise"},{"file":"Main.lean","name":"MGC003.nullRadiusJ_eq_iInf"}],"representation":"J 非空：点态半径 nullRadiusJ=⨅_{j∈J}nullRadius_j，且该下确界在某个 j∈J 处取到（有限非空最小值）。","dependencies":["CH03-D02","CH03-D04","CH03-P14-02"]},
{"id":"CH03-P13-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_10_uniform"}],"representation":"统一半径 uniformNullRadiusJ=⨅_{j∈J}nullMatrix j i（交换基点 inf 与有限 min），并在某个 j 取到。","dependencies":["CH03-D04","CH03-D05","CH03-P13-01"]},
{"id":"CH03-P13-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_10_anti"}],"representation":"J⊆K（J 非空）时 uniformNullRadiusJ(K)≤uniformNullRadiusJ(J)。","dependencies":["CH03-D05","CH03-P13-02"]},
{"id":"CH03-P14-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_11_a"}],"representation":"y'∈Fib_{ϕ₂,j}(ϕ₂ y|U₂) ⟹ d_j(ϕ₂ y,ϕ₂ y')=0。","dependencies":["CH03-D02"]},
{"id":"CH03-P14-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_11_b"},{"file":"Main.lean","name":"MGC003.zero_of_lt_nullRadius"}],"representation":"d_i(y,y')<nullRadius(y|U₂)、y'∈U₂ ⟹ d_j(ϕ₂ y,ϕ₂ y')=0（由 sSup 取得合法有限正半径）。","dependencies":["CH03-D04"]},
{"id":"CH03-P14-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_11_c"}],"representation":"复合输入实例：ϕ₁x,ϕ₁x'∈U₂ 且 ϕ₁x'∈Fib_{ϕ₂,j}(ϕ₂(ϕ₁x)|U₂) ⟹ d_j((ϕ₂∘ϕ₁)x,(ϕ₂∘ϕ₁)x')=0。","dependencies":["CH03-D02","CH03-P14-01"]},
{"id":"CH03-P15-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_12_i"}],"representation":"下游在实际像域 ϕ₁(U) 上 d_l-零距⟹d_j-零距时 nullMatrix(ϕ₁) l i ≤ nullMatrix(ϕ₂∘ϕ₁) j i。","dependencies":["CH03-D04","CH03-D05","CH03-P14-02"]},
{"id":"CH03-P15-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_12_ii"}],"representation":"L∈(0,∞)，d_l(ϕ₁x,ϕ₁x')≤L·d_i(x,x')（U 上）⟹ nullMatrix(ϕ₂|ϕ₁(U)) j l / L ≤ nullMatrix(ϕ₂∘ϕ₁|U) j i；右端 0/⊤ 由 ENNReal 除法统一处理","dependencies":["CH03-D04","CH03-D05","CH03-P14-02"]},
{"id":"CH03-P16-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.lemma3_13_cells"}],"representation":"thresholdType 的四种取值各自等价于对应不等式组合，四种组合互斥且穷尽。","dependencies":["CH03-D05","CH03-D06"]},
{"id":"CH03-P16-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.lemma3_13_i"}],"representation":"τσ≤τσ' 时第一项为 true 的通道集合单调不减。","dependencies":["CH03-D06"]},
{"id":"CH03-P16-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.lemma3_13_ii"}],"representation":"τN≤τN' 时第二项为 true 的通道集合单调不增。","dependencies":["CH03-D05","CH03-D06"]},
{"id":"CH03-P17-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_14_i"}],"representation":"任意输入尺度函数族：B⊆A、B 非空时 σ_i(B)≤σ_i(A)，且 σ_i(A)<τσ⟹σ_i(B)<τσ。","dependencies":["CH03-D06"]},
{"id":"CH03-P17-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_14_ii_a"},{"file":"Main.lean","name":"MGC003.nullRadius_mono_domain"}],"representation":"B⊆A 且基点 x∈B：nullRadius(x|A)≤nullRadius(x|B)。","dependencies":["CH03-D04"]},
{"id":"CH03-P17-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_14_ii_b"}],"representation":"∅≠B⊆A⊆dom f：nullMatrix(f|A) j i ≤ nullMatrix(f|B) j i（同时缩小评估域与基点集合）。","dependencies":["CH03-D04","CH03-D05","CH03-P17-02"]},
{"id":"CH03-P17-04","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.RealLine.prop3_14_iii"},{"file":"Main.lean","name":"MGC003.RealLine.prop3_14_iii_neg"}],"representation":"A={0,1}⊇B={0}（f=id，τσ=1/2，直径尺度，带吸收元的通常实线 dR）：σ(B)=0<1/2 而 σ(A)=1≥1/2，且 A⊆dom(id)，反向判断不成立；RealLine.prop3_14_iii_neg 把‘反向尺度判断不成立’写成全称命题的否定（B⊆A 非空、σ(B)<τσ 不蕴含 σ(A)<τσ）。","dependencies":["CH03-D06","CH03-P10-01"]},
{"id":"CH03-P18-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_15_i"}],"representation":"x,y∈A、d_i(x,y)<nullMatrix(f|A) j i ⟹ d_j(f x,f y)=0。","dependencies":["CH03-D04","CH03-D05","CH03-P14-02"]},
{"id":"CH03-P18-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_15_ii"}],"representation":"d_j(f x,f y)>0 ⟹ nullMatrix(f|A) j i ≤ d_i(x,y)（(i) 的逆否）。","dependencies":["CH03-D05","CH03-P18-01"]},
{"id":"CH03-P18-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_15_iii"}],"representation":"r̲<α<τN（α 有限）：存在 x,y∈A 与 NNReal ε>0 使 d_i(x,y)<α 且 ε≤d_j(f x,f y)（输出距离为 ⊤ 时取 ε=1，否则取 min(1,距离)）。","dependencies":["CH03-D04","CH03-D05"]},
{"id":"CH03-P19-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_16_i"}],"representation":"τN∈(0,∞)、τN≤nullMatrix(f|A) j i：∀x∈A，B_i(x,τN)∩A⊆Fib_{f,{j}}(f x|A)。","dependencies":["CH03-D02","CH03-D05","CH03-P18-01"]},
{"id":"CH03-P19-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_16_ii_a"},{"file":"Main.lean","name":"MGC003.prop3_16_net"}],"representation":"任意 B⊆A（含空集、无有限覆盖）：covering_number d_j ε f(B) ≤ covering_number d_i τN B；prop3_16_net 显式构造内部输出中心集 f(S)（中心数不增）","dependencies":["CH03-D02","CH03-D05","CH03-D07","CH03-P19-01"]},
{"id":"CH03-P19-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_16_ii_b"}],"representation":"B 非空时由 log2 单调得 metric_entropy d_j ε f(B) ≤ metric_entropy d_i τN B。","dependencies":["CH03-D05","CH03-D07","CH03-P19-02"]},
{"id":"CH03-P20-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.RealLine.pointwise_not_uniform"},{"file":"Main.lean","name":"MGC003.RealLine.two_point_cover"},{"file":"Main.lean","name":"MGC003.RealLine.no_positive_scale_for_covering"}],"representation":"同一阶跃例（stepOp、Ustep、dR）上，对任意有限正 τ 取 a=min(1,τ/4)（0<a≤1,2a<τ），B={-a,a}⊆U：输入覆盖数 𝒩(τ,B)=1，输出 𝒩(1/2,f(B))=2（two_point_cover 的下界通过对内部中心集的案例分析给出），故 1<2；RealLine.no_positive_scale_for_covering 给出其明确结论：不存在有限正 τ 使 𝒩(1/2,f(B)) ≤ 𝒩(τ,B) 对所有 B⊆U 同时成立（而每点的零化半径均为正，见 counterexample3_1）。","dependencies":["CH03-D07","CH03-P10-01"]},
{"id":"CH03-P21-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.cor3_17_iff"},{"file":"Main.lean","name":"MGC003.cor3_17_type"}],"representation":"diam_{d_i}(A)<τσ≤τN（τσ,τN 有限正）：nullMatrix≥τN ⇔ ∀x,y∈A d_j(f x,f y)=0（反向用 nullRadius_eq_top_of_zero 得 ⊤）；cor3_17_type 给出推论后的说明：此时 Type_{f,A}(i,j) 的第一项为 1，第二项为 1 当且仅当整个局部像落入同一个 d_j-零距类。","dependencies":["CH03-D04","CH03-D05","CH03-D06","CH03-P18-01"]},
{"id":"CH03-P21-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.cor3_17_cover"}],"representation":"等价条件成立且 A 非空：任意有限正 ε，covering_number d_j ε f(A)=1。","dependencies":["CH03-D05","CH03-D06","CH03-D07","CH03-P21-01"]},
{"id":"CH03-P22-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.note_finite_entropy_diff"}],"representation":"非空有限 U（及任意两端子族、有限正 ε）：两端子族覆盖数均 ≥1 且 <⊤，熵为实数 a,b，mapEntropyDiff=(a−b:ℝ)，MapEntropyDiffDefined 成立。","dependencies":["CH03-D02","CH03-D07","CH03-D08"]},
{"id":"CH03-P23-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_18_i"}],"representation":"j∈Iconst：输出覆盖数=1、熵=0、熵差良定且 mapEntropyDiff=metric_entropy(U)（x−0=x，输入熵可为 ⊤）。","dependencies":["CH03-D01","CH03-D07","CH03-D08"]},
{"id":"CH03-P23-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_18_ii_a"}],"representation":"j∈Iid：覆盖数 ϕ(U) 与 U 相等（前向推中心；反向对每个像中心用 Classical.choose 选代表元），熵相等。","dependencies":["CH03-D01","CH03-D07","CH03-P01-03"]},
{"id":"CH03-P23-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_18_ii_b"}],"representation":"j∈Iid 且 MapEntropyDiffDefined 成立时 mapEntropyDiff=0；不定义 ∞−∞。","dependencies":["CH03-D01","CH03-D07","CH03-D08","CH03-P23-02"]},
{"id":"CH03-P24-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_19_cover"},{"file":"Main.lean","name":"MGC003.prop3_19_net"}],"representation":"L∈(0,∞) 的单通道 Lip 上界：U 的内部 ε/L-中心集的像是 ϕ(U) 的内部 ε-中心集（中心数不增），故 𝒩_j(ε,ϕ(U))≤𝒩_i(ε/L,U)。","dependencies":["CH03-D07"]},
{"id":"CH03-P24-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_19_entropy"}],"representation":"U 在 d_i 下全有界：三个覆盖数 ≥1 且有限，熵为实数，MapEntropyDiffDefined 成立，且 E_ε(U)−E_{ε/L}(U) ≤ mapEntropyDiff。","dependencies":["CH03-D07","CH03-D08","CH03-P24-01"]},
{"id":"CH03-P25-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_20_cover"},{"file":"Main.lean","name":"MGC003.prop3_20_net"}],"representation":"0<K_{i→j}<⊤ 的 co-Lip 条目：对输出内部 ε-中心集 T，对每个中心选原像代表元（Classical.choose）得 U 的内部 ε/K-中心集，中心数不增，故 𝒩_i(ε/K,U)≤𝒩_j(ε,ϕ(U))。","dependencies":["CH03-D07"]},
{"id":"CH03-P25-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.prop3_20_entropy"}],"representation":"U 全有界、输出熵可为 ⊤：MapEntropyDiffDefined 成立，且 mapEntropyDiff ≤ E_ε(U)−E_{ε/K}(U)（EReal 中对 e=⊥,实数,⊤ 分情形）。","dependencies":["CH03-D07","CH03-D08","CH03-P25-01"]},
{"id":"CH03-P26-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex31.ex3_1_i_a"},{"file":"Main.lean","name":"MGC003.Ex31.affOp"},{"file":"Main.lean","name":"MGC003.Ex31.affOp_some"},{"file":"Main.lean","name":"MGC003.Ex31.affOp2_some"},{"file":"Main.lean","name":"MGC003.Ex31.U"},{"file":"Main.lean","name":"MGC003.Ex31.U_dom"},{"file":"Main.lean","name":"MGC003.RealLine.dA"},{"file":"Main.lean","name":"MGC003.RealLine.dA_gauge"},{"file":"Main.lean","name":"MGC003.RealLine.dA_zero_iff"}],"representation":"绝对值读数伪度量 d_i(x,y)=||x|−|y||（⊥ 孤立；RealLine.dA 与 dA_gauge 验证其为合法扩展伪度量），仿射算子 φ(s)=2s−1（Ex31.affOp，φ(⊥)=⊥ 由 Operator 结构保证），U={0,1}（Ex31.U，U_dom 验证 U⊆dom φ 与 U⊆dom φ²）；φ(0)=−1,φ(1)=1，Fib_{φ,i}(φ(0)|U)=Fib_{φ,i}(φ(1)|U)=U，i∈Iconst，故 ∉Iid、∉Iact。","dependencies":["CH03-D01","CH03-D02"]},
{"id":"CH03-P26-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex31.ex3_1_i_b"}],"representation":"φ²(x)=4x−3：φ²(0)=−3,φ²(1)=1，Fib(φ²(0)|U)={0}、Fib(φ²(1)|U)={1}（纤维精确保留 U，并为 U 的分划），i∈Iact。","dependencies":["CH03-D01","CH03-D02","CH03-P26-01"]},
{"id":"CH03-P26-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex31.ex3_1_ii"},{"file":"Main.lean","name":"MGC003.Ex31.ex3_1_ii_branches"}],"representation":"ψ 在 U 上取同一值 c：ψ∘ψ(0)=ψ∘ψ(1)，任意纤维不分开 0,1；ψ(c)=⊥ 时 U⊄dom(ψ∘ψ)（再次像为吸收元，纤维定义不适用），ψ(c)≠⊥ 时 U⊆dom(ψ∘ψ)；两分支均有实例。","dependencies":["CH03-D02","CH03-P26-01"]},
{"id":"CH03-P27-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.ex3_2_i"}],"representation":"K i j>0（无需有限）、y∈U：d_i(x,y)∉(0,nullRadius(y|U))（正距离导致 K i j=0 的矛盾）。","dependencies":["CH03-D04","CH03-P14-02"]},
{"id":"CH03-P27-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.ex3_2_ii"}],"representation":"nullMatrix j i>0 且 K i j>0：∀x,y∈U，d_i(x,y)∈{0}∪[nullMatrix,∞]。","dependencies":["CH03-D05","CH03-P18-01"]},
{"id":"CH03-P28-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex33.ex3_3_i_id"},{"file":"Main.lean","name":"MGC003.Ex33.ex3_3_i_shift"},{"file":"Main.lean","name":"MGC003.Ex33.shiftOp"},{"file":"Main.lean","name":"MGC003.Ex33.shiftOp_some"},{"file":"Main.lean","name":"MGC003.Ex33.shift_image"},{"file":"Main.lean","name":"MGC003.Ex33.U"},{"file":"Main.lean","name":"MGC003.Ex33.mem_U"},{"file":"Main.lean","name":"MGC003.Ex33.U_dom"}],"representation":"d_i=||x|−|y||（沿用 RealLine.dA/dA_gauge 的合法性验证）；U={−3,−2,0,2}（Ex33.U）；Ex33.U_dom 验证 U⊆dom(id)、U⊆dom(shiftOp)；恒等算子纤维 {−3},{−2,2},{0}；平移 shiftOp(x)=x+1 的纤维 {−3},{−2,0},{2}（ex3_3_i_id/ex3_3_i_shift 同时给出纤维族等于分划）；shift_image：φ(U)={−2,−1,1,3}。","dependencies":["CH03-D02","CH03-P26-01"]},
{"id":"CH03-P28-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex33.ex3_3_ii"},{"file":"Main.lean","name":"MGC003.RealLine.dA_lt_iff"},{"file":"Main.lean","name":"MGC003.RealLine.dA_ge_iff"}],"representation":"ε=3/2：𝒩_i(ε,U)=2（上界取 {−3,0}，下界用 two_le_card_of_net），𝒩_i(ε,φ(U))=1（{−2}），ΔE=1−0=1。","dependencies":["CH03-D07","CH03-D08","CH03-P26-01","CH03-P28-01"]},
{"id":"CH03-P29-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex34.ex3_4_i_a"},{"file":"Main.lean","name":"MGC003.Ex34.floorOp"},{"file":"Main.lean","name":"MGC003.Ex34.floorOp_some"},{"file":"Main.lean","name":"MGC003.Ex34.floor_dom"},{"file":"Main.lean","name":"MGC003.Ex34.dR_floor_zero_iff"},{"file":"Main.lean","name":"MGC003.Ex34.diam_Icc"},{"file":"Main.lean","name":"MGC003.Ex34.nullRadius_floor_one"},{"file":"Main.lean","name":"MGC003.Ex34.uniform_floor_zero"},{"file":"Main.lean","name":"MGC003.Ex34.nullRadius_top_of_floor_const"}],"representation":"取整算子 floorOp（f(⊥)=⊥ 由 Operator 结构保证）、通常实线 dR（合法性 RealLine.dR_gauge）、直径尺度与 τσ=τN=1；D=[0,1/2]：D⊆dom floorOp（floor_dom），diam=1/2（diam_Icc），f 在 D 上取值恒为 0 故 nullMatrix=⊤（nullRadius_top_of_floor_const），类型 (true,true)。floorOp 的辅助引理 nullRadius_floor_one/uniform_floor_zero 供 (i-b)(i-d) 使用。","dependencies":["CH03-D04","CH03-D05","CH03-D06","CH03-P10-01"]},
{"id":"CH03-P29-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex34.ex3_4_i_b"}],"representation":"D=[9/10,11/10]：diam=1/5，nullMatrix=0，类型 (true,false)。","dependencies":["CH03-D05","CH03-D06","CH03-P10-01","CH03-P29-01"]},
{"id":"CH03-P29-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex34.ex3_4_i_c"}],"representation":"D={0,2}：diam=2，nullMatrix=2，类型 (false,true)。","dependencies":["CH03-D04","CH03-D05","CH03-D06","CH03-P10-01","CH03-P29-01"]},
{"id":"CH03-P29-04","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex34.ex3_4_i_d"}],"representation":"D=[0,2]：diam=2，nullMatrix=0，类型 (false,false)。","dependencies":["CH03-D05","CH03-D06","CH03-P10-01","CH03-P29-01"]},
{"id":"CH03-P29-05","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex34.ex3_4_ii"}],"representation":"否定“nullMatrix≥1⟹整体零化”：D={0,2} 满足 nullMatrix=2≥1 但 d(f0,f2)≠0；正半径来自不同点距离≥2（孤立），直径 2≥τσ=1，推论 3.17 条件不满足。","dependencies":["CH03-D05","CH03-D06","CH03-P10-01","CH03-P29-01","CH03-P29-03"]},
{"id":"CH03-P30-01","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex35.cover_U"},{"file":"Main.lean","name":"MGC003.Ex35.cover_U_of_finite"},{"file":"Main.lean","name":"MGC003.Ex35.cover_seven_fourths"},{"file":"Main.lean","name":"MGC003.Ex35.cover_le_two"},{"file":"Main.lean","name":"MGC003.Ex35.cover_le_one"},{"file":"Main.lean","name":"MGC003.Ex35.cover_gt_two"},{"file":"Main.lean","name":"MGC003.Ex35.U"},{"file":"Main.lean","name":"MGC003.Ex35.mem_U"},{"file":"Main.lean","name":"MGC003.Ex35.mem_U'"},{"file":"Main.lean","name":"MGC003.Ex35.mem_pts"},{"file":"Main.lean","name":"MGC003.Ex35.dist_ge_one"},{"file":"Main.lean","name":"MGC003.Ex35.dR_lt_iff"},{"file":"Main.lean","name":"MGC003.Ex35.dR_ge_iff"},{"file":"Main.lean","name":"MGC003.Ex35.dR_gauge'"},{"file":"Main.lean","name":"MGC003.Ex35.cover_U_piecewise"}],"representation":"实线 dR（合法性 RealLine.dR_gauge，另有 Ex35.dR_gauge'）、U={0,1,2,3}（Ex35.U，mem_U/mem_U'/mem_pts 为元素刻画）；𝒩(ε,U)=4(ε≤1)，2(1<ε≤2)，1(ε>2)（cover_le_one/cover_le_two/cover_gt_two，cover_U 与 cover_U_of_finite 汇总所有有限正 ε，端点 ε=1,2 属前一段）；ε=7/4 时为 2，3/2∉U 故 {3/2} 不是合法内覆盖（但其球覆盖 U，cover_seven_fourths）；Ex35.cover_U_piecewise 显式写出分段结果及端点：ε=1 时 4，ε=2 时 2。","dependencies":["CH03-D07","CH03-P10-01"]},
{"id":"CH03-P30-02","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex35.ex3_5_ii"},{"file":"Main.lean","name":"MGC003.Ex35.f_image"},{"file":"Main.lean","name":"MGC003.Ex35.g_image"},{"file":"Main.lean","name":"MGC003.Ex35.fOp"},{"file":"Main.lean","name":"MGC003.Ex35.gOp"},{"file":"Main.lean","name":"MGC003.Ex35.fFun"},{"file":"Main.lean","name":"MGC003.Ex35.gFun"},{"file":"Main.lean","name":"MGC003.Ex35.fOp_some"},{"file":"Main.lean","name":"MGC003.Ex35.gOp_some"},{"file":"Main.lean","name":"MGC003.Ex35.U_sub_dom_f"},{"file":"Main.lean","name":"MGC003.Ex35.U_sub_dom_g"},{"file":"Main.lean","name":"MGC003.Ex35.fOp_eq_none_of_not_mem"},{"file":"Main.lean","name":"MGC003.Ex35.gOp_eq_none_of_not_mem"}],"representation":"f(x)=x（U 上）、g：0→0,1→3,2→1,3→2，二者在 𝒳∖U 上取 ⊥（Ex35.fOp/gOp；U_sub_dom_f/g 验证 U⊆dom）；f(U)=g(U)=U（f_image/g_image），任意有限正 ε 覆盖数相同，两算子映射熵差均为 0（ex3_5_ii）；fOp_eq_none_of_not_mem / gOp_eq_none_of_not_mem 证明两算子在 𝒳∖U 上取吸收元 ⊥（题设）。","dependencies":["CH03-D07","CH03-D08","CH03-P10-01","CH03-P30-01"]},
{"id":"CH03-P30-03","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex35.f_lip"},{"file":"Main.lean","name":"MGC003.Ex35.f_lip_least"},{"file":"Main.lean","name":"MGC003.Ex35.g_lip"},{"file":"Main.lean","name":"MGC003.Ex35.g_lip_least"}],"representation":"用背景 HasScalarLipBound：f 的最优标量 Lip 常数为 1，g 为 3（IsLeast；必要下界由点对 (0,1) 给出）。","dependencies":["CH03-P10-01","CH03-P30-01","CH03-P30-02"]},
{"id":"CH03-P30-04","status":"complete","declarations":[{"file":"Main.lean","name":"MGC003.Ex35.ex3_5_iii_b"},{"file":"Main.lean","name":"MGC003.Ex35.ex3_5_iii_entropy"},{"file":"Main.lean","name":"MGC003.Ex35.div_ofReal"}],"representation":"ε=7/4：命题 3.19 的覆盖数上界 f:𝒩(7/4,U)=2（与真实值相等），g:𝒩(7/12,U)=4（严格大于真实值 2）；熵层面 E(ε)−E(ε/L)=0 与 −1。","dependencies":["CH03-D07","CH03-D08","CH03-P10-01","CH03-P24-01","CH03-P30-01","CH03-P30-02","CH03-P30-03"]}
]}