{
  "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.Fixed"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Ident"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Active"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.component_partition"
        }
      ],
      "representation": "Each index is represented by applying the predicates to d i. Ident explicitly excludes Const, so the three proved mutually exclusive and exhaustive predicates implement constant-first component partitioning.",
      "dependencies": []
    },
    {
      "id": "CH03-D02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Fiber"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.composite_zero"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_representation"
        }
      ],
      "representation": "Fiber is exactly the restricted set defined by zero composite output distance. composite_zero proves equivalence of the supremum composite pseudometric with all component zero equations.",
      "dependencies": [
        "CH03-D07"
      ]
    },
    {
      "id": "CH03-D03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.EqRel"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.ZeroRel"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.FiberPreorder"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.imageSetoid"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.ImageQuotient"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.imageClass"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.zero_relation_fiber"
        }
      ],
      "representation": "Relations are subsets of X×X with both endpoints in U. The actual image subtype carries the componentwise zero setoid, whose equivalence is proved from pseudometric axioms; its quotient and canonical image class are constructed. The fiber relation correspondence includes symmetry.",
      "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_iff"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.radius_empty_legal"
        }
      ],
      "representation": "Legal radii are ENNReal values strictly between zero and infinity. The ball-intersection inclusion is proved equivalent to Legal; Radius is their supremum, with empty legal set giving zero.",
      "dependencies": []
    },
    {
      "id": "CH03-D05",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.UniformOn"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Uniform"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.NullMatrix"
        }
      ],
      "representation": "UniformOn distinguishes the basepoint set A from the assessment domain U; Uniform uses A=U. NullMatrix has arguments output j followed by input i and is the singleton-output uniform radius.",
      "dependencies": [
        "CH03-D04"
      ]
    },
    {
      "id": "CH03-D06",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.ScaleFamily"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.diameter"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.diameter_mono"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.diameterScale"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.thresholdType"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.ChannelType"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.channel_type_formula"
        }
      ],
      "representation": "ScaleFamily is monotone on nonempty subsets. diameterScale proves validity of the default double supremum diameter. ChannelType uses the input scale and the j,i null-matrix entry, encoding 1 and 0 by true and false.",
      "dependencies": [
        "CH03-D05"
      ]
    },
    {
      "id": "CH03-D07",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.TotallyBoundedBy"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.totally_bounded_iff"
        },
        {
          "file": "formal_oet/vol_01/ch_01_foundations/metric_entropy.lean",
          "name": "formal_oet.vol_01.ch_01_foundations.InternalEpsilonNet"
        },
        {
          "file": "formal_oet/vol_01/ch_01_foundations/metric_entropy.lean",
          "name": "formal_oet.vol_01.ch_01_foundations.covering_number"
        },
        {
          "file": "formal_oet/vol_01/ch_01_foundations/metric_entropy.lean",
          "name": "formal_oet.vol_01.ch_01_foundations.covering_number_attained"
        },
        {
          "file": "formal_oet/vol_01/ch_01_foundations/metric_entropy.lean",
          "name": "formal_oet.vol_01.ch_01_foundations.covering_number_eq_top_iff"
        },
        {
          "file": "formal_oet/vol_01/ch_01_foundations/metric_entropy.lean",
          "name": "formal_oet.vol_01.ch_01_foundations.log2_ereal"
        },
        {
          "file": "formal_oet/vol_01/ch_01_foundations/metric_entropy.lean",
          "name": "formal_oet.vol_01.ch_01_foundations.metric_entropy"
        },
        {
          "file": "formal_oet/vol_01/ch_01_foundations/metric_entropy.lean",
          "name": "formal_oet.vol_01.ch_01_foundations.subfamily_pseudometric"
        },
        {
          "file": "formal_oet/vol_01/ch_01_foundations/metric_entropy.lean",
          "name": "formal_oet.vol_01.ch_01_foundations.subfamily_metric_entropy"
        },
        {
          "file": "formal_oet/vol_01/ch_01_foundations/metric_entropy.lean",
          "name": "formal_oet.vol_01.ch_01_foundations.subfamily_metric_entropy_eq_metric_entropy"
        }
      ],
      "representation": "The imported frozen InternalEpsilonNet uses finite centers inside the set and strict open balls. covering_number_attained and covering_number_eq_top_iff supply the minimum/infinity correspondence. Composite distance and entropy are the imported chapter-1 definitions. TotallyBoundedBy is proved equivalent to finite covering number at every finite positive precision.",
      "dependencies": []
    },
    {
      "id": "CH03-D08",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.DifferenceDefined"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.EntropyDifference"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.entropy_difference_formula"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.difference_no_indeterminate"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.difference_top"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.difference_bottom"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.difference_real"
        }
      ],
      "representation": "The difference requires the specified disjunction of finite input/output covering numbers. Instantiating di and dout by the respective composite pseudometrics gives the chapter definition. The no-infinity-minus-infinity condition, both infinite-result branches, and finite-real subtraction are proved.",
      "dependencies": [
        "CH03-D07"
      ]
    },
    {
      "id": "CH03-P01-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.const_zero_row"
        }
      ],
      "representation": "Constant output has zero ENNReal tsum upper row, for every pair in U.",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P01-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.const_colip_entry"
        }
      ],
      "representation": "An actual sum lower bound plus a positive source-distance witness forces the corresponding ENNReal coefficient to zero, including infinite distances and coefficients.",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P01-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.ident_isometry"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.zero_replace"
        }
      ],
      "representation": "Identity components preserve the component distance in both directions, using symmetry and triangle inequalities.",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P02-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.active_comp"
        }
      ],
      "representation": "Componentwise implication represents the requested set inclusion. The outer evaluation domain is exactly f image U. All constant/identity alternatives are handled.",
      "dependencies": [
        "CH03-D01",
        "CH03-P01-03",
        "CH03-P02-03",
        "CH03-P04-01"
      ]
    },
    {
      "id": "CH03-P02-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.chainPrefix"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.chainPrefix_domain_step"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.active_chain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.identity_not_active"
        }
      ],
      "representation": "chainPrefix uses zero-based steps, starts with id, and recurses by postcomposition. The intermediate domain is exactly the prefix image. The theorem gives a step k<n witnessing activity; the zero-step case is proved impossible.",
      "dependencies": [
        "CH03-P02-01",
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P02-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.ident_comp"
        }
      ],
      "representation": "Both pointwise zero-displacement and exclusion of constant output are proved for the composition on U and the actual intermediate image.",
      "dependencies": [
        "CH03-D01",
        "CH03-P01-03"
      ]
    },
    {
      "id": "CH03-P03-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.twoDist"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.twoDist_lawful"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.swap"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.twoDomain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.swap_domain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.swap_image"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.swap_twice"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.swap_composite_domain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.swap_counterexample"
        }
      ],
      "representation": "Option Bool realizes the absorbing point and the two exchanged points, with distance 1 between them. The extended metric and lawful operator/domain/image are checked. Both steps are active and nonidentity while the composition is identity and nonactive. With a singleton index set these are the stated component-set computations and witnesses against both reverse inclusions.",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P04-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.outer_const"
        }
      ],
      "representation": "Outer constancy on the actual image directly implies composite constancy on U.",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P04-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.Six"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.discreteRead"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.discreteRead_lawful"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.sevenGauge"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.sevenGauge_lawful"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.sevenInner"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.sevenOuter"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.sevenDomain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.seven_domain_legal"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.seven_image"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.seven_inner_constant"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.seven_composite_not_constant"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.seven_other_component_separates"
        }
      ],
      "representation": "Option Six has exactly the absorbing point and a,b,p,q,r,s. The first component identifies p,q and has unit distance on all other distinct nonabsorbing classes; the second is discrete. Both extended pseudometrics and both absorbing-point operators are proved lawful. The exact inner image is {p,q}; it is constant in the first component, while the composite outputs r,s at distance one. The second component separates p,q.",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P05-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.sparse_row_const"
        }
      ],
      "representation": "An actual output-row sum inequality on the image and zero off-diagonal coefficients propagate inner constancy. No coefficient finiteness assumption is imposed.",
      "dependencies": [
        "CH03-D01"
      ]
    },
    {
      "id": "CH03-P06-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_target_zero"
        }
      ],
      "representation": "Arbitrary targets with all selected component distances zero give identical restricted fibers, by triangle inequalities and symmetry.",
      "dependencies": [
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P06-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_image_nonempty"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_cover"
        }
      ],
      "representation": "Every image-target fiber is nonempty, and their union is exactly U, including U empty.",
      "dependencies": [
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P06-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.fibers_equal_or_disjoint"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_cover"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_image_nonempty"
        }
      ],
      "representation": "For any two targets, fibers are equal or disjoint; together with image-fiber nonemptiness and exact coverage this is the partition after duplicate removal.",
      "dependencies": [
        "CH03-D02",
        "CH03-P06-01",
        "CH03-P06-02"
      ]
    },
    {
      "id": "CH03-P06-04",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_intersection"
        }
      ],
      "representation": "For nonempty J, the fiber equals the intersection of singleton-component fibers. The proof works for arbitrary J, hence for finite nonempty J.",
      "dependencies": [
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P06-05",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_antitone"
        }
      ],
      "representation": "J subset K implies K-fiber subset J-fiber.",
      "dependencies": [
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P06-06",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_singleton"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_full_subset"
        }
      ],
      "representation": "Singleton fibers have exactly one zero-distance equation; the full-family fiber is contained in each singleton fiber.",
      "dependencies": [
        "CH03-D02",
        "CH03-P06-05"
      ]
    },
    {
      "id": "CH03-P06-07",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_ident"
        }
      ],
      "representation": "At an identity component, every arbitrary-target fiber equals the corresponding input zero-distance class within U.",
      "dependencies": [
        "CH03-D01",
        "CH03-D02",
        "CH03-P06-06"
      ]
    },
    {
      "id": "CH03-P06-08",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_const"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_const_empty"
        }
      ],
      "representation": "Constant component fibers at image targets equal U. For arbitrary targets at positive distance from an image target, the fiber is empty.",
      "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": "The forward implication of factors_iff proves actual point-valued image factorization implies inclusion of equality relations.",
      "dependencies": [
        "CH03-D03"
      ]
    },
    {
      "id": "CH03-P07-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Factors"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.factors_iff"
        }
      ],
      "representation": "The reverse implication constructs T on the image subtype using representatives and relation inclusion; it also works when U is empty.",
      "dependencies": [
        "CH03-D03"
      ]
    },
    {
      "id": "CH03-P07-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.mutual_factors_iff"
        }
      ],
      "representation": "Factorizations in both directions are equivalent to equality of the restricted point-value relations.",
      "dependencies": [
        "CH03-P07-01",
        "CH03-P07-02"
      ]
    },
    {
      "id": "CH03-P07-04",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.factor_lip"
        }
      ],
      "representation": "For a specified image factorization T, positive finite K and finite L give the exact L/K scalar inequality on all actual image points.",
      "dependencies": []
    },
    {
      "id": "CH03-P08-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.QuotientFactors"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.quotient_factors_iff"
        }
      ],
      "representation": "The quotient-lift construction is independent of image representatives, satisfies the required canonical-class equation, and is equivalent to zero-relation inclusion.",
      "dependencies": [
        "CH03-D03"
      ]
    },
    {
      "id": "CH03-P08-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.mutual_quotient_factors_iff"
        }
      ],
      "representation": "Factorizations between the two actual-image zero quotients in both directions are equivalent to equality of zero relations.",
      "dependencies": [
        "CH03-P08-01"
      ]
    },
    {
      "id": "CH03-P08-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.separated_relations"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.separated_factorization"
        }
      ],
      "representation": "Explicit separation is assumed only on each actual image. Under precisely those hypotheses the zero relations equal point-value equality relations, and the factorization criteria agree.",
      "dependencies": [
        "CH03-D03",
        "CH03-P07-01",
        "CH03-P07-02",
        "CH03-P08-01"
      ]
    },
    {
      "id": "CH03-P09-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_preorder_refl"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_preorder_trans"
        }
      ],
      "representation": "Fixed-domain inclusion of restricted zero relations is reflexive and transitive.",
      "dependencies": [
        "CH03-D03"
      ]
    },
    {
      "id": "CH03-P09-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.relation_chain"
        }
      ],
      "representation": "For any chain of sets R k and any a≤b≤n, consecutive inclusions imply R a subset R b. Instantiate R k with the restricted zero relations on the common U.",
      "dependencies": []
    },
    {
      "id": "CH03-P09-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.relation_chain_strict"
        }
      ],
      "representation": "A strict step supplies a concrete point-pair in the final relation but not the initial relation, as well as strict endpoint inclusion.",
      "dependencies": [
        "CH03-P09-02"
      ]
    },
    {
      "id": "CH03-P10-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.absorbDist"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.readingDist"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realDist"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realDist_formula"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realDist_lawful"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.stepOp"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.stepDomain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.step_domain_legal"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.step_formula"
        }
      ],
      "representation": "Option ℝ realizes the usual real line plus its isolated absorbing point. The exact usual-distance formula and all extended pseudometric axioms are proved. stepOp is the absorbing-preserving step 0 for x<0, 1 for x≥0. stepDomain is exactly the image of [-1,0) union (0,1], and is proved nonempty and contained in the operator domain.",
      "dependencies": []
    },
    {
      "id": "CH03-P10-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.step_real_nonzero"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.step_lower_radius"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.step_point_radius"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.legal_iff_radius_bound"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.step_legal_radii"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.step_point_radius_positive"
        }
      ],
      "representation": "For every real y in the fixed step domain, the point radius equals ofReal |y| and is positive. Legal finite positive radii are proved equivalent to 0<r≤ofReal |y|, including the endpoint r=|y|. The upper bound constructs an opposite-sign domain point whenever the proposed radius exceeds |y|.",
      "dependencies": [
        "CH03-D04",
        "CH03-P10-01",
        "CH03-P14-02"
      ]
    },
    {
      "id": "CH03-P10-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.step_uniform_zero"
        }
      ],
      "representation": "On the same fixed stepDomain the uniform radius is exactly zero. For every positive extended threshold the proof constructs a positive basepoint inside this domain whose computed point radius lies below the threshold.",
      "dependencies": [
        "CH03-D05",
        "CH03-P10-02"
      ]
    },
    {
      "id": "CH03-P11-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_const"
        }
      ],
      "representation": "Constancy of every selected output component makes every image-target J-fiber equal U.",
      "dependencies": [
        "CH03-D01",
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P11-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.const_family_radii"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.const_radius"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.const_uniform"
        }
      ],
      "representation": "Constancy gives top pointwise radii at all basepoints and top uniform radius for any input distance. The proof uses arbitrarily large strictly positive finite legal radii.",
      "dependencies": [
        "CH03-D01",
        "CH03-D04",
        "CH03-D05",
        "CH03-D07",
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P11-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.infiniteDist_lawful"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.twoGauge_lawful"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.identityOp"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.identity_domain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.infinite_input_radius"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Examples.infinite_radius_counterexample"
        }
      ],
      "representation": "The lawful Option Bool structure with two components realizes infinite input separation and either infinite same-component or unit distinct-component output separation. Identity has top pointwise/uniform radii but is not constant in either output component.",
      "dependencies": [
        "CH03-D01",
        "CH03-D04",
        "CH03-D05"
      ]
    },
    {
      "id": "CH03-P12-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.identity_image_fiber"
        }
      ],
      "representation": "For y in U, the identity-component fiber at f y is exactly the input zero class of y within U.",
      "dependencies": [
        "CH03-D01",
        "CH03-D02",
        "CH03-P01-03",
        "CH03-P06-06"
      ]
    },
    {
      "id": "CH03-P12-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.identity_radius_bound"
        }
      ],
      "representation": "A finite positive radius whose input ball contains only zero-distance points is legal under the identity-component assumption, yielding radius≥r>0.",
      "dependencies": [
        "CH03-D01",
        "CH03-D04",
        "CH03-P01-03"
      ]
    },
    {
      "id": "CH03-P13-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.radius_components"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.finite_inf_attained"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.radius_component_minimum"
        }
      ],
      "representation": "The pointwise family radius equals the infimum of singleton radii. For a finite nonempty family, a minimizing component is explicitly obtained, proving the stated minimum formula.",
      "dependencies": [
        "CH03-D04",
        "CH03-D07",
        "CH03-P14-02"
      ]
    },
    {
      "id": "CH03-P13-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.uniform_components"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.uniform_component_minimum"
        }
      ],
      "representation": "The basepoint and component infima are interchanged with both inequalities proved. The finite nonempty result is attained at a component and equals the corresponding null-matrix entry.",
      "dependencies": [
        "CH03-D05",
        "CH03-P13-01"
      ]
    },
    {
      "id": "CH03-P13-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.radius_output_antitone"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.uniform_output_antitone"
        }
      ],
      "representation": "Enlarging the selected output family decreases the pointwise and uniform radii.",
      "dependencies": [
        "CH03-D04",
        "CH03-D05",
        "CH03-D07"
      ]
    },
    {
      "id": "CH03-P14-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.fiber_step"
        }
      ],
      "representation": "A singleton-fiber membership gives output zero distance, with the chapter orientation obtained by symmetry.",
      "dependencies": [
        "CH03-D02"
      ]
    },
    {
      "id": "CH03-P14-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.below_radius"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.radius_step"
        }
      ],
      "representation": "Strict inequality below the supremum extracts a legal finite positive radius exceeding the distance and proves output zero distance. Both symmetry orientations are made explicit.",
      "dependencies": [
        "CH03-D04"
      ]
    },
    {
      "id": "CH03-P14-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.composite_fiber_step"
        }
      ],
      "representation": "Both inner image points are explicitly assumed in the downstream domain. Applying the singleton-fiber condition yields the composite output zero equation.",
      "dependencies": [
        "CH03-P14-01"
      ]
    },
    {
      "id": "CH03-P15-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.composite_radius_mono"
        }
      ],
      "representation": "A zero-preserving downstream map on the exact actual image sends every legal inner radius to a legal composite radius, proving the uniform lower bound.",
      "dependencies": [
        "CH03-D04",
        "CH03-D05"
      ]
    },
    {
      "id": "CH03-P15-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.le_radius_iff"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.composite_lip_radius"
        }
      ],
      "representation": "The exact downstream uniform radius divided by L is a lower bound for the composite. The proof uses a characterization valid for all extended thresholds, including 0 and infinity, without excluding either boundary.",
      "dependencies": [
        "CH03-D04",
        "CH03-D05",
        "CH03-P14-02",
        "CH03-P18-01"
      ]
    },
    {
      "id": "CH03-P16-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.threshold_type_iff"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.threshold_exhaustive"
        }
      ],
      "representation": "There exists exactly one Bool×Bool pair satisfying the two threshold comparisons. As Bool has exactly false/true this proves the four combinations exhaustive and mutually exclusive.",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P16-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.scale_threshold_mono"
        }
      ],
      "representation": "Increasing the scale threshold preserves every first-coordinate true comparison, pointwise on channels and hence as channel-set inclusion.",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P16-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.radius_threshold_antitone"
        }
      ],
      "representation": "Increasing the null-radius threshold can only shrink the second-coordinate true channel set.",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P17-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.scale_domain_mono"
        }
      ],
      "representation": "For every monotone scale family and nonempty B subset A, both the scale inequality and the strict threshold implication are proved.",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P17-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.radius_mono_domain"
        }
      ],
      "representation": "Shrinking the assessment domain enlarges the legal radius set at each fixed basepoint. The result holds even without requiring the basepoint in B, and therefore includes that case.",
      "dependencies": [
        "CH03-D04"
      ]
    },
    {
      "id": "CH03-P17-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.uniform_mono_domain"
        }
      ],
      "representation": "Both the assessment domain and the infimum basepoint domain shrink from A to B. Each basepoint comparison is composed with the original uniform lower bound.",
      "dependencies": [
        "CH03-D05",
        "CH03-P17-02"
      ]
    },
    {
      "id": "CH03-P17-04",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realDist_lawful"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realIdentity"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.zeroOne"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.real_two_point_scale_counterexample"
        }
      ],
      "representation": "This is the actual absorbing real-line example, not merely an abstract two-point substitute. A={some 0,some 1}, B={some 0}, and the lawful identity operator satisfy the domain and nonemptiness conditions. Their diameters are 1 and 0, giving B<1/2 but not A<1/2.",
      "dependencies": [
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P18-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.below_uniform"
        }
      ],
      "representation": "Any input pair in the domain whose distance is strictly below the uniform radius has zero output distance.",
      "dependencies": [
        "CH03-D05",
        "CH03-P14-02"
      ]
    },
    {
      "id": "CH03-P18-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.separated_lower_bound"
        }
      ],
      "representation": "Positive output distance forces the input distance to be at least the uniform radius, by contraposition.",
      "dependencies": [
        "CH03-P18-01"
      ]
    },
    {
      "id": "CH03-P18-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.insufficient_radius_witness"
        }
      ],
      "representation": "For every α strictly above the uniform radius, there are domain points with input distance below α and positive output separation. ε=min(output distance,1) is positive finite and bounded by the output distance, including infinite output separation.",
      "dependencies": [
        "CH03-D05",
        "CH03-P14-02"
      ]
    },
    {
      "id": "CH03-P19-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.threshold_ball"
        }
      ],
      "representation": "A threshold below or equal to the uniform radius makes every restricted open input ball lie in the corresponding output zero fiber.",
      "dependencies": [
        "CH03-P18-01"
      ]
    },
    {
      "id": "CH03-P19-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.transfer_net"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.transfer_cover"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.null_cover_bound"
        }
      ],
      "representation": "Images of finite internal input centers form internal output centers with nonincreasing cardinality. Infima give the bound for every B subset A, including empty B and absence of any finite input cover.",
      "dependencies": [
        "CH03-D07",
        "CH03-P18-01"
      ]
    },
    {
      "id": "CH03-P19-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.log2_mono_positive"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.entropy_cover_mono"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.null_entropy_bound"
        }
      ],
      "representation": "The extended base-two logarithm is proved monotone on positive covering numbers. For nonempty B the covering bound therefore yields the stated entropy comparison, including infinite values.",
      "dependencies": [
        "CH03-D07",
        "CH03-P19-02"
      ]
    },
    {
      "id": "CH03-P20-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.step_domain_legal"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.step_point_radius_positive"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.step_uniform_zero"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.zeroOne_cover_half"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.step_cover_counterexample"
        }
      ],
      "representation": "For every finite positive τ the theorem chooses a=min(τ.toReal/4,1)>0, proves a≤1 and ofReal(2a)<τ, and proves {-a,a} is inside the same fixed stepDomain. Its internal input covering number at τ is exactly one; its step image is {0,1}, whose internal covering number at 1/2 is exactly two.",
      "dependencies": [
        "CH03-D07",
        "CH03-P10-01",
        "CH03-P10-02",
        "CH03-P10-03"
      ]
    },
    {
      "id": "CH03-P21-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.small_domain_iff"
        }
      ],
      "representation": "Under diameter(A)<τσ≤τN, the τN uniform-radius test is equivalent to all outputs being zero-distance. Constancy gives top uniform radius for the reverse direction.",
      "dependencies": [
        "CH03-D01",
        "CH03-D05",
        "CH03-D06",
        "CH03-P11-02",
        "CH03-P18-01"
      ]
    },
    {
      "id": "CH03-P21-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.const_cover_one"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.small_domain_iff"
        }
      ],
      "representation": "For nonempty A and every positive ε, all-output zero distance makes a singleton internal output net, and nonemptiness supplies the matching lower bound one. Combining with small_domain_iff gives the requested consequence.",
      "dependencies": [
        "CH03-D07",
        "CH03-P21-01"
      ]
    },
    {
      "id": "CH03-P22-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.finite_cover_bound"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.finite_entropy_real"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.finite_difference_defined"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.finite_difference_real"
        }
      ],
      "representation": "Finite U is covered by its own centers. The theorem gives positive finite covering numbers and finite real entropy for each self-zero distance, hence for both composite metrics. The image of finite nonempty U is finite nonempty, and its entropy difference is a genuine real value.",
      "dependencies": [
        "CH03-D07",
        "CH03-D08"
      ]
    },
    {
      "id": "CH03-P23-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.const_cover_one"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.const_entropy_zero"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.const_difference"
        }
      ],
      "representation": "Constant components give output cover number one, entropy zero, and a defined entropy difference equal to the input entropy, with no finiteness assumption on that input entropy.",
      "dependencies": [
        "CH03-D01",
        "CH03-D07",
        "CH03-D08"
      ]
    },
    {
      "id": "CH03-P23-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.pull_net"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.pull_cover"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.ident_cover_entropy"
        }
      ],
      "representation": "Forward image centers and backward chosen representatives both give cardinality-nonincreasing internal nets. Identity-component isometry proves both covering inequalities and equality of entropy.",
      "dependencies": [
        "CH03-P01-03",
        "CH03-D07",
        "CH03-P19-02"
      ]
    },
    {
      "id": "CH03-P23-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.ident_difference_zero"
        }
      ],
      "representation": "Only under DifferenceDefined and nonempty U does equal entropy yield difference zero. Infinite input entropy is explicitly ruled out by the finiteness condition and equality of both entropies.",
      "dependencies": [
        "CH03-D08",
        "CH03-P23-02"
      ]
    },
    {
      "id": "CH03-P24-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.lip_transfer"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.transfer_net"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.transfer_cover"
        }
      ],
      "representation": "For positive finite L, an ε/L internal net pushes to an ε output net; the returned center set has cardinality at most the original, and the covering-number inequality follows.",
      "dependencies": [
        "CH03-D07",
        "CH03-P19-02"
      ]
    },
    {
      "id": "CH03-P24-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.lip_entropy_bound"
        }
      ],
      "representation": "Total boundedness makes the ε and ε/L input coverings finite, hence the ε output covering finite. Nonempty-set entropy is nonnegative and not top. The displayed entropy-difference lower bound follows with a proof of DifferenceDefined.",
      "dependencies": [
        "CH03-D07",
        "CH03-D08",
        "CH03-P19-03",
        "CH03-P24-01"
      ]
    },
    {
      "id": "CH03-P25-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.colip_transfer"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.pull_net"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.pull_cover"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.matrix_entry_lower"
        }
      ],
      "representation": "For positive finite K, chosen preimages of each internal output center give an ε/K input net with no larger cardinality; the covering lower bound follows.",
      "dependencies": [
        "CH03-D07",
        "CH03-P23-02"
      ]
    },
    {
      "id": "CH03-P25-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.colip_entropy_bound"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.matrix_entry_lower"
        }
      ],
      "representation": "Input total boundedness supplies the finiteness condition for the entropy difference. The exact difference upper bound follows from the co-Lip covering inequality, without assuming output entropy finite.",
      "dependencies": [
        "CH03-D07",
        "CH03-D08",
        "CH03-P19-03",
        "CH03-P25-01"
      ]
    },
    {
      "id": "CH03-P26-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.absDist"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.absDist_formula"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.absDist_lawful"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.affine"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.zeroOne"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.affine_domain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.affine_constant"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.affine_fiber"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.affine_component"
        }
      ],
      "representation": "The actual Option ℝ model uses the absolute-value reading pseudometric ||x|-|y||, whose extended axioms are verified. The lawful affine map is 2x-1 on reals. On the exact U={0,1}, its fiber at φ(0) equals U and the component is constant, explicitly not identity and not active.",
      "dependencies": [
        "CH03-D01",
        "CH03-D02",
        "CH03-P11-01"
      ]
    },
    {
      "id": "CH03-P26-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.affine_domain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.affine_squared_fiber"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.affine_squared_component"
        }
      ],
      "representation": "For the same U={0,1}, the selfcomposite has fiber {0} at φ²(0), and is active. The exact composite domain includes U; the proof does not replace U by an intermediate image.",
      "dependencies": [
        "CH03-D01",
        "CH03-D02",
        "CH03-P26-01"
      ]
    },
    {
      "id": "CH03-P26-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.point_constant_selfcomp"
        }
      ],
      "representation": "For any lawful absorbing-point operator, a common point-value c on U remains a common point-value f(c) after selfcomposition. If f(c) is nonabsorbing U stays in the composite domain; if it is absorbing the intersection with that domain is empty. This applies in particular to the real-valued constant case of the exercise.",
      "dependencies": []
    },
    {
      "id": "CH03-P27-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.colip_gap_point"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.matrix_entry_lower"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.matrix_colip_gap_point"
        }
      ],
      "representation": "Positive co-Lip coefficient and a pointwise null-radius test exclude every input distance in (0,radius); K is allowed to be infinite.",
      "dependencies": [
        "CH03-P14-02"
      ]
    },
    {
      "id": "CH03-P27-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.colip_gap_uniform"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.matrix_colip_gap_uniform"
        }
      ],
      "representation": "Each input pair has either zero distance or distance at least the uniform radius. The result is stronger than the positive-uniform-radius case, and K need not be finite.",
      "dependencies": [
        "CH03-P27-01",
        "CH03-D05"
      ]
    },
    {
      "id": "CH03-P28-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.absDist_formula"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.absDist_lawful"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realIdentity"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.translation"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.translationDomain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.translation_domain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.identity_translation_domain_fibers"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.translation_fibers"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.translation_partition_equalities"
        }
      ],
      "representation": "Both operators are lawful on the specified four-point real domain. The duplicate-free identity fiber partition is {{-3},{-2,2},{0}} and the translation fiber partition is {{-3},{-2,0},{2}}. Four target computations for each map and exact set-of-fibers equalities establish the complete partitions.",
      "dependencies": [
        "CH03-D02",
        "CH03-P26-01"
      ]
    },
    {
      "id": "CH03-P28-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.translation_input_cover"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.translation_output_cover"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.translation_entropy_difference"
        }
      ],
      "representation": "At the exact ENNReal precision 3/2, the internal input covering number is two and the internal output covering number is one. Explicit internal nets and lower bounds prove equality, and the defined extended-real entropy difference is exactly one.",
      "dependencies": [
        "CH03-D07",
        "CH03-D08",
        "CH03-P28-01"
      ]
    },
    {
      "id": "CH03-P29-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realDist_formula"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realDist_lawful"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floorOp"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floor_domain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realInterval"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realInterval_nonempty"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realInterval_diameter"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floor_half_constant"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floor_half_data"
        }
      ],
      "representation": "The lawful absorbing real-line floor operator is restricted to the exact lifted closed interval [0,1/2]. Its diameter is ofReal(1/2), its uniform radius is infinity, and its threshold type at (1,1) is (true,true), representing (1,1).",
      "dependencies": [
        "CH03-D05",
        "CH03-D06",
        "CH03-P11-02"
      ]
    },
    {
      "id": "CH03-P29-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floorOp"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floor_domain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realInterval_nonempty"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realInterval_diameter"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floor_crossing_radius_zero"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floor_crossing_uniform_zero"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floor_crossing_data"
        }
      ],
      "representation": "On the exact interval [9/10,11/10], diameter is ofReal(1/5), uniform radius is zero, and type is (true,false). At basepoint 1, every positive finite legal radius is contradicted by a point just below 1 inside the same interval.",
      "dependencies": [
        "CH03-D04",
        "CH03-D05",
        "CH03-D06",
        "CH03-P29-01"
      ]
    },
    {
      "id": "CH03-P29-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floorOp"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realDist_lawful"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.zeroTwo"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.zeroTwo_domain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.zeroTwo_diameter"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.zeroTwo_floor_radius"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.zeroTwo_floor_uniform"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.zeroTwo_floor_type"
        }
      ],
      "representation": "On the exact two-point domain {0,2}, diameter is two, each point radius and the uniform radius are two, and the threshold type is (false,true). The radius upper bound uses the other point, and the lower bound verifies every strict input ball.",
      "dependencies": [
        "CH03-D04",
        "CH03-D05",
        "CH03-D06"
      ]
    },
    {
      "id": "CH03-P29-04",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floorOp"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floor_domain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realInterval_nonempty"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realInterval_diameter"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floor_wide_uniform_zero"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floor_wide_data"
        }
      ],
      "representation": "On [0,2], diameter is two, uniform radius is zero, and type is (false,false). The crossing interval is explicitly included in this domain, so domain monotonicity transports its zero uniform-radius upper bound.",
      "dependencies": [
        "CH03-D05",
        "CH03-D06",
        "CH03-P17-03",
        "CH03-P29-02"
      ]
    },
    {
      "id": "CH03-P29-05",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.zeroTwo_domain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.zeroTwo_floor_radius"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.zeroTwo_floor_uniform"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.floor_positive_radius_not_constant"
        }
      ],
      "representation": "The lawful nonempty domain {0,2} has uniform radius two, hence at least one, but output distances are not all zero. The point-radius proof shows the positive radius comes from the isolated two-point input gap, not from constant output.",
      "dependencies": [
        "CH03-P29-03"
      ]
    },
    {
      "id": "CH03-P30-01",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.realDist_lawful"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.fourDomain"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.fourCenters"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.fourCenters_coe"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.fourCenters_card"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.four_nonempty"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.four_finite"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.separated_finite_cover"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.four_separated"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.four_cover_small"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.four_cover_medium"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.four_cover_large"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.four_cover_all"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.three_halves_not_internal"
        }
      ],
      "representation": "For every positive ε, the exact internal covering number is 4 for ε≤1, 2 for 1<ε≤2, and 1 for 2<ε. Thus the strict-ball endpoints at 1 and 2 are included in the correct branches. Finite-center lower bounds and explicit internal nets prove all branches. The proposed center 3/2 is proved outside U and therefore illegal at 7/4.",
      "dependencies": [
        "CH03-D07"
      ]
    },
    {
      "id": "CH03-P30-02",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.fourIdentity"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.fourShuffle"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.four_operators_domains"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.four_images"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.same_image_entropy_difference"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.four_image_covers_and_differences"
        }
      ],
      "representation": "Both absorbing-preserving operators have exactly U as domain, hence are absorbing outside U. Their actual images both equal U. Covering numbers at every positive precision coincide with the full piecewise formula, and both entropy differences are defined and equal zero.",
      "dependencies": [
        "CH03-D07",
        "CH03-D08",
        "CH03-P30-01"
      ]
    },
    {
      "id": "CH03-P30-03",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.four_identity_lip"
        },
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.four_shuffle_lip"
        }
      ],
      "representation": "The operators satisfy scalar Lip bounds one and three respectively on every pair in U. Evaluating the pair (0,1) proves the necessary lower bounds for every admissible ENNReal coefficient, establishing optimality.",
      "dependencies": [
        "CH03-P30-02"
      ]
    },
    {
      "id": "CH03-P30-04",
      "status": "complete",
      "declarations": [
        {
          "file": "Main.lean",
          "name": "Chapter3.Supplement.four_precision_comparison"
        }
      ],
      "representation": "At ε=7/4 both actual output covering numbers equal two. Applying the general Lip transfer bound with the proved optimal constants yields input covering numbers two at (7/4)/1 and four at (7/4)/3. Both inequalities and the exact comparison values are included.",
      "dependencies": [
        "CH03-P24-01",
        "CH03-P30-01",
        "CH03-P30-02",
        "CH03-P30-03"
      ]
    }
  ]
}