{"case_id":"MG-C003","version":"0.1.1","items":[
{"id":"CH03-D01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.Iconst"},{"file":"Main.lean","name":"OETCh03.Iid"},{"file":"Main.lean","name":"OETCh03.Iact"},{"file":"Main.lean","name":"OETCh03.IconstG"},{"file":"Main.lean","name":"OETCh03.IidG"},{"file":"Main.lean","name":"OETCh03.IactG"},{"file":"Main.lean","name":"OETCh03.mem_Iact_iff"},{"file":"Main.lean","name":"OETCh03.not_mem_Iact_iff"},{"file":"Main.lean","name":"OETCh03.component_partition"},{"file":"Main.lean","name":"OETCh03.not_mem_Iconst_iff"}],"representation":"Iconst/Iid/Iact d ϕ U : Set I。I_const 为 U 内输出两两 d_i 零距；I_id 显式要求 i∉I_const（常值优先）且 ∀x∈U, d_i(ϕx,x)=0；I_act = univ \\ (I_const ∪ I_id)（I 用 univ 表示）。U⊆dom ϕ 作为各定理前提；IconstG/IidG/IactG 为 U=dom ϕ 的全域分划；component_partition 证明三类两两不交且并为 I；mem_Iact_iff/not_mem_Iact_iff/not_mem_Iconst_iff 为成员刻画。","dependencies":[]},
{"id":"CH03-D02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.Fib"},{"file":"Main.lean","name":"OETCh03.Fib1"},{"file":"Main.lean","name":"OETCh03.FibG"},{"file":"Main.lean","name":"OETCh03.mem_Fib_iff"},{"file":"Main.lean","name":"OETCh03.Fib_singleton"},{"file":"Main.lean","name":"OETCh03.Fib_eq_empty_of_pos"}],"representation":"Fib d ϕ J y U = {x | x∈U ∧ d_J(ϕx,y)=0}，d_J 为冻结的 subfamily_pseudometric（子族逐点上确界，有限非空时即 max）；目标 y∈X 任意；Fib1 为单分量 Fib_{ϕ,j}；Fib_singleton 证明 J={j} 时二者相等；FibG 为 U=dom ϕ 的全域纤维。Fib_eq_empty_of_pos 证明目标与 ϕ(U) 中每点都有正 d_J-距离时相应纤维为空。","dependencies":["CH03-D07"]},
{"id":"CH03-D03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.Req"},{"file":"Main.lean","name":"OETCh03.Rsim"},{"file":"Main.lean","name":"OETCh03.mem_Rsim_iff_mem_Fib"},{"file":"Main.lean","name":"OETCh03.Req_subset_Rsim"},{"file":"Main.lean","name":"OETCh03.gaugeSetoid"},{"file":"Main.lean","name":"OETCh03.ImageQuot"},{"file":"Main.lean","name":"OETCh03.imgCls"},{"file":"Main.lean","name":"OETCh03.imgCls_eq_iff"},{"file":"Main.lean","name":"OETCh03.fiberGE"},{"file":"Main.lean","name":"OETCh03.fiberGE_iff_Fib_subset"}],"representation":"Req ϕ U / Rsim d ϕ U : Set (X×X) 为 U×U 中 ϕ 点值相等 / 族零距 GaugeZeroRelated 的点对；mem_Rsim_iff_mem_Fib 证明 (x,y)∈R_∼ ↔ y∈Fib_{ϕ,I}(ϕx|U)（I=univ）；gaugeSetoid 由第1章引理1.1 给出等价关系，ImageQuot 为实际像集子类型 ϕ(U) 上限制该 setoid 的 Quotient，imgCls 为类 [ϕ(x)]；fiberGE d U ϕA ϕB :⇔ R_∼(ϕA|U) ⊆ R_∼(ϕB|U)（即 ϕA ⪰_{fiber,U} ϕB）。fiberGE_iff_Fib_subset 证明 ϕA ⪰_{fiber,U} ϕB ↔ ∀x∈U, Fib_{ϕA,I}(ϕA x|U) ⊆ Fib_{ϕB,I}(ϕB x|U)，即 ϕA 的零测距纤维分划细于或等于 ϕB 的分划（与商映射存在的等价见 P08-01）。","dependencies":["CH03-D02","CH03-D07"]},
{"id":"CH03-D04","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.admRadii"},{"file":"Main.lean","name":"OETCh03.nullRadius"},{"file":"Main.lean","name":"OETCh03.nullRadiusG"},{"file":"Main.lean","name":"OETCh03.rNJ"},{"file":"Main.lean","name":"OETCh03.rN"},{"file":"Main.lean","name":"OETCh03.rNJ_singleton"},{"file":"Main.lean","name":"OETCh03.zeroSet_eq_Fib"},{"file":"Main.lean","name":"OETCh03.zeroSet_eq_Fib1"},{"file":"Main.lean","name":"OETCh03.admRadii_mono"},{"file":"Main.lean","name":"OETCh03.le_nullRadius"},{"file":"Main.lean","name":"OETCh03.exists_adm_of_lt_nullRadius"},{"file":"Main.lean","name":"OETCh03.zero_of_lt_nullRadius"},{"file":"Main.lean","name":"OETCh03.le_nullRadius_of_forall"},{"file":"Main.lean","name":"OETCh03.nullRadius_eq_top_of_forall"},{"file":"Main.lean","name":"OETCh03.nullRadius_of_admRadii_empty"}],"representation":"admRadii d_in d_out ϕ y U = {r : ENNReal | 0<r ∧ r<⊤ ∧ ball d_in y r ∩ U ⊆ {x | x∈U ∧ d_out(ϕx,ϕy)=0}}（ball 为第1章开球 {x | d_in(x,y)<r}，r 取有限正值）；nullRadius = sSup admRadii，ENNReal 中 sSup ∅ = 0（nullRadius_of_admRadii_empty）、可取 ⊤；rNJ/rN 为 r^N_{ϕ,i,J}=r^N_{ϕ,d_i,d_J} 与 r^N_{ϕ,i,j} 简写，rNJ_singleton 证明 J={j} 一致；zeroSet_eq_Fib 证明输出零测距集即 Fib_{ϕ,J}(ϕy|U)；nullRadiusG 为全域简写；其余为上确界的基本接口引理。U 非空、y∈U、U⊆dom ϕ 作为定理前提。","dependencies":["CH03-D02","CH03-D07"]},
{"id":"CH03-D05","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.uniformNullRadius"},{"file":"Main.lean","name":"OETCh03.uNR"},{"file":"Main.lean","name":"OETCh03.uNRG"},{"file":"Main.lean","name":"OETCh03.nullMatrix"},{"file":"Main.lean","name":"OETCh03.nullMatrixG"},{"file":"Main.lean","name":"OETCh03.uniform_le_nullRadius"},{"file":"Main.lean","name":"OETCh03.le_uniform"}],"representation":"uniformNullRadius d_in d_out ϕ A U = ⨅ y∈A, nullRadius(y|U)（A 为基点集合、U 为评估域）；uNR 为 A=U 简写，uNRG 为 A=U=dom ϕ；nullMatrix d ϕ U j i := uNR (d i) (d j) ϕ U，第一参数 j 为输出（行）、第二参数 i 为输入（列），与 [N(ϕ)|_U]_{ji} 一致；nullMatrixG 为全域零化矩阵；U≠∅ 约定作为定理前提。","dependencies":["CH03-D04"]},
{"id":"CH03-D06","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.InputScaleFamily"},{"file":"Main.lean","name":"OETCh03.diam"},{"file":"Main.lean","name":"OETCh03.diam_mono"},{"file":"Main.lean","name":"OETCh03.le_diam"},{"file":"Main.lean","name":"OETCh03.diamScale"},{"file":"Main.lean","name":"OETCh03.thresholdType"},{"file":"Main.lean","name":"OETCh03.thresholdType_fst_eq_one"},{"file":"Main.lean","name":"OETCh03.thresholdType_snd_eq_one"},{"file":"Main.lean","name":"OETCh03.InputScaleFamily.ofNonempty"},{"file":"Main.lean","name":"OETCh03.InputScaleFamily.ofNonempty_eq"},{"file":"Main.lean","name":"OETCh03.InputScaleFamily.restrict_mono"}],"representation":"InputScaleFamily X I：σ : I → Set X → ENNReal 与单调性 ∀i A₁ A₂, A₁ 非空 → A₁⊆A₂ → σ i A₁ ≤ σ i A₂（空集上的值不进入任何陈述）；表示对应：InputScaleFamily.ofNonempty 由仅定义在非空子集 {A // A.Nonempty} 上的单调族构造本结构且 ofNonempty_eq 证明在每个非空子集上取回原值，restrict_mono 证明反向限制仍为原文意义的单调族；diam d A = ⨆_{x,y∈A} d x y，diamScale 为默认直径尺度族；thresholdType σ τσ τN d f A i j : Fin 2 × Fin 2 = (1{σ_i(A)<τσ}, 1{τN ≤ r̲^N_{f,i,j}|_A})；两阈值有限正性在使用处作前提。","dependencies":["CH03-D05"]},
{"id":"CH03-D07","status":"complete","declarations":[{"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.subfamily_pseudometric"},{"file":"formal_oet/vol_01/ch_01_foundations/metric_entropy.lean","name":"formal_oet.vol_01.ch_01_foundations.log2_ereal"},{"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":"Main.lean","name":"OETCh03.TotallyBoundedIn"},{"file":"Main.lean","name":"OETCh03.covering_entropy_interface"},{"file":"Main.lean","name":"OETCh03.covering_number_le_card"},{"file":"Main.lean","name":"OETCh03.covering_number_ne_zero"},{"file":"Main.lean","name":"OETCh03.metric_entropy_real"},{"file":"Main.lean","name":"OETCh03.metric_entropy_mono_cov"},{"file":"Main.lean","name":"OETCh03.log2_ereal_mono"},{"file":"Main.lean","name":"OETCh03.log2_ereal_one"},{"file":"Main.lean","name":"OETCh03.log2_ereal_natCast"},{"file":"Main.lean","name":"OETCh03.log2_ereal_lt_top"},{"file":"Main.lean","name":"OETCh03.subfamily_pseudometric_eq_zero_iff"},{"file":"Main.lean","name":"OETCh03.subfamily_pseudometric_eq_max"},{"file":"Main.lean","name":"OETCh03.two_le_covering_number"},{"file":"Main.lean","name":"OETCh03.covering_number_le_one"},{"file":"Main.lean","name":"OETCh03.covering_number_le_two"},{"file":"Main.lean","name":"OETCh03.card_le_covering_number_of_isolated"}],"representation":"直接复用冻结定义：InternalEpsilonNet（有限中心⊆U 且每点 d(x,c)<ε，即 U⊆⋃ B(s,ε)）、covering_number（iInf 实现）、metric_entropy=log2_ereal∘覆盖数、子族版本以 d_J 代入（subfamily_pseudometric_eq_max 证明有限非空 J 上冻结的上确界实现由某 j∈J 取到，即 d_J = max_{j∈J} d_j）。covering_entropy_interface 证明对应：存在有限内覆盖时由某中心集取到且最小；否则为 ⊤；空集为 0；非空 ≥1；熵即 log₂ 覆盖数；非空熵 ≥0；空集熵 = ⊥(−∞)；J={i} 时子族覆盖数/熵退化为单分量。TotallyBoundedIn d U :⇔ ∀ r, 0<r<⊤ → N(r,U)<⊤；另含 log₂ 单调、有限正覆盖数熵为实数等接口，以及具体计算所用的覆盖数上下界工具（covering_number_le_card/le_one/le_two、two_le_covering_number、card_le_covering_number_of_isolated）。","dependencies":[]},
{"id":"CH03-D08","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.EntropyDiffDomain"},{"file":"Main.lean","name":"OETCh03.mapEntropyDiff"},{"file":"Main.lean","name":"OETCh03.mapEntropyDiff_cases"},{"file":"Main.lean","name":"OETCh03.mapEntropyDiff_single"},{"file":"Main.lean","name":"OETCh03.entropyDiffDomain_single"}],"representation":"EntropyDiffDomain d J_in J_out ε ϕ U 打包原文全部前提（U 非空、U⊆dom ϕ、两端子族非空、0<ε<⊤、N_{J_in}(ε,U)<⊤ ∨ N_{J_out}(ε,ϕ(U))<⊤）；mapEntropyDiff 仅在给出该证明时定义为 EReal 中 E_{ε,J_in}(U) − E_{ε,J_out}(ϕ(U))，因而从不对 +∞−+∞ 取值；mapEntropyDiff_cases 证明域内两端熵 ≥0、不同时为 ⊤，且 +∞−有限=+∞、有限−+∞=−∞、两端有限时为实数差；ΔE_{ε,i,j}、ΔE_{ε,J} 取 J_in={i},J_out={j} 等（mapEntropyDiff_single 化为单分量熵之差）。","dependencies":["CH03-D07"]},
{"id":"CH03-P01-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop31_i"}],"representation":"i∈Iconst d ϕ U、U⊆dom ϕ：∀x y∈U, d_i(ϕx,ϕy) ≤ Σ_k 0·d_k(x,y)，且该零行和为 0；并证明把任一合法受限 Lip 矩阵（IsLipMatrix，L k j 表示 L_{k→j}）的输出行 i 置零后仍合法。","dependencies":["CH03-D01"]},
{"id":"CH03-P01-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop31_ii"}],"representation":"i∈Iconst d ϕ U、K 满足 IsCoLipMatrix d ϕ U K（含 U 非空、U⊆dom ϕ）、源分量 k 存在 x y∈U 使 0<d_k(x,y) ⇒ K k i = 0（K_{k→i}=0）。","dependencies":["CH03-D01"]},
{"id":"CH03-P01-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop31_iii"}],"representation":"i∈Iid d ϕ U ⇒ ∀x y∈U, d_i(ϕx,ϕy)=d_i(x,y)，两方向均由三角不等式与 d_i(ϕz,z)=0 得到。","dependencies":["CH03-D01"]},
{"id":"CH03-P02-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop32_i"},{"file":"Main.lean","name":"OETCh03.mem_dom_mul"},{"file":"Main.lean","name":"OETCh03.image_subset_dom_of_subset_dom_mul"}],"representation":"复合 ϕ₂∘ϕ₁ 用幺半群乘法 ϕ₂*ϕ₁；前提 U⊆dom(ϕ₂*ϕ₁)；结论 Iact(ϕ₂*ϕ₁|U) ⊆ Iact(ϕ₁|U) ∪ Iact(ϕ₂|ϕ₁.func '' U)，第二步在实际中间像域上读取；证明取逆否并按 (a)–(d) 四情形；mem_dom_mul 证明 ϕ₁(U)⊆dom ϕ₂。","dependencies":["CH03-D01"]},
{"id":"CH03-P02-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.chainComp"},{"file":"Main.lean","name":"OETCh03.stepDom"},{"file":"Main.lean","name":"OETCh03.stepDom_eq_image"},{"file":"Main.lean","name":"OETCh03.Iact_chain_zero"},{"file":"Main.lean","name":"OETCh03.prop32_ii"},{"file":"Main.lean","name":"OETCh03.prop32_ii_contra"},{"file":"Main.lean","name":"OETCh03.chainComp_eq_prod"},{"file":"Main.lean","name":"OETCh03.chainComp_eq_OperatorChain"},{"file":"Main.lean","name":"OETCh03.finSeq"},{"file":"Main.lean","name":"OETCh03.finSeq_of_lt"},{"file":"Main.lean","name":"OETCh03.chainComp_finSeq"},{"file":"Main.lean","name":"OETCh03.prop32_ii_fin"}],"representation":"有限族 ϕ_1,…,ϕ_n 用 ϕ : ℕ → Operator 的前 n 项表示（0 起标号，ϕ m 为第 m+1 步）；表示对应：finSeq 把有限族 φ : Fin n → Operator 延拓为序列（越界项取 id），chainComp_finSeq 证明 chainComp (finSeq φ) n = (List.ofFn φ).reverse.prod = φ_n ∘ ⋯ ∘ φ_1，chainComp_eq_prod/chainComp_eq_OperatorChain 证明一般 chainComp ϕ n 即按复合顺序的幺半群乘积并与冻结 OperatorChain 一致，prop32_ii_fin 直接对 Fin n 有限族陈述 (ii)；chainComp ϕ n = ϕ(n−1)*⋯*ϕ 0，chainComp 0 = 1 = id；stepDom ϕ U m 递归给出实际域（U_1=U, U_{m+1}=ϕ_m(U_m)），stepDom_eq_image 证明它等于 c_m(U)；Iact_chain_zero 为零步基例 I_act(c_0|U)=∅；prop32_ii 对所有 n（含 0）在前提 U⊆dom(c_n) 下归纳证明 I_act(c_n|U) ⊆ ⋃_{m<n} I_act(ϕ m|U_m)；prop32_ii_contra 为“各步均非有效 ⇒ 复合非有效”。","dependencies":["CH03-D01","CH03-P02-01"]},
{"id":"CH03-P02-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop32_iii"}],"representation":"Iid(ϕ₁|U) ∩ Iid(ϕ₂|ϕ₁(U)) ⊆ Iid(ϕ₂*ϕ₁|U)，前提 U⊆dom(ϕ₂*ϕ₁)；证明中显式排除常值优先分支：由 ϕ₁ 非常值得到见证点对，再用 ϕ₂ 在实际像域上的保距（命题3.1(iii)）说明复合非常值。","dependencies":["CH03-D01","CH03-P01-03"]},
{"id":"CH03-P03-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.clsDist"},{"file":"Main.lean","name":"OETCh03.clsDist_epm"},{"file":"Main.lean","name":"OETCh03.P3"},{"file":"Main.lean","name":"OETCh03.dSwap"},{"file":"Main.lean","name":"OETCh03.dSwap_epm"},{"file":"Main.lean","name":"OETCh03.swap3"},{"file":"Main.lean","name":"OETCh03.U3"},{"file":"Main.lean","name":"OETCh03.swap3_mul"},{"file":"Main.lean","name":"OETCh03.swap3_image"},{"file":"Main.lean","name":"OETCh03.U3_sub_dom_swap"},{"file":"Main.lean","name":"OETCh03.swap_not_const"},{"file":"Main.lean","name":"OETCh03.swap_act"},{"file":"Main.lean","name":"OETCh03.swap_comp"},{"file":"Main.lean","name":"OETCh03.remark_swap"},{"file":"Main.lean","name":"OETCh03.remark_reverse_fails"},{"file":"Main.lean","name":"OETCh03.U3_sub_dom_swap1"}],"representation":"X={⊥,a,b}（归纳类型 P3），I=Unit，d(a,b)=1、自距 0、与 ⊥ 距 ⊤（clsDist_epm 验证四条公理与非吸收点）；swap3 交换 a,b 并保持 ⊥；证明 U⊆dom swap、swap(U)=U（第二步实际域即 U）、U⊆dom(swap²)、I_act(swap|U)={()}、I_id(swap|U)=∅、I_id(swap²|U)={()}、I_act(swap²|U)=∅，命题3.2(i)(iii) 两条包含均为真包含；remark_reverse_fails 否定两条逆向包含的全称命题。","dependencies":["CH03-D01"]},
{"id":"CH03-P04-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop33_i"}],"representation":"前提 U⊆dom(ψ*ϕ)；i∈Iconst d ψ (ϕ.func '' U)（外侧在实际像域上常值）⇒ i∈Iconst d (ψ*ϕ) U。","dependencies":["CH03-D01"]},
{"id":"CH03-P04-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.P7"},{"file":"Main.lean","name":"OETCh03.I2"},{"file":"Main.lean","name":"OETCh03.cls7"},{"file":"Main.lean","name":"OETCh03.d7"},{"file":"Main.lean","name":"OETCh03.d7_epm"},{"file":"Main.lean","name":"OETCh03.phi7"},{"file":"Main.lean","name":"OETCh03.psi7"},{"file":"Main.lean","name":"OETCh03.U7"},{"file":"Main.lean","name":"OETCh03.prop33_ii_example"},{"file":"Main.lean","name":"OETCh03.prop33_ii"}],"representation":"X={⊥,a,b,p,q,r,s}（P7），I={i,m}（I2）；d_i 由类函数把 q 并入 p（p,q 零距，其余不同点距 1），d_m 离散，均与 ⊥ 距 ⊤ 并验证扩展伪度量；ϕ(a)=p,ϕ(b)=q,ψ(p)=r,ψ(q)=s，其余取 ⊥；证明 U⊆dom ϕ、U⊆dom(ψ*ϕ)、d_i(p,q)=0、d_m(p,q)=1、d_i(r,s)=1、i∈I_const(ϕ|U)、i∉I_const(ψ*ϕ|U)；prop33_ii 否定“内侧常值 ⇒ 复合常值”的全称命题。","dependencies":["CH03-D01","CH03-P03-01"]},
{"id":"CH03-P05-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.cor34"}],"representation":"前提 U⊆dom(ψ*ϕ)、j∈Iconst d ϕ U、∃ L, IsLipMatrix d ψ (ϕ.func '' U) L ∧ ∀k≠j, L k j = 0（L_{j→j} 可为 ⊤，ENNReal 中 ⊤·0=0）⇒ j∈Iconst d (ψ*ϕ) U；使用冻结 lip_bound_of_single_input_row。","dependencies":["CH03-D01"]},
{"id":"CH03-P06-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop35_i"}],"representation":"任意目标 y,y'：d_J(y,y')=0 ⇒ Fib d ϕ J y U = Fib d ϕ J y' U（逐分量三角不等式与对称性）。","dependencies":["CH03-D02","CH03-D07"]},
{"id":"CH03-P06-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop35_ii_a"}],"representation":"∀y∈ϕ(U), Fib(y|U) 非空；∀x∈U, x∈Fib(ϕx|U)；且 ⋃_{y∈ϕ(U)} Fib(y|U) = U。","dependencies":["CH03-D02","CH03-D07"]},
{"id":"CH03-P06-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.IsPartitionOf"},{"file":"Main.lean","name":"OETCh03.Fib_eq_or_disjoint"},{"file":"Main.lean","name":"OETCh03.prop35_ii_b"}],"representation":"任意两纤维相等或不交（对像目标及任意目标均成立）；集合族 (fun y ↦ Fib(y|U)) '' ϕ(U)（Set (Set X)，自动去重）满足 IsPartitionOf U：成员非空且⊆U，U 中每点恰属于一个成员（∃!）。","dependencies":["CH03-D02","CH03-D07","CH03-P06-01","CH03-P06-02"]},
{"id":"CH03-P06-04","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop35_iii"}],"representation":"J 非空：Fib d ϕ J y U = ⋂_{j∈J} Fib1 d ϕ j y U（I 有限，J 自动有限）。","dependencies":["CH03-D02"]},
{"id":"CH03-P06-05","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop35_iv"}],"representation":"J ⊆ K ⇒ Fib d ϕ K y U ⊆ Fib d ϕ J y U。","dependencies":["CH03-D02"]},
{"id":"CH03-P06-06","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop35_v"},{"file":"Main.lean","name":"OETCh03.Fib_singleton"}],"representation":"Fib d ϕ {i} y U = Fib1 d ϕ i y U = {x | x∈U ∧ d_i(ϕx,y)=0}，以及 J=I（univ）时 Fib d ϕ univ y U ⊆ Fib1 d ϕ i y U。","dependencies":["CH03-D02","CH03-P06-05"]},
{"id":"CH03-P06-07","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop35_vi_a"}],"representation":"j∈Iid d ϕ U ⇒ 对任意目标 y，Fib d ϕ {j} y U = {x | x∈U ∧ d_j(x,y)=0}。","dependencies":["CH03-D01","CH03-D02"]},
{"id":"CH03-P06-08","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop35_vi_b"}],"representation":"j∈Iconst d ϕ U、y₀∈ϕ(U) ⇒ Fib d ϕ {j} y₀ U = U，且对任意 y 满足 0<d_j(y,y₀) 有 Fib d ϕ {j} y U = ∅。","dependencies":["CH03-D01","CH03-D02"]},
{"id":"CH03-P07-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.IsImageFactor"},{"file":"Main.lean","name":"OETCh03.prop36_nec"}],"representation":"T : ↥(ϕA.func '' U) → X（定义在实际像集上），IsImageFactor 表示 ∀x∈U, T(ϕA x)=ϕB x；存在这样的 T ⇒ Req ϕA U ⊆ Req ϕB U。","dependencies":["CH03-D03"]},
{"id":"CH03-P07-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.factorMap"},{"file":"Main.lean","name":"OETCh03.prop36_suff"},{"file":"Main.lean","name":"OETCh03.prop36_suff_empty"},{"file":"Main.lean","name":"OETCh03.prop36_i"}],"representation":"factorMap 显式构造：对 y∈ϕA(U) 选代表元 x∈U（Classical.choose），令 T y = ϕB x；prop36_suff 在 Req ϕA U ⊆ Req ϕB U 下证明对任意代表元 T(ϕA x)=ϕB x（即良定义且 T∘ϕA=ϕB）；prop36_suff_empty 处理 U=∅（像集空、空映射）；prop36_i 汇总为 iff（前提 U⊆dom ϕA ∩ dom ϕB）。","dependencies":["CH03-D03","CH03-P07-01"]},
{"id":"CH03-P07-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop36_ii"}],"representation":"两个方向的像值变换 T、T' 都存在 ↔ Req ϕA U = Req ϕB U，由 (i) 双向应用。","dependencies":["CH03-D03","CH03-P07-01","CH03-P07-02"]},
{"id":"CH03-P07-04","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop36_iii"},{"file":"Main.lean","name":"OETCh03.prop36_iii_matrix"}],"representation":"单分量情形以同一分量伪度量 δ 的标量界表示：0<K_A<⊤、L_B<⊤、∀x x'∈U, K_A·δ(x,x') ≤ δ(ϕAx,ϕAx')、δ(ϕBx,ϕBx') ≤ L_B·δ(x,x')，T 满足 IsImageFactor ⇒ ∀y y'∈ϕA(U)（子类型），δ(Ty,Ty') ≤ (L_B/K_A)·δ(y,y')；prop36_iii_matrix 为 Subsingleton I 时由 co-Lip/Lip 矩阵唯一条目给出的同一结论。","dependencies":["CH03-P07-01"]},
{"id":"CH03-P08-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.IsQuotFactor"},{"file":"Main.lean","name":"OETCh03.quotFactorMap"},{"file":"Main.lean","name":"OETCh03.quotFactorMap_spec"},{"file":"Main.lean","name":"OETCh03.prop37_one"}],"representation":"商映射 Tb : ImageQuot d hd ϕA U → ImageQuot d hd ϕB U，IsQuotFactor 为规定公式 Tb[ϕA x]=[ϕB x]（∀x∈U）；quotFactorMap 用 Quotient.lift 构造（lift 的相容性证明即代表元无关性），quotFactorMap_spec 证明规定公式；prop37_one：存在满足公式的商映射 ↔ Rsim ϕA ⊆ Rsim ϕB。","dependencies":["CH03-D03"]},
{"id":"CH03-P08-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop37_two"}],"representation":"双向商映射（各自满足规定公式）存在 ↔ Rsim d ϕA U = Rsim d ϕB U。","dependencies":["CH03-D03","CH03-P08-01"]},
{"id":"CH03-P08-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.SeparatingOn"},{"file":"Main.lean","name":"OETCh03.Req_eq_Rsim_of_sep"},{"file":"Main.lean","name":"OETCh03.prop37_sep"}],"representation":"SeparatingOn d S：S 内族零距蕴含相等；仅假设在两个实际像集 ϕA(U)、ϕB(U) 上各自分离，证明 Req=Rsim（两侧各自），并证明单向点值判据 ↔ 单向商值判据、双向点值 ↔ 双向商值（以映射存在性陈述）。","dependencies":["CH03-D03","CH03-P07-01","CH03-P07-02","CH03-P07-03","CH03-P08-01","CH03-P08-02"]},
{"id":"CH03-P09-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.fiberGE_refl"},{"file":"Main.lean","name":"OETCh03.fiberGE_trans"},{"file":"Main.lean","name":"OETCh03.fiberGE_isPreorder"}],"representation":"固定 U 时 fiberGE d U 自反、传递，并实例化为 IsPreorder (Operator X bot) (fiberGE d U)。","dependencies":["CH03-D03"]},
{"id":"CH03-P09-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.fiber_chain"},{"file":"Main.lean","name":"OETCh03.fiber_chain_fin"}],"representation":"链 ϕ : ℕ → Operator 的前 m+1 项，∀r∈[1,m], ϕ(r−1) ⪰ ϕ r ⇒ ∀a<b≤m, ϕ a ⪰ ϕ b（Nat.le_induction）。fiber_chain_fin 给出有限族 φ : Fin (m+1) → Operator（φ_0,…,φ_m）的直接形式：∀r : Fin m, φ r ⪰ φ (r+1) ⇒ ∀a≤b, φ a ⪰ φ b（Fin.monotone_iff_le_succ）。","dependencies":["CH03-D03","CH03-P09-01"]},
{"id":"CH03-P09-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.fiber_chain_strict"},{"file":"Main.lean","name":"OETCh03.fiber_chain_fin_strict"}],"representation":"若某 1≤r≤m 有 R_{r−1} ⊊ R_r，则 R_r \\ R_{r−1} ⊆ R_m \\ R_0、该差集非空（见证点对），且 R_0 ⊊ R_m。fiber_chain_fin_strict 为 Fin (m+1) 有限族的同一结论（差集见证与 R_0 ⊊ R_m）。","dependencies":["CH03-D03","CH03-P09-01","CH03-P09-02"]},
{"id":"CH03-P10-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.RB"},{"file":"Main.lean","name":"OETCh03.liftDist"},{"file":"Main.lean","name":"OETCh03.liftDist_epm"},{"file":"Main.lean","name":"OETCh03.dR"},{"file":"Main.lean","name":"OETCh03.dR_epm"},{"file":"Main.lean","name":"OETCh03.gR"},{"file":"Main.lean","name":"OETCh03.gR_epm"},{"file":"Main.lean","name":"OETCh03.realOp"},{"file":"Main.lean","name":"OETCh03.stepF"},{"file":"Main.lean","name":"OETCh03.stepOp"},{"file":"Main.lean","name":"OETCh03.stepSet"},{"file":"Main.lean","name":"OETCh03.Ustep"},{"file":"Main.lean","name":"OETCh03.ex_step_structure"}],"representation":"ℝ⊔{⊥} 表示为 Option ℝ（none=⊥）；liftDist 按吸收元约定延拓实距离，liftDist_epm 验证扩展伪度量；dR 为通常距离 ENNReal.ofReal|x−y|，gR 为单分量族（I=Unit）；realOp 把实函数提升为保持 ⊥ 的算子；stepF 为阶跃函数，Ustep = some '' ([-1,0) ∪ (0,1])；ex_step_structure 验证结构合法、f(⊥)=⊥、U⊆dom f、U 非空、⊥∉U。","dependencies":[]},
{"id":"CH03-P10-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.stepF_eq_of_close"},{"file":"Main.lean","name":"OETCh03.stepSet_ne_zero"},{"file":"Main.lean","name":"OETCh03.step_witness"},{"file":"Main.lean","name":"OETCh03.ex_step_adm"},{"file":"Main.lean","name":"OETCh03.ex_step_radius"}],"representation":"ex_step_adm：对每个 y∈U，合法有限正半径集 admRadii dR dR f (some y) U 恰为 Ioc 0 (ofReal|y|)（≤|y| 时同号点输出相同；>|y| 时 step_witness 构造 U 中异号点落入开球）；ex_step_radius：r^N(y|U)=|y|>0。","dependencies":["CH03-D04","CH03-P10-01"]},
{"id":"CH03-P10-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.ex_step_uniform"},{"file":"Main.lean","name":"OETCh03.counterexample31"}],"representation":"对同一固定 U：取基点 min(1,ε)→0 证明 uNR dR dR f U = 0（ENNReal.le_of_forall_pos_le_add），即零化矩阵唯一条目为 0；counterexample31 汇总：∀y∈U, 0<r^N(y|U)，而统一半径为 0。","dependencies":["CH03-D04","CH03-D05","CH03-P10-01","CH03-P10-02"]},
{"id":"CH03-P11-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop38_i_a"}],"representation":"U 非空、U⊆dom ϕ、J 非空且 J⊆Iconst d ϕ U ⇒ ∀y∈U, Fib d ϕ J (ϕy) U = U。","dependencies":["CH03-D01","CH03-D02","CH03-D07"]},
{"id":"CH03-P11-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop38_i_b"}],"representation":"同前提，对任意输入分量 i：∀y∈U, r^N_{ϕ,i,J}(y|U)=⊤（所有有限正半径均合法）且 r̲^N_{ϕ,i,J}|_U=⊤。","dependencies":["CH03-D01","CH03-D02","CH03-D04","CH03-D05","CH03-D07","CH03-P11-01"]},
{"id":"CH03-P11-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.dInf"},{"file":"Main.lean","name":"OETCh03.dInf_epm"},{"file":"Main.lean","name":"OETCh03.prop38_ii_example"},{"file":"Main.lean","name":"OETCh03.prop38_ii"}],"representation":"X={⊥,a,b}，任意（可判等）指标集 I 与输入分量 i：d_i(a,b)=⊤、其余分量 d_k(a,b)=1，均验证扩展伪度量；ϕ=id，U={a,b}；对任意 j（含 j=i 与 j≠i）证明 ∀y∈U, r^N=⊤、[N(ϕ)|_U]_{ji}=⊤ 而 j∉I_const；prop38_ii 分别以 I=Unit（i=j）与 I=Bool（i≠j）否定“[N]_{ji}=⊤ ⇒ j 常值”的全称命题。","dependencies":["CH03-D01","CH03-D04","CH03-D05","CH03-P03-01"]},
{"id":"CH03-P12-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop39_i"}],"representation":"y∈U⊆dom ϕ、i∈Iid d ϕ U ⇒ Fib1 d ϕ i (ϕy) U = {x | 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":"OETCh03.prop39_ii"}],"representation":"同前提，0<r₀<⊤ 且 ball d_i y r₀ ∩ U ⊆ {x∈U | d_i(x,y)=0} ⇒ r₀ ≤ r^N_{ϕ,i,i}(y|U) 且 0 < r^N_{ϕ,i,i}(y|U)。","dependencies":["CH03-D01","CH03-D02","CH03-D04","CH03-P12-01"]},
{"id":"CH03-P13-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.admRadii_subfamily"},{"file":"Main.lean","name":"OETCh03.prop310_pointwise"},{"file":"Main.lean","name":"OETCh03.prop310_pointwise_min"}],"representation":"J 非空：r 对 d_J 合法 ↔ 对每个 j∈J 合法；r^N_{ϕ,i,J}(y|U) = ⨅_{j∈J} r^N_{ϕ,i,j}(y|U)（≤ 由合法集包含，≥ 由合法集向下封闭与稠密性）；prop310_pointwise_min（I 有限）给出最小值形式：∃ j∈J 使 r^N_{ϕ,i,J}(y|U) = r^N_{ϕ,i,j}(y|U) 且 ∀ j'∈J, r^N_{ϕ,i,j}(y|U) ≤ r^N_{ϕ,i,j'}(y|U)。","dependencies":["CH03-D04","CH03-D07"]},
{"id":"CH03-P13-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop310_uniform"},{"file":"Main.lean","name":"OETCh03.iInf_finite_attained"},{"file":"Main.lean","name":"OETCh03.prop310_uniform_min"}],"representation":"r̲^N_{ϕ,i,J}|_U = ⨅_{j∈J} nullMatrix d ϕ U j i（iInf₂_comm 交换基点下确界与子族下确界）；iInf_finite_attained 证明有限非空 J 上该下确界由某 j∈J 取到，即为最小值 min；prop310_uniform_min（I 有限）直接给出 ∃ j∈J, r̲^N_{ϕ,i,J}|_U = [N(ϕ)|_U]_{ji} 且该条目是 J 上最小者。","dependencies":["CH03-D04","CH03-D05","CH03-D07","CH03-P13-01"]},
{"id":"CH03-P13-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop310_anti"}],"representation":"J 非空、J⊆K ⇒ r̲^N_{ϕ,i,K}|_U ≤ r̲^N_{ϕ,i,J}|_U（由最小值公式与 biInf_mono）。","dependencies":["CH03-D05","CH03-D07","CH03-P13-02"]},
{"id":"CH03-P14-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop311_fib"}],"representation":"y,y'∈U₂⊆dom ϕ₂，y'∈Fib1 d ϕ₂ j (ϕ₂y) U₂ ⇒ d_j(ϕ₂y,ϕ₂y')=0（对称性）。","dependencies":["CH03-D02"]},
{"id":"CH03-P14-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop311_radius"},{"file":"Main.lean","name":"OETCh03.exists_adm_of_lt_nullRadius"},{"file":"Main.lean","name":"OETCh03.zero_of_lt_nullRadius"}],"representation":"d_i(y,y') < r^N_{ϕ₂,i,j}(y|U₂) ⇒ 由 lt_sSup 提取合法有限正半径 ρ>d_i(y,y')，y'∈ball∩U₂，归结为纤维判据，得 d_j(ϕ₂y,ϕ₂y')=0。","dependencies":["CH03-D04","CH03-P14-01"]},
{"id":"CH03-P14-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop311_comp"}],"representation":"x,x'∈dom ϕ₁、ϕ₁x,ϕ₁x'∈U₂：ϕ₁x'∈Fib1 d ϕ₂ j (ϕ₂(ϕ₁x)) U₂ ⇒ d_j((ϕ₂*ϕ₁)x,(ϕ₂*ϕ₁)x')=0；并附半径判据的复合版本。","dependencies":["CH03-D02","CH03-D04","CH03-P14-01","CH03-P14-02"]},
{"id":"CH03-P15-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop312_i"}],"representation":"U 非空、U⊆dom(ϕ₂*ϕ₁)、∀y y'∈ϕ₁(U), d_l(y,y')=0 → d_j(ϕ₂y,ϕ₂y')=0 ⇒ nullMatrix d ϕ₁ U l i ≤ nullMatrix d (ϕ₂*ϕ₁) U j i。","dependencies":["CH03-D04","CH03-D05"]},
{"id":"CH03-P15-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop312_ii"},{"file":"Main.lean","name":"OETCh03.prop312_ii_top"}],"representation":"0<L<⊤ 且 ∀x x'∈U, d_l(ϕ₁x,ϕ₁x') ≤ L·d_i(x,x') ⇒ nullMatrix d ϕ₂ (ϕ₁(U)) j l / L ≤ nullMatrix d (ϕ₂*ϕ₁) U j i（下游在实际像域 ϕ₁(U) 上读取）；右端为 0 时由 ENNReal 非负平凡成立，右端为 ⊤ 时 prop312_ii_top 给出复合条目为 ⊤。","dependencies":["CH03-D04","CH03-D05"]},
{"id":"CH03-P16-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.lemma313_cases"},{"file":"Main.lean","name":"OETCh03.lemma313_complement"},{"file":"Main.lean","name":"OETCh03.lemma313_exclusive"}],"representation":"lemma313_cases：type=(1,1)/(1,0)/(0,1)/(0,0) 分别 ↔ (σ<τσ ∧ τN≤r̲)/(σ<τσ ∧ r̲<τN)/(τσ≤σ ∧ τN≤r̲)/(τσ≤σ ∧ r̲<τN)，且 type 属于这四值之一；lemma313_complement 证明两项判断的否定即互补不等式、四种组合穷尽；lemma313_exclusive 显式证明四种条件组合两两互斥（6 对）。","dependencies":["CH03-D05","CH03-D06"]},
{"id":"CH03-P16-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.lemma313_i"}],"representation":"τσ ≤ τσ'（其他数据固定）⇒ {p : I×I | 第一项=1 (τσ)} ⊆ {p | 第一项=1 (τσ')}。","dependencies":["CH03-D06"]},
{"id":"CH03-P16-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.lemma313_ii"}],"representation":"τN ≤ τN' ⇒ {p | 第二项=1 (τN')} ⊆ {p | 第二项=1 (τN)}。","dependencies":["CH03-D05","CH03-D06"]},
{"id":"CH03-P17-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop314_i"}],"representation":"任意 InputScaleFamily σ，∅≠B⊆A⊆dom f：σ_i(B) ≤ σ_i(A)，且 σ_i(A)<τσ ⇒ σ_i(B)<τσ。","dependencies":["CH03-D06"]},
{"id":"CH03-P17-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop314_ii_a"}],"representation":"固定 x∈B（∅≠B⊆A⊆dom f）：r^N_{f,i,j}(x|A) ≤ r^N_{f,i,j}(x|B)（A 上合法半径在 B 上仍合法）。","dependencies":["CH03-D04"]},
{"id":"CH03-P17-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop314_ii_b"}],"representation":"uNR (d i) (d j) f A ≤ uNR (d i) (d j) f B：inf_{x∈B} r(x|B) ≥ inf_{x∈B} r(x|A) ≥ inf_{x∈A} r(x|A)。","dependencies":["CH03-D04","CH03-D05","CH03-P17-02"]},
{"id":"CH03-P17-04","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.diam_pair_01"},{"file":"Main.lean","name":"OETCh03.diam_single_0"},{"file":"Main.lean","name":"OETCh03.prop314_iii"},{"file":"Main.lean","name":"OETCh03.prop314_iii_not"}],"representation":"带 ⊥ 实直线、通常距离、f=id、A={0,1}、B={0}、直径尺度、τσ=1/2：σ(B)=0<1/2，σ(A)=1≥1/2；prop314_iii_not 否定“σ(B)<τσ ⇒ σ(A)<τσ”。","dependencies":["CH03-D06","CH03-P10-01"]},
{"id":"CH03-P18-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop315_i"}],"representation":"∅≠A⊆dom f，x y∈A，d_i(x,y) < r̲^N_{f,i,j}|_A ⇒ d_j(fx,fy)=0（经 r̲ ≤ r^N(x|A) 与单步判据）。","dependencies":["CH03-D04","CH03-D05","CH03-P14-02"]},
{"id":"CH03-P18-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop315_ii"}],"representation":"0 < d_j(fx,fy) ⇒ r̲^N_{f,i,j}|_A ≤ d_i(x,y)（(i) 的逆否）。","dependencies":["CH03-D05","CH03-P18-01"]},
{"id":"CH03-P18-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop315_iii"}],"representation":"0<τN<⊤、r̲<τN，对每个有限正 α 满足 r̲<α<τN：∃x y∈A, ∃ε, 0<ε<⊤ ∧ d_i(x,y)<α ∧ ε ≤ d_j(fx,fy)；ε 取 min(d_j(fx,fy),1)，含输出距离为 ⊤ 情形。","dependencies":["CH03-D04","CH03-D05"]},
{"id":"CH03-P19-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop316_i"}],"representation":"0<τN<⊤、τN ≤ r̲^N_{f,i,j}|_A ⇒ ∀x∈A, ball d_i x τN ∩ A ⊆ Fib1 d f j (fx) A。","dependencies":["CH03-D02","CH03-D04","CH03-D05"]},
{"id":"CH03-P19-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop316_ii_a"},{"file":"Main.lean","name":"OETCh03.prop316_ii_empty"}],"representation":"同前提，对任意 B⊆A 与 0<ε<⊤：covering_number (d j) ε (f(B)) ≤ covering_number (d i) τN B；对每个输入内覆盖 S 构造 S.image f 为 f(B) 的内部中心集（基数不增），再取 iInf；B=∅ 与无有限覆盖（右端 ⊤）情形均由同一论证覆盖，prop316_ii_empty 另行记录 B=∅ 时两侧均为 0。","dependencies":["CH03-D05","CH03-D07","CH03-P19-01"]},
{"id":"CH03-P19-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop316_ii_b"}],"representation":"B 非空：metric_entropy (d j) ε (f(B)) ≤ metric_entropy (d i) τN B（log₂ 单调）。","dependencies":["CH03-D05","CH03-D07","CH03-P19-02"]},
{"id":"CH03-P20-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.cov_pair_01_half"},{"file":"Main.lean","name":"OETCh03.remark316"},{"file":"Main.lean","name":"OETCh03.remark316_no_uniform_scale"},{"file":"Main.lean","name":"OETCh03.remark316_forall"},{"file":"Main.lean","name":"OETCh03.remark316_no_scale"}],"representation":"在反例3.1 的阶跃算子与同一 U 上：remark316_forall 对任意 0<τ<⊤ 及任意满足 0<a≤1、ofReal(2a)<τ 的实数 a（全称量化），证明 B={−a,a}⊆U、N(τ,B)=1、f(B)={0,1}、N(1/2,f(B))=2；remark316 证明这样的 a 存在（取 a=min(1,τ/4)）并给出同一结论；remark316_no_uniform_scale：对每个有限正 τ 存在 B⊆U 使 N(τ,B) < N(1/2,f(B))，即点态正半径不能保证统一输入尺度。remark316_no_scale 直接否定：不存在有限正 τ 使 ∀B⊆U, ∀ε∈(0,∞), N(ε,f(B)) ≤ N(τ,B)。","dependencies":["CH03-D07","CH03-P10-01"]},
{"id":"CH03-P21-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.cor317"},{"file":"Main.lean","name":"OETCh03.cor317_type"}],"representation":"0<τσ,τN<⊤、(diamScale d).σ i A < τσ ≤ τN：τN ≤ r̲^N_{f,i,j}|_A ↔ ∀x y∈A, d_j(fx,fy)=0；→ 用直径界与 3.15(i)，← 证明各点 r^N=⊤。cor317_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":"OETCh03.cor317_cover"},{"file":"Main.lean","name":"OETCh03.covering_number_eq_one_of_zero"},{"file":"Main.lean","name":"OETCh03.cor317_cover_of_radius"}],"representation":"A 非空且输出两两 d_j 零距 ⇒ ∀ 0<ε<⊤, covering_number (d j) ε (f(A)) = 1（单中心内覆盖 + 非空下界）；cor317_cover_of_radius 在推论 3.17 的直径与阈值条件下由 τN ≤ r̲^N 一侧给出同一结论。","dependencies":["CH03-D05","CH03-D06","CH03-D07","CH03-P21-01"]},
{"id":"CH03-P22-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.covering_number_le_of_finite"},{"file":"Main.lean","name":"OETCh03.covering_number_lt_top_of_finite"},{"file":"Main.lean","name":"OETCh03.remark_finite_wd"}],"representation":"U 非空有限、U⊆dom ϕ、两端子族非空、0<ε<⊤：两端（子族）覆盖数 >0 且 <⊤，两端熵为实数，EntropyDiffDomain 成立，且对任意定义域证明 h，mapEntropyDiff … h 为实数。","dependencies":["CH03-D07","CH03-D08"]},
{"id":"CH03-P23-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop318_i"}],"representation":"j∈Iconst、U 非空、0<ε<⊤：N_j(ε,ϕ(U))=1、E_{ε,j}(ϕ(U))=0、熵差定义域成立，且对任意定义域证明 h，mapEntropyDiff d {j} {j} ε ϕ U h = E_{ε,j}(U)（输入熵可为 ⊤）。","dependencies":["CH03-D01","CH03-D07","CH03-D08","CH03-P21-02"]},
{"id":"CH03-P23-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.preCenters"},{"file":"Main.lean","name":"OETCh03.preCenters_spec"},{"file":"Main.lean","name":"OETCh03.prop318_ii_a"}],"representation":"j∈Iid：前向用 S.image ϕ、反向用 preCenters（对 T⊆ϕ(U) 每个中心选 U 中代表元）各自构造内覆盖，证明 N_j(ε,ϕ(U)) = N_j(ε,U)，进而熵相等。","dependencies":["CH03-D01","CH03-D07","CH03-P01-03"]},
{"id":"CH03-P23-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop318_ii_b"}],"representation":"仅在给出 h : EntropyDiffDomain d {j} {j} ε ϕ U 时陈述 mapEntropyDiff … h = 0；有限性由 h 的一端有限与覆盖数相等推出，不对 ⊤−⊤ 赋值。","dependencies":["CH03-D01","CH03-D07","CH03-D08","CH03-P23-02"]},
{"id":"CH03-P24-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.lip_push_net"},{"file":"Main.lean","name":"OETCh03.prop319_cover"}],"representation":"0<L<⊤ 且 ∀x y∈U, d_j(ϕx,ϕy) ≤ L·d_i(x,y)：U 的 ε/L-内覆盖 S 推出 S.image ϕ 为 ϕ(U) 的 ε-内覆盖且 |S.image ϕ| ≤ |S|；故 N_j(ε,ϕ(U)) ≤ N_i(ε/L,U)。","dependencies":["CH03-D07"]},
{"id":"CH03-P24-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop319"}],"representation":"U 非空、U⊆dom ϕ、TotallyBoundedIn (d i) U、0<ε<⊤、0<L<⊤：E_{ε,i}(U)、E_{ε,j}(ϕ(U))、E_{ε/L,i}(U) 均为实数，EntropyDiffDomain 成立（映射熵差良定），且对任意定义域证明 h：E_{ε,i}(U) − E_{ε/L,i}(U) ≤ ΔE_{ε,i,j}(ϕ|U)。","dependencies":["CH03-D07","CH03-D08","CH03-P24-01"]},
{"id":"CH03-P25-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.colip_pull_net"},{"file":"Main.lean","name":"OETCh03.prop320_cover"}],"representation":"K 满足 IsCoLipMatrix 且 0<K i j<⊤：ϕ(U) 的 ε-内覆盖 T 经 preCenters 拉回为 U 的 ε/K_{i→j}-内覆盖（K_{i→j}d_i ≤ Σ_k K_{k→j}d_k ≤ d_j），基数不增；故 N_i(ε/K_{i→j},U) ≤ N_j(ε,ϕ(U))。","dependencies":["CH03-D07","CH03-P23-02"]},
{"id":"CH03-P25-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.prop320"}],"representation":"输入全有界给出 E_{ε,i}(U)、E_{ε/K,i}(U) 为实数，EntropyDiffDomain 由输入端有限成立（输出熵可为 ⊤，差值仍良定），且对任意定义域证明 h：ΔE_{ε,i,j}(ϕ|U) ≤ E_{ε,i}(U) − E_{ε/K_{i→j},i}(U)（EReal.sub_le_sub，⊤ 输出时左端为 ⊥）。","dependencies":["CH03-D07","CH03-D08","CH03-P25-01"]},
{"id":"CH03-P26-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.dAbs"},{"file":"Main.lean","name":"OETCh03.dAbs_epm"},{"file":"Main.lean","name":"OETCh03.gAbs"},{"file":"Main.lean","name":"OETCh03.gAbs_epm"},{"file":"Main.lean","name":"OETCh03.affOp"},{"file":"Main.lean","name":"OETCh03.U01"},{"file":"Main.lean","name":"OETCh03.ex31_i_a"}],"representation":"dAbs 为绝对值读数距离 ofReal||x|−|y||（liftDist_epm 验证扩展伪度量），ϕ(x)=2x−1 由 realOp 给出且 ϕ(⊥)=⊥，U={0,1}⊆dom ϕ；ϕ(0)=−1、ϕ(1)=1，Fib_{ϕ,i}(ϕ(0)|U)=U，i∈I_const(ϕ|U)。","dependencies":["CH03-D01","CH03-D02","CH03-P06-08","CH03-P10-01"]},
{"id":"CH03-P26-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.ex31_i_b"}],"representation":"在同一 U={0,1} 上：U⊆dom ϕ²、ϕ²(0)=−3、ϕ²(1)=1、Fib_{ϕ²,i}(ϕ²(0)|U)={0}，i∈I_act(ϕ²|U)（非常值且非恒等）。","dependencies":["CH03-D01","CH03-D02","CH03-P10-01","CH03-P26-01"]},
{"id":"CH03-P26-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.ex31_ii"}],"representation":"任意算子 ψ 在 U 上取同一实数值 c：ψ²(0)=ψ²(1)、d_i 零距、两目标纤维相同；ψ(c)≠⊥ 时 U⊆dom ψ²、Fib_{ψ²,i}(ψ²(0)|U)=U、i 为常值分量；ψ(c)=⊥ 时 U∩dom ψ²=∅ 且 U⊄dom ψ²（不在纤维定义的适用域内）。","dependencies":["CH03-D01","CH03-D02","CH03-P06-08","CH03-P10-01","CH03-P26-01"]},
{"id":"CH03-P27-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.ex32_i"}],"representation":"U 非空、K 满足 IsCoLipMatrix、0<K i j（可为 ⊤）、y∈U、0<r^N_{ϕ,i,j}(y|U) ⇒ ∀x∈U, d_i(x,y) ∉ Ioo 0 r^N（零化判据给 d_j=0，co-Lip 单项给正下界，矛盾）。","dependencies":["CH03-D04"]},
{"id":"CH03-P27-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.ex32_ii"}],"representation":"0<r̲^N_{ϕ,i,j}|_U ⇒ {0} 与 Ici r̲ 不交，且 ∀x y∈U, d_i(x,y) ∈ {0} ∪ Ici r̲（Ici 含 ⊤，即 [r̲,+∞]）。","dependencies":["CH03-D04","CH03-D05","CH03-P27-01"]},
{"id":"CH03-P28-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.shiftOp"},{"file":"Main.lean","name":"OETCh03.U33"},{"file":"Main.lean","name":"OETCh03.mem_U33"},{"file":"Main.lean","name":"OETCh03.fib33"},{"file":"Main.lean","name":"OETCh03.one_eq_realOp_id"},{"file":"Main.lean","name":"OETCh03.ex33_i"}],"representation":"d_i=dAbs，U={−3,−2,0,2}，ϕ(x)=x+1；验证结构与 U⊆dom；恒等算子纤维族 = {{−3},{−2,2},{0}}，平移纤维族 = {{−3},{−2,0},{2}}（Set (Set RB)，去重后），二者均满足 IsPartitionOf U。","dependencies":["CH03-D02","CH03-P06-03","CH03-P10-01","CH03-P26-01"]},
{"id":"CH03-P28-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.ex33_image"},{"file":"Main.lean","name":"OETCh03.ofReal_three_halves"},{"file":"Main.lean","name":"OETCh03.ex33_ii"},{"file":"Main.lean","name":"OETCh03.log2_ereal_two"}],"representation":"ε=ofReal(3/2)=3/2：N_i(ε,U)=2（上界：中心 {0,2}；下界：0 与 2 无公共内部中心），ϕ(U)={−2,−1,1,3} 且 N_i(ε,ϕ(U))=1（中心 −2），EntropyDiffDomain 成立，且对任意定义域证明 h，ΔE_{ε,i}(ϕ|U)=log₂2−log₂1=1。","dependencies":["CH03-D07","CH03-D08","CH03-P10-01","CH03-P26-01","CH03-P28-01"]},
{"id":"CH03-P29-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.floorOp"},{"file":"Main.lean","name":"OETCh03.D1"},{"file":"Main.lean","name":"OETCh03.diam_Icc"},{"file":"Main.lean","name":"OETCh03.floor_D1"},{"file":"Main.lean","name":"OETCh03.uNR_D1"},{"file":"Main.lean","name":"OETCh03.ex34_D1"}],"representation":"f=⌊·⌋（floorOp），D=[0,1/2]：D 非空且 D⊆dom f，diam=1/2，f 在 D 上恒为 0 故统一半径 ⊤，Type=(1,1)（τσ=τN=1）。","dependencies":["CH03-D04","CH03-D05","CH03-D06","CH03-P10-01","CH03-P16-01"]},
{"id":"CH03-P29-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.D2"},{"file":"Main.lean","name":"OETCh03.floor_radius_one_zero"},{"file":"Main.lean","name":"OETCh03.uNR_zero_of"},{"file":"Main.lean","name":"OETCh03.ex34_D2"}],"representation":"D=[9/10,11/10]：D 非空且 D⊆dom f，diam=1/5；基点 1 处无合法有限正半径（左侧点 1−min(e/2,1/10) 的 floor 为 0）故 r^N(1|D)=0、统一半径 0；Type=(1,0)。","dependencies":["CH03-D04","CH03-D05","CH03-D06","CH03-P10-01","CH03-P16-01","CH03-P29-01"]},
{"id":"CH03-P29-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.D3"},{"file":"Main.lean","name":"OETCh03.D3_radius"},{"file":"Main.lean","name":"OETCh03.uNR_D3"},{"file":"Main.lean","name":"OETCh03.diam_D3"},{"file":"Main.lean","name":"OETCh03.ex34_D3"}],"representation":"D={0,2}：D 非空且 D⊆dom f，diam=2；两基点的合法半径恰到 2 为止，r^N=2，统一半径 2；Type=(0,1)。","dependencies":["CH03-D04","CH03-D05","CH03-D06","CH03-P10-01","CH03-P16-01","CH03-P29-01"]},
{"id":"CH03-P29-04","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.D4"},{"file":"Main.lean","name":"OETCh03.ex34_D4"}],"representation":"D=[0,2]：D 非空且 D⊆dom f，diam=2，统一半径 0（基点 1），Type=(0,0)。","dependencies":["CH03-D05","CH03-D06","CH03-P10-01","CH03-P16-01","CH03-P29-01","CH03-P29-02"]},
{"id":"CH03-P29-05","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.ex34_ii"},{"file":"Main.lean","name":"OETCh03.D3_ball"}],"representation":"否定 ∀ 非空 D⊆ℝ, 1 ≤ r̲^N_{f,d,d}|_D ⇒ 全部输出零距；反例 D={0,2}：r̲=2≥1 但 d(f0,f2)=2≠0；同时记录正半径来源为输入两点间隙 d(0,2)=2。D3_ball 证明半径 r∈(0,2] 的开球与 D 之交只含基点，即正零化半径来源于输入两点间隙。","dependencies":["CH03-D05","CH03-P10-01","CH03-P29-01","CH03-P29-03"]},
{"id":"CH03-P30-01","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.U4"},{"file":"Main.lean","name":"OETCh03.mem_U4"},{"file":"Main.lean","name":"OETCh03.U4_sep"},{"file":"Main.lean","name":"OETCh03.U4_finset_card"},{"file":"Main.lean","name":"OETCh03.cov4"},{"file":"Main.lean","name":"OETCh03.cov4'"},{"file":"Main.lean","name":"OETCh03.ex35_i_center"}],"representation":"U={0,1,2,3}，通常距离；cov4：∀e>0, N(ofReal e,U) = 4 (e≤1)、2 (1<e≤2)、1 (e>2)（含端点），cov4' 为 ENNReal ε∈(0,∞) 形式；ex35_i_center：3/2∉U，所有点到 3/2 的距离 <7/4 但 {3/2} 不是内覆盖，N(7/4,U)=2。","dependencies":["CH03-D07","CH03-P10-01"]},
{"id":"CH03-P30-02","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.fPart"},{"file":"Main.lean","name":"OETCh03.gPart"},{"file":"Main.lean","name":"OETCh03.f5"},{"file":"Main.lean","name":"OETCh03.g5"},{"file":"Main.lean","name":"OETCh03.f5_fix"},{"file":"Main.lean","name":"OETCh03.g5_v0"},{"file":"Main.lean","name":"OETCh03.g5_v1"},{"file":"Main.lean","name":"OETCh03.g5_v2"},{"file":"Main.lean","name":"OETCh03.g5_v3"},{"file":"Main.lean","name":"OETCh03.ex35_structure"},{"file":"Main.lean","name":"OETCh03.f5_image"},{"file":"Main.lean","name":"OETCh03.g5_image"},{"file":"Main.lean","name":"OETCh03.U4_finite"},{"file":"Main.lean","name":"OETCh03.ex35_dE"},{"file":"Main.lean","name":"OETCh03.ex35_ii"}],"representation":"f,g 由偏映射 partialOp 给出，在 U 上按表取值、在 X\\U 上为 ⊥（ex35_structure）；f(U)=g(U)=U；任意 0<ε<⊤ 下两像集覆盖数均等于 N(ε,U)，且两映射的 EntropyDiffDomain 均成立、对任意定义域证明 h 熵差均为 0。","dependencies":["CH03-D07","CH03-D08","CH03-P10-01","CH03-P22-01","CH03-P30-01"]},
{"id":"CH03-P30-03","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.ofReal_le_three_mul"},{"file":"Main.lean","name":"OETCh03.ex35_lip"}],"representation":"IsLeast {L | ∀x y∈U, d(fx,fy) ≤ L·d(x,y)} 1 与 IsLeast {…g…} 3：1、3 为合法常数（g 逐对 16 情形验证），必要下界由点对 (1,0)（d(f1,f0)=1、d(g1,g0)=3）给出。","dependencies":["CH03-P10-01","CH03-P30-01","CH03-P30-02"]},
{"id":"CH03-P30-04","status":"complete","declarations":[{"file":"Main.lean","name":"OETCh03.ofReal_seven_fourths"},{"file":"Main.lean","name":"OETCh03.ex35_iii_b"}],"representation":"ε=ofReal(7/4)=7/4，代入命题3.19 证明中的上界 prop319_cover：f（L=1）：N(ε,f(U)) ≤ N(ε/1,U)=2，真实值 2；g（L=3）：N(ε,g(U)) ≤ N(ε/3,U)=N(7/12,U)=4，真实值 2。","dependencies":["CH03-D07","CH03-P10-01","CH03-P24-01","CH03-P30-01","CH03-P30-02","CH03-P30-03"]}
]}