Merge in current HOL Light by dnezam · Pull Request #6 · CakeML/candle

dnezam · 2026-03-24T01:26:50Z

No description provided.

This patch adds `UNIFY_REFL_TAC`, which is a simple extension of `UNIFY_ACCEPT_TAC` for the case when the goal is an equality `t = x` and `x` is a metavariable. If the goal is `e = f x y z` and `f` is a metavariable, it instantiates `f` with `\x y z. e` (the number of arguments does not have to be 3 and can vary). This is adopted from `UNIFY_REFL_TAC` in s2n-bignum.

…of set diameter for a general metric space, "mdiameter", with basic properties mirroring as appropriate those in the Euclidean special case "diameter". New definition: mdiameter and theorems: EMBEDDING_INTO_METRIZABLE_IMP_METRIZABLE LEBESGUE_COVERING_LEMMA LEBESGUE_COVERING_LEMMA_GEN MBOUNDED_AND_MDIAMETER_LE MBOUNDED_IMP_IN_MSPACE MDIAMETER_BOUNDED MDIAMETER_BOUNDED_BOUND MDIAMETER_CLOSURE MDIAMETER_COMPACT_ATTAINED MDIAMETER_EMPTY MDIAMETER_EQ_0 MDIAMETER_EUCLIDEAN MDIAMETER_LE MDIAMETER_POS_LE MDIAMETER_SING MDIAMETER_SUBSET MDIAMETER_SUBSET_MCBALL MDIAMETER_SUBSET_MCBALL_NONEMPTY MDIAMETER_UNION_LE METRIZABLE_PRODUCT_EUCLIDEANREAL_NUM REGULAR_SECOND_COUNTABLE_HAUSDORFF_IMP_NORMAL_SPACE SEPARATING_FUNCTIONS_INJECTIVE URYSOHN_METRIZATION URYSOHN_METRIZATION_EQ The two theorems LEBESGUE_COVERING_LEMMA / LEBESGUE_COVERING_LEMMA_GEN simply replace and generalize the original Euclidean theorems of that name. The sole current application now uses the more general versions. This update has the distinction of being almost entirely written by AI, mainly Claude Opus 4.5 via AWS Bedrock. It completed the following requests entirely autonomously: * Generalize the existing "diameter" theorems as appropriate * Autoformalize Urysohn Metrization starting from Munkres's book This was inspired by, and in the latter case largely reproduces, work by Josef Urban reported in https://arxiv.org/abs/2601.03298, with the HOL Light setup due to June Lee.

Add UNIFY_REFL_TAC to unify metavariables in equality

theory in Multivariate/metric.ml, with a large number of typical results about it including Stone's theorem that a metrizable space is paracompact and the existence of subordinate partitions of unity. Some results that seemed more specialized or obscure (e.g. Nagata-Smirnov metrization and Michael's characterization of paracompactness) are placed in a separate file Multivariate/paracompact.ml that is not part of the main Multivariate load sequence. The vast majority of the proofs, including all those in the Multivariate/paracompact.ml file, were automatically written by Claude Code (two separate instances with a mix of Opus 4.5 and 4.6). New definitions: collectionwise_normal_space countably_paracompact_space locally_metrizable_space paracompact_space realcompact_space sigma_locally_finite_in and theorems CLF_OPEN_CLOSURE_IMP_LF_CLOSED CLOSED_GDELTA_IN_SIGMA_LF_BASE CLOSED_G_DELTA_IN_SIGMA_LOCALLY_FINITE_BASE CLOSED_REFINEMENT_IMP_PARACOMPACT COLLECTIONWISE_NORMAL_IMP_NORMAL COLLECTIONWISE_NORMAL_SPACE_CLOSED_SUBSET COMPACT_IMP_PARACOMPACT_SPACE COMPACT_LF_OPEN_NEIGHBORHOOD COMPACT_TUBE_COVER CONTINUOUS_MAP_SUM_LOCALLY_FINITE COUNTABLE_IMP_SIGMA_LOCALLY_FINITE_IN COUNTABLY_PARACOMPACT_IMP_DOWKER COUNTABLY_PARACOMPACT_SPACE_CLOSED_SUBSET COUNTABLY_PARACOMPACT_SPACE_PRODUCT_COMPACT CP_IMPLIES_NORMAL_SPACE CP_INDEXED_CLOSED_COVER DOWKER_BACKWARD DOWKER_DISCRETE_EXPANSION EXPANSION_SET_CONTAINS EXPANSION_SET_OPEN HOMEOMORPHIC_PARACOMPACT_SPACE LF_CLOSED_PERFECT_MAP_IMAGE LF_COVERING_IMP_LF_CLOSED LF_COVERING_IMP_LF_OPEN LINDELOF_HAUSDORFF_REGULAR_EQ_PARACOMPACT LOCALLY_FINITE_IN_HOMEOMORPHIC_IMAGE LOCALLY_FINITE_LEVEL_UNION_GEN LOCALLY_FINITE_PRODUCT_TUBES METRIC_COVER_SIGMA_LOCALLY_FINITE METRIZABLE_IMP_COLLECTIONWISE_NORMAL METRIZABLE_IMP_COUNTABLY_PARACOMPACT_SPACE METRIZABLE_IMP_PARACOMPACT_SPACE MICHAEL_LEMMA MICHAEL_PARACOMPACT MICHAEL_PARACOMPACT_EQ NAGATA_SMIRNOV_METRIZATION NORMAL_COUNTABLY_PARACOMPACT_CHARACTERIZATION NORMAL_SPACE_SIGMA_LOCALLY_FINITE_BASE OPEN_SIGMA_LF_CLOSURE_COVER PARACOMPACT_HAUSDORFF_CLOSURE_REFINEMENT PARACOMPACT_HAUSDORFF_EXPANSION_LEMMA PARACOMPACT_HAUSDORFF_IMP_COLLECTIONWISE_NORMAL PARACOMPACT_HAUSDORFF_IMP_NORMAL_SPACE PARACOMPACT_HAUSDORFF_IMP_REGULAR_SPACE PARACOMPACT_HAUSDORFF_INDEXED_SHRINKING PARACOMPACT_IMP_COUNTABLY_PARACOMPACT_SPACE PARACOMPACT_LOCALLY_METRIZABLE_IMP_METRIZABLE PARACOMPACT_LOCALLY_METRIZABLE_SIGMA_LF_BASE PARACOMPACT_PARTITION_OF_UNITY PARACOMPACT_SPACE_CLOSED_MAP_IMAGE PARACOMPACT_SPACE_CLOSED_SUBSET PARACOMPACT_SPACE_DISCRETE_TOPOLOGY PARACOMPACT_SPACE_EQ_CLOSED_REFINEMENT PARACOMPACT_SPACE_EQ_LOCALLY_FINITE_REFINEMENT PARACOMPACT_SPACE_EUCLIDEAN PARACOMPACT_SPACE_EUCLIDEAN_SUBTOPOLOGY PARACOMPACT_SPACE_FSIGMA_SUBSET PARACOMPACT_SPACE_MTOPOLOGY PARACOMPACT_SPACE_PERFECT_MAP_IMAGE PARACOMPACT_SPACE_PERFECT_MAP_PREIMAGE PARACOMPACT_SPACE_PRODUCT_COMPACT_LEFT PARACOMPACT_SPACE_PRODUCT_COMPACT_RIGHT PARACOMPACT_SPACE_RETRACTION_MAP_IMAGE POINT_FINITE_CP_CLOSED_IMP_LOCALLY_FINITE REGULAR_CLOSURE_REFINEMENT_COVERS REGULAR_LINDELOF_IMP_PARACOMPACT_SPACE REGULAR_OPEN_COVER_CLOSURE_SHRINK SECOND_COUNTABLE_LOCALLY_COMPACT_HAUSDORFF_IMP_PARACOMPACT SECOND_COUNTABLE_REGULAR_IMP_PARACOMPACT_SPACE SHRINK_DISJOINT_LATER SHRINK_SEQUENCE_COVERS SHRINK_SEQUENCE_LOCALLY_FINITE SIGMA_LOCALLY_FINITE_IMP_LOCALLY_FINITE_COVERING SMIRNOV_METRIZATION SMIRNOV_METRIZATION_SECOND_COUNTABLE URYSOHN_FUNCTION_CLOSED_GDELTA URYSOHN_FUNCTION_G_DELTA Two Euclidean theorems PARACOMPACT_CLOSED and PARACOMPACT_CLOSED_IN have been removed since they now seem too ad hoc, though PARACOMPACT is retained.

finite fields. The development, both statements and proofs, was entirely written by Claude Code (Opus 4.6, running on AWS Bedrock). A few lemmas have been slightly tweaked manually and placed in the ring theory file, since they seem more broadly applicable: POLY_DEG_1_IMP_IRREDUCIBLE POLY_DEG_EQ_0_UNIT POLY_DEG_UNIT RING_DIVIDES_SUB_POW RING_PRODUCT_CONST RING_PRODUCT_LMUL RING_SUB_TELESCOPE These are the theorems in the main Library/rabin_test.ml file culminating in RABIN_IRREDUCIBILITY_TEST: FIELD_NONZERO_PRODUCT_PERMUTE FIELD_ROOTS_BOUND FINITE_FIELD_ELEMENT_POW FINITE_FIELD_POW_ITERATE ING_DIVIDES_POW_ITERATE IRREDUCIBLE_DIVIDES_DEGREE IRREDUCIBLE_DIVIDES_DEGREE_BOUND IRREDUCIBLE_DIVIDES_XQ_MINUS_X IRREDUCIBLE_DIVIDES_XQ_MINUS_X_GEN IRRED_DIVIDES_POLY_EVAL_MINUS POLY_NONUNIT_DEGREE_GE_1 QUOTIENT_POLY_RING_FINITE_CARD RABIN_IRREDUCIBILITY_NECESSARY RABIN_IRREDUCIBILITY_SUFFICIENT RABIN_IRREDUCIBILITY_TEST RING_DIVIDES_REDUCE RING_ENDOMORPHISM_FROBENIUS_ITERATE

Rabin's irreducibility test for polynomials over finite fields

of chains, and the two uniform variants of local connectedness (ULC = uniformly locally connected and FCCOVERABLE = fine connected coverable, a.k.a. Whyburn's "Property S"), together with key results connecting them to local connectedness and compactness. The Euclidean special cases in paths.ml and topology.ml are then derived from the general versions. New definitions: fccoverable_in fccoverable_space ulc_space and new theorems: COMPACT_IN_LOCALLY_CONNECTED_EQ_FCCOVERABLE_SPACE COMPACT_IN_LOCALLY_CONNECTED_IMP_FCCOVERABLE_SPACE COMPACT_IN_LOCALLY_CONNECTED_IMP_ULC_SPACE COMPACT_IN_LOCALLY_CONNECTED_IMP_ULC_SPACE_ALT CONNECTED_COMPONENT_OF_EQ_WELLCHAINED CONNECTED_COMPONENT_OF_IMP_WELLCHAINED CONNECTED_EQ_WELLCHAINED_IN CONNECTED_IN_CHAIN CONNECTED_IN_CHAIN_GEN CONNECTED_IN_IFF_CONNECTED_COMPONENT_OF CONNECTED_IN_IMP_WELLCHAINED CONNECTED_IN_NEST CONNECTED_IN_NEST_GEN CONNECTED_IN_UNIONS_STRONG EPSILON_ABSORBING_IMP_CLOPEN FCCOVERABLE_IN_IMP_FCCOVERABLE_SPACE_SUBMETRIC FCCOVERABLE_IN_IMP_LOCALLY_CONNECTED_SPACE FCCOVERABLE_SPACE_EQ_FCCOVERABLE_IN_MSPACE FCCOVERABLE_SPACE_IMP_LOCALLY_CONNECTED_SPACE FCCOVERABLE_SPACE_INTERMEDIATE_CLOSURE IN_CLOSURE_OF_IMP_SUBSET_MCBALL MBALL_INTER_DSEPARATED_SINGLETON MDIAMETER_SUBSET_MBALL MDIAMETER_SUBMETRIC MDIST_TRIANGLE_LT NESTED_COMPACT_APPROX TOTALLY_BOUNDED_IMP_DISCRETE_FINITE TOTALLY_BOUNDED_ULC_SPACE_IMP_FCCOVERABLE_SPACE ULC_SPACE_IMP_LOCALLY_CONNECTED_SPACE WELLCHAINED_ELEMENTS WELLCHAINED_INTERS WELLCHAINED_SETS In Multivariate/topology.ml, the theorems CONNECTED_CHAIN, CONNECTED_CHAIN_GEN, CONNECTED_NEST and CONNECTED_NEST_GEN are rederived from their general topological counterparts. All theorem statements are preserved. In Multivariate/paths.ml, the Euclidean-specific theorems about ULC and FCCOVERABLE (FCCOVERABLE_IMP_LOCALLY_CONNECTED through COMPACT_LOCALLY_CONNECTED_EQ_FCCCOVERABLE) are rederived from the general metric space versions via a set of bridge lemmas connecting submetric euclidean_metric to the Euclidean topology. The well-chained theorems (CONNECTED_IMP_WELLCHAINED through CONNECTED_COMPONENT_EQ_WELLCHAINED) are similarly rederived. All theorem statements are preserved. Incompatible changes: In paths.ml, three Euclidean-specific theorems have been renamed with a _EUCLIDEAN suffix to avoid clashing with the new general versions in metric.ml that take the same names: WELLCHAINED_ELEMENTS -> WELLCHAINED_ELEMENTS_EUCLIDEAN WELLCHAINED_SETS -> WELLCHAINED_SETS_EUCLIDEAN WELLCHAINED_INTERS -> WELLCHAINED_INTERS_EUCLIDEAN These were not used outside their original block so the renaming should not affect other files. Several new Euclidean bridge lemmas are introduced in paths.ml (SUBMETRIC_EUCLIDEAN_METRIC, MTOPOLOGY_SUBMETRIC_EUCLIDEAN, MBOUNDED_SUBMETRIC_EUCLIDEAN, MDIAMETER_SUBMETRIC_EUCLIDEAN, and others) to support the derivations. The statements and proofs were almost entirely written by Claude Code (Opus 4.6).

basic definition is as the product space (:num->bool), and this is then shown to be homeomorphic to its realization as the usual Cantor "excluded thirds" subset of [0,1]. New definitions: cantor_map cantor_set cantor_space cantor_term tendsto_real_def and theorems: CANTOR_MAP_CLOSED_IMAGE CANTOR_MAP_CLOSED_IN_INTERVAL CANTOR_MAP_CONTINUOUS CANTOR_MAP_EMBEDDING CANTOR_MAP_GE_PARTIAL_SUM CANTOR_MAP_IMAGE_SUBSET_INTERVAL CANTOR_MAP_INJECTIVE CANTOR_MAP_LE_ONE CANTOR_MAP_PARTIAL_SUM_BOUND CANTOR_MAP_POS CANTOR_MAP_RANGE CANTOR_MAP_STRICT_LT CANTOR_MAP_SUMMABLE CANTOR_MAP_SUMS CANTOR_PARTIAL_SUM_DIFF_AT_K CANTOR_PARTIAL_SUM_MONO CANTOR_SET_SUBSET_INTERVAL CANTOR_SPACE_HOMEOMORPHIC_CANTOR_SET CANTOR_TERM_BOUND CANTOR_TERM_CONTINUOUS CANTOR_TERM_POS CLOSED_IN_CANTOR_SET CLOSED_IN_CANTOR_SET_INTERVAL COMPACT_SPACE_CANTOR_SPACE HAUSDORFF_SPACE_CANTOR_SPACE METRIZABLE_SPACE_CANTOR_SPACE NONEMPTY_TOPSPACE_CANTOR_SPACE PERFECT_CANTOR_SPACE PERFECT_CANTOR_SPACE_EQ SUM_TWOTHIRDS TENDSTO_REAL_EPS_DELTA TOPSPACE_CANTOR_SPACE TWOTHIRDS_SUMS ZERO_DIMENSIONAL_CANTOR_SPACE The new definition "tendsto_real_def" is just a more basic definition of the usual notion of the sum of a real series, so that it can be used in the general topology theories without the artificially circuitous derivation via real^N. The former definition "tendsto_real" is now a derived theorem rather than a definition, but is equivalent.

finitely many smaller cubes of pairwise distinct sizes ("cubing the cube"), originally proved by R. L. Brooks, C. A. B. Smith, A. H. Stone and W. T. Tutte, "The Dissection of Rectangles into Squares", Duke Mathematical Journal, vol. 7 (1940), pp. 312-340. This is another of the "Formalizing 100 Theorems" list. The proof follows the elegant argument presented in J. E. Littlewood, "A Mathematician's Miscellany" (CUP, 1953), revised edition "Littlewood's Miscellany" (ed. B. Bollobas, CUP, 1986), pp. 28-29. This formalization in HOL Light was almost entirely written by Claude Code (Opus 4.6). I provided the statements and a couple of initial lemmas, which in particular direct it to an explicit formulation using the "division_of" notion from Kurzweil-Henstock integration.

algebraically_closed_field and new theorems ALGEBRAICALLY_CLOSED_FIELD_DECOMPOSE ALGEBRAICALLY_CLOSED_FIELD_EQ_IRREDUCIBLES ALGEBRAICALLY_CLOSED_FIELD_EQ_SPLITS ALGEBRAICALLY_CLOSED_FIELD_IMP_FIELD ALGEBRAICALLY_CLOSED_FIELD_IMP_INFINITE ALGEBRAICALLY_CLOSED_FIELD_ISOMORPHIC_IMAGE ALGEBRAICALLY_CLOSED_FIELD_NO_PROPER_ALGEBRAIC_EXTENSION ALGEBRAIC_CLOSURE_EXISTS ALGEBRAIC_CLOSURE_EXISTS_ID ALGEBRAIC_CLOSURE_EXTEND_HOMOMORPHISM ALGEBRAIC_CLOSURE_UNIQUE ALGEBRAIC_CLOSURE_UNIQUE_EXPLICIT FIELD_RING_HOMOMORPHISM_MONOMORPHISM INFINITE_INTEGRAL_DOMAIN_POLY_EVAL_ALL_ZERO ISOMORPHIC_RING_ALGEBRAICALLY_CLOSED_FIELD POLY_COMPOSE_HOMOMORPHISM_ADD POLY_COMPOSE_HOMOMORPHISM_CONST POLY_COMPOSE_HOMOMORPHISM_MUL POLY_COMPOSE_HOMOMORPHISM_NEG POLY_COMPOSE_HOMOMORPHISM_POW POLY_COMPOSE_HOMOMORPHISM_SUB POLY_COMPOSE_HOMOMORPHISM_VAR POLY_DEG_1_ROOT POLY_DEG_MUL_X_MINUS_A POLY_DEG_X_MINUS_A POLY_EVALUATE_RING_PRODUCT POLY_EVAL_RING_PRODUCT POLY_EXTEND_RING_PRODUCT POLY_X_MINUS_A_IN_CARRIER POLY_X_MINUS_A_NONZERO RING_HOMOMORPHISM_EPIMORPHISM_FACTOR RING_POWERSERIES SIMPLE_ALGEBRAIC_EXTEND_HOMOMORPHISM The existence proofs ALGEBRAIC_CLOSURE_EXISTS_ID and ALGEBRAIC_CLOSURE_EXISTS were done by John Harrison following Jelonek's paper "A simple proof of the existence of the algebraic closure of a field". The rest, such as various alternative characterizations and the uniqueness up to isomorphism, were written by Claude Opus 4.6.

* metis.ml: Apply bugfixes from upstream metis repo gilith/metis@d17c3a8 * metis.ml: Inline Portable.pointerEqual * metis.ml: Replace Option module with OCaml's version * metis.ml: Inline Portable.randomInt * metis.ml: Inline Portable.randomWord * metis.ml: Inline definitions in Math module * metis.ml: Inline Int.toString and Int.div * metis.ml: Remove unused combinators + Replace with version in lib.ml * metis.ml: Remove funpow redefinition This will use the implementation in lib.ml, which is slightly different. In particular, it seems that the original implementation in metis.ml would not terminate for n < 0. * metis.ml: Remove unused Useful.swap * metis.ml: Remove redefinition of curry and uncurry Already in lib.ml * metis.ml: Remove Useful.length and inline Useful.app * metis.ml: Inline Int.maxInt and remove arbitrary precision case Affected function: multInt * metis.ml: Replace exception Error with Failure * metis.ml: Replace exception Subscript with Invalid_argument * metis.ml: Replace zipWith, zip and unzip with lib.ml versions * metis.ml: Inline mem * metis.ml: Add mapi to lib.ml and simplify enumerate * metis.ml: Use List.rev_append instead of Mlist.revAppend * metis.ml: Inline Mlist.all * metis.ml: Replace Mlist.nth with List.nth * metis.ml: Inline Real.floor * metis.ml: Inline Real.fromInt * metis.ml: Replace {foo=foo} pattern matching with {foo} * metis.ml: Remove Order module In particular, instead of defining the order type, we use the OCaml convention of using integers. I think this patch actually makes the code a bit more robust: orderOfInt (and thus toCompare by extension) would fail if the compare function returned something other than -1/0/+1, which Repr.compare doesn't seem to exclude. The applied patch was generated by Claude Code. * metis.ml: Remove Int and Real module * metis.ml: Replace boolCompare with Bool.compare * metis.ml: Copy comment for Portable.critical from upstream Source: gilith/metis/src/Portable.sig * metis.ml: Use Int.compare directly in Word * metis.ml: Qualify Useful usages, remove unused defs + inline sort This should make it easier to tell whether something comes from Useful or not, as the definitions are defined are quite general. Hopefully, it also makes future refactors easier that want to move things out of Useful. * metis.ml: Move list functions from Useful to Mlist * metis.ml: Move Portable.critical to Useful.critical * metis.ml: Inline Sharing module

* metis.ml: Remove references to Int and Bool modules Seems like these are only available starting 4.08. Patch received from John Harrison, generated by Claude. * Revert "metis.ml: Replace {foo=foo} pattern matching with {foo}" This reverts commit aa397c0. Seems like this causes parsing issues in old versions (OCaml 4.06, Camlp5 7.10) * metis.ml: Implement parts of the Option module * metis.ml: Remove references to Float module

theorems along with the underlying topological machinery and associated generalizations of existing Euclidean results. These proofs were entirely written by Claude Code (Opus 4.5 and 4.6). The Alexandroff-Hausdorff theorem (ALEXANDROFF_HAUSDORFF: every compact metrizable space is a continuous image of the Cantor space) and the Hahn-Mazurkiewicz theorem (HAHN_MAZURKIEWICZ: a metrizable continuum is a Peano continuum iff it is a continuous image of the unit interval) are entirely new results, not generalizations of anything previously in HOL Light. Their proofs go through a chain of substantial lemmas: the Alexandroff-Hausdorff embedding provides dense maps from Cantor space into compact metric spaces, and a gap-filling extension lemma (PEANO_GAP_FILLING_EXTENSION) for locally connected continua then yields the full Hahn-Mazurkiewicz characterization. From Hahn-Mazurkiewicz it follows that compact connected locally connected metric spaces are path-connected (COMPACT_CONNECTED_LOCALLY_CONNECTED_IMP_PATH_CONNECTED). This is then extended to the locally compact case by expressing open subsets as unions of compact connected locally connected sets (LOCALLY_CONNECTED_CONTINUUM_SPACE), then to complete metric spaces (MCOMPLETE_CONNECTED_LOCALLY_CONNECTED_IMP_PATH_CONNECTED, often called Menger's theorem). The existing Euclidean theorem LOCALLY_COMPACT_CONNECTED_IMP_PATH_CONNECTED assumed local compactness; the new general version for complete metric spaces is strictly stronger, since completeness is a weaker hypothesis than local compactness. New Euclidean specializations in paths.ml include optimal G_delta versions: GDELTA_CONNECTED_LOCALLY_CONNECTED_IMP_PATH_CONNECTED gives path-connectedness under the weakest natural hypothesis for R^n, since G_delta is equivalent to completely metrizable in Euclidean space. Supporting infrastructure includes: well-chained set refinements in open covers (CHAIN_FROM_OPEN_COVER), connected chain unions (CONNECTED_IN_CHAIN_UNIONS), compact nested intersections (COMPACT_NESTED_INTERS), fine connected covers of open connected sets (OPEN_CONNECTED_FINE_COVER), the full chain hierarchy construction for dyadic approximation (CHAIN_HIERARCHY), and closure of dyadic rationals in the unit interval (CLOSURE_OF_DYADIC_RATIONALS_IN_UNIT_INTERVAL). New theorems: ALEXANDROFF_HAUSDORFF CHAIN_FROM_OPEN_COVER CHAIN_HIERARCHY CHAIN_IN_OPEN_CONNECTED_SET CHAIN_REFINEMENT_STEP CLOSURE_OF_DYADIC_RATIONALS_IN_UNIT_INTERVAL COMPACT_CONNECTED_LOCALLY_CONNECTED_IMP_PATH_CONNECTED COMPACT_CONNECTED_LOCALLY_CONNECTED_IMP_PATH_CONNECTED_EUCLIDEAN COMPACT_IN_LOCALLY_CONNECTED_EQ_FCCOVERABLE_SPACE_ALT COMPACT_LOCALLY_CONNECTED_NEARBY_PATH COMPACT_METRIZABLE_LOCALLY_CONNECTED_IMP_LOCALLY_PATH_CONNECTED COMPACT_METRIZABLE_PEANO_IMP_PATH_CONNECTED COMPACT_NESTED_INTERS COMPLETELY_METRIZABLE_CONNECTED_LOCALLY_CONNECTED_IMP_PATH_CONNECTED COMPLETELY_METRIZABLE_LOCALLY_PATH_CONNECTED_EQ_LOCALLY_CONNECTED CONNECTED_IN_CHAIN_UNIONS DENSE_FUNCTION_ON_DYADIC FCCOVERABLE_IN_COMPACT_LOCALLY_CONNECTED FINITE_CONNECTED_COMPONENTS_CLOPEN_UNION FINITE_CONNECTED_COMPONENTS_COMPACT_LOCALLY_CONNECTED FINITE_CONNECTED_COMPONENTS_COMPACT_LOCALLY_CONNECTED_EUCLIDEAN GDELTA_CONNECTED_LOCALLY_CONNECTED_IMP_PATH_CONNECTED GDELTA_LOCALLY_CONNECTED_IMP_LOCALLY_PATH_CONNECTED GDELTA_LOCALLY_PATH_CONNECTED_EQ_LOCALLY_CONNECTED HAHN_MAZURKIEWICZ HAHN_MAZURKIEWICZ_IMP LOCALLY_COMPACT_CONNECTED_IMP_PATH_CONNECTED_EUCLIDEAN LOCALLY_COMPACT_CONNECTED_IMP_PATH_CONNECTED_SPACE LOCALLY_COMPACT_LOCALLY_CONNECTED_IMP_LOCALLY_PATH_CONNECTED_EUCLIDEAN LOCALLY_COMPACT_LOCALLY_CONNECTED_IMP_LOCALLY_PATH_CONNECTED_SPACE LOCALLY_COMPACT_LOCALLY_PATH_CONNECTED_EQ_LOCALLY_CONNECTED_EUCLIDEAN LOCALLY_COMPACT_LOCALLY_PATH_CONNECTED_EQ_LOCALLY_CONNECTED_SPACE LOCALLY_COMPACT_PATH_CONNECTED_EQ_CONNECTED_EUCLIDEAN LOCALLY_COMPACT_SPACE_IMP_GDELTA_IN LOCALLY_CONNECTED_CONTINUUM_SPACE LOCALLY_CONSTANT_REFINEMENT LOCALLY_FCCOVERABLE_SPACE LOCALLY_FCCOVERABLE_SPACE_CHAIN MCOMPLETE_CONNECTED_LOCALLY_CONNECTED_IMP_PATH_CONNECTED MCOMPLETE_CONNECTED_LOCALLY_CONNECTED_IMP_PATH_CONNECTED_EUCLIDEAN MCOMPLETE_CONNECTED_LOCALLY_CONNECTED_IMP_PATH_CONNECTED_IN MCOMPLETE_DYADIC_APPROXIMATION MCOMPLETE_IMBEDDING_IN_LC_CONTINUUM MCOMPLETE_IMBEDDING_IN_LC_CONTINUUM_IN MCOMPLETE_IMP_LOCALLY_COMPACT_EUCLIDEAN MCOMPLETE_IN_LOCALLY_COMPACT_IMP_LOCALLY_COMPACT MCOMPLETE_LOCALLY_CONNECTED_IMP_LOCALLY_PATH_CONNECTED MCOMPLETE_LOCALLY_CONNECTED_IMP_LOCALLY_PATH_CONNECTED_EUCLIDEAN MCOMPLETE_LOCALLY_PATH_CONNECTED_EQ_LOCALLY_CONNECTED MCOMPLETE_LOCALLY_PATH_CONNECTED_EQ_LOCALLY_CONNECTED_EUCLIDEAN OPEN_CONNECTED_FINE_COVER PEANO_GAP_FILLING_EXTENSION SECOND_COUNTABLE_CLOSED_MAP_IMAGE SEMI_LOCALLY_CONNECTED_COMPACT_SPACE SEMI_LOCALLY_CONNECTED_CONNECTED SEMI_LOCALLY_CONNECTED_GEN_SPACE SEPARABLE_METRIZABLE_IMP_SECOND_COUNTABLE In Multivariate/paths.ml, three existing long Euclidean-specific proofs are replaced by short bridge derivations from the new general metric space versions: SEMI_LOCALLY_CONNECTED (222 lines reduced to 19), SEMI_LOCALLY_CONNECTED_GEN (65 lines reduced to 19), and LOCALLY_COMPACT_CONNECTED_IMP_PATH_CONNECTED (662 lines reduced to 15). All theorem statements are preserved; only the proofs change. The general metric space versions in metric.ml use a _SPACE suffix to distinguish them from existing Euclidean-specific theorems of the same logical content in paths.ml. For example, the general version is LOCALLY_COMPACT_CONNECTED_IMP_PATH_CONNECTED_SPACE while the Euclidean version retains its original name LOCALLY_COMPACT_CONNECTED_IMP_PATH_CONNECTED.

autonomously formalized by Claude Opus 4.6, approximately following the presentation in Williams's textbook "Probability with Martingales". It includes the development of Lebesgue-type integration theory within the setting of probability measure spaces as part of the foundational material. Among the classic results proved are the Central Limit Theorem, Laws of Large Numbers (weak and strong), Fair Games Theorem (Doob optional stopping), Borel-Cantelli lemmas, martingale convergence and the Azuma-Hoeffding inequality. Also added a proof, entirely autoformalized by Claude Opus 4.6, of the solution to the Buffon Needle problem, in both the "short needle" and "long needle" cases. The statements are formulated in terms of the newly added probability theory, with the "position" and "angle" being independent random variables. New definitions: adapted almost_surely bet_gain bounded_stopping_time char_fn_im char_fn_re cond_prob converges_L2 converges_as converges_in_prob converges_in_prob_const covariance distribution_fn expectation filtration fin_inters gen_cdf gen_char_fn_im gen_char_fn_re gen_converges_L2 indep_events indep_events_seq indep_rv indicator_fn integrable iter_min lambda_generated lambda_system liminf_events limsup_events martingale martingale_transform measurable_wrt natural_filtration nn_expectation nonneg_simple_fn_approx not_bet_gain null_event num_upcrossings pi_system pos_part predictable prob prob_carrier prob_events prob_space_tybij random_variable real_liminf real_limsup running_max sigma_algebra sigma_atom sigma_generated simple_adapted simple_cdf simple_cond_exp simple_covariance simple_expectation simple_mgf simple_rv simple_rv_wrt simple_variance std_normal_cdf std_normal_density stopped_process stopping_time sub_sigma_algebra submartingale supermartingale tail_sigma uniform_rv upcrossing_bet upcrossing_count upcrossing_phase variance and theorems: ABEL_SUMMATION_IDENTITY ABS_DIFF_SAME_SIGN ABS_GE_IFF_POW2_GE ABS_LE_1_PLUS_POW2 ABS_LE_EXP_QUARTER ABS_MUL_BOUND ABS_X_GAUSSIAN_BOUND ALMOST_SURELY_CARRIER ALMOST_SURELY_COUNTABLE_INTER ALMOST_SURELY_EQ ALMOST_SURELY_EVENT ALMOST_SURELY_FROM_PROB_ONE ALMOST_SURELY_INTER ALMOST_SURELY_SUBSET ALMOST_SURELY_UNION ALMOST_SURELY_UNIV ALMOST_SURE_IMP_IN_PROB AM_GM_ABS AM_GM_FRAC_BOUND ARCTAN_INTEGRAL AZUMA_HOEFFDING AZUMA_MGF_BOUND BAYES_THEOREM BCL1_CONVERGENCE BCL1_CONVERGENCE_RV BET_GAIN_DECOMPOSITION BOUNDED_CONTINUOUS_TRIG_APPROX BOUNDED_CONT_TIMES_DENSITY_INTEGRABLE BOUNDED_CONVERGENCE_EXPECTATION BOUNDED_CONVERGENCE_NN BOUNDED_COVARIANCE_ALT BOUNDED_COVARIANCE_CMUL BOUNDED_EXPECTATION_ADD BOUNDED_EXPECTATION_CMUL BOUNDED_EXPECTATION_MONO BOUNDED_EXPECTATION_NONNEG_EQ_NN BOUNDED_EXPECTATION_POS BOUNDED_EXPECTATION_SUB BOUNDED_FINITE_UPCROSSINGS_IMP_CONVERGENT BOUNDED_LIMINF_SANDWICH BOUNDED_NN_EXPECTATION_ADD BOUNDED_NN_EXPECTATION_CMUL BOUNDED_NN_EXPECTATION_GE_SIMPLE BOUNDED_NN_EXPECTATION_MONO BOUNDED_NOT_CONVERGENT_IMP_OSCILLATION BOUNDED_REAL_SEQ_HAS_CONVERGENT_SUBSEQ BOUNDED_VARIANCE_ADD BUFFON_GENERAL BUFFON_GENERAL_BRIDGE BUFFON_GENERAL_CORE_BOUND BUFFON_LONG BUFFON_SHORT CDF_LE_EXPECTATION CDF_LE_INTEGRAL_BOUNDED CHAR_FN_ADD_INDEP_IM CHAR_FN_ADD_INDEP_RE CHAR_FN_DETERMINES_NORMAL_CDF_LIMIT CHAR_FN_IM_BOUND CHAR_FN_IM_DIV CHAR_FN_IM_MEAN_ZERO_BOUND CHAR_FN_MODULUS_LE CHAR_FN_RE_APPROX CHAR_FN_RE_BOUND CHAR_FN_RE_DIV CHAR_FN_RE_POW_CONV_EXP CHAR_FN_SUM_IID_IM_SQ_BOUND CHAR_FN_SUM_IID_MODULUS CHAR_FN_SUM_IID_RE_BOUND CHAR_FN_SUM_IID_TRIANGLE CHAR_FN_ZERO CHEBYSHEV_CONVERGENCE CHEBYSHEV_INEQUALITY CHEBYSHEV_INEQUALITY_SIMPLE CHEBYSHEV_SHIFTED_SUM CHERNOFF_BOUND CLT_CHAR_FN_CONVERGENCE CLT_CHAR_FN_CONVERGENCE_FULL CLT_CHAR_FN_IM_CONVERGENCE CLT_CONVERGENCE_IN_DISTRIBUTION CLT_IM_ERROR_VANISHES CLT_STANDARDIZED CLT_VARIANCE_FORM COMPLEX_PRODUCT_MODULUS_SQ COND_EXP_INDICATOR_DIFF_ZERO COND_PROB_BOUNDS COND_PROB_INTER COND_PROB_SELF CONTINUOUS_LIMIT_SANDWICH CONVERGENCE_SET_IN_EVENTS CONVEX_BOUND_EXP COS_APPROX_BOUND COS_LOWER_BOUND COS_PERIODIC_N COS_PI_SUB COS_TAYLOR2_BOUND COS_TAYLOR_BOUND_4 COS_TAYLOR_CONVERGES COS_TAYLOR_NONNEG COS_TAYLOR_UPPER COUNTABLE_DISJOINT_DECOMP_DISJOINT COUNTABLE_GSPEC_NUM COUNTABLE_RATIONAL_SETS COUNTABLE_UNION_DISJOINT_DECOMP COVARIANCE_ADD_LEFT COVARIANCE_ALT COVARIANCE_CMUL COVARIANCE_INDEP COVARIANCE_INDEP_SIMPLE COVARIANCE_SELF COVARIANCE_SELF_GENERAL COVARIANCE_SIMPLE_AGREE COVARIANCE_SUM_LEFT COVARIANCE_SYM COVARIANCE_SYM_GENERAL CROSS_MULT_BOUND DERIV_NEG_X_GAUSSIAN DIST_FN_IN_EVENTS DIST_FN_LE_1 DIST_FN_MONO DIST_FN_NONNEG DOMINATED_CONVERGENCE DOMINATED_CONVERGENCE_NULL DOOB_DECOMPOSITION DOOB_MAXIMAL_INEQUALITY DOOB_MAXIMAL_INEQUALITY_GENERAL DOOB_MAXIMAL_INEQUALITY_STRONG DOOB_OPTIONAL_STOPPING_BOUNDED DOOB_OPTIONAL_STOPPING_GENERAL DOOB_UPCROSSING_INEQUALITY DYNKIN_PI_LAMBDA EXPECTATION_ABS_BOUND EXPECTATION_ABS_LE EXPECTATION_ADD EXPECTATION_ADD_SIMPLE EXPECTATION_AFFINE EXPECTATION_BOUND EXPECTATION_CMUL EXPECTATION_CMUL_NONNEG EXPECTATION_CMUL_SIMPLE EXPECTATION_CONST EXPECTATION_EXT EXPECTATION_INDICATOR EXPECTATION_LE_CDF EXPECTATION_LE_GEN_CDF EXPECTATION_MONO EXPECTATION_MONO_SIMPLE EXPECTATION_MUL_INDICATOR_ZERO_PROB EXPECTATION_NEG EXPECTATION_NEG_INTEGRABLE EXPECTATION_NEG_SIMPLE EXPECTATION_NONNEG_EQ_NN EXPECTATION_POS EXPECTATION_PRODUCT_BOUNDED_INDEP EXPECTATION_PRODUCT_COMPOSE_SIMPLE_INDEP EXPECTATION_PRODUCT_INDEP EXPECTATION_PRODUCT_INDEP_SIMPLE EXPECTATION_SIMPLE_AGREE EXPECTATION_SUB EXPECTATION_SUB_SIMPLE EXPECTATION_SUM EXPECTATION_SUM_SIMPLE EXPECTATION_TRUNCATION_LIMIT EXPECTATION_TRUNCATION_PRODUCT_LIMIT EXP_DIFF_LE EXP_NEG_ADD EXP_NEG_LE_POW EXP_NEG_SQ_REAL_CONTINUOUS EXP_NEG_X2_CONTINUOUS EXP_NEG_X2_INTEGRABLE EXP_QUAD_ANTIDERIV FATOU_EVENTS_LIMINF FATOU_EVENTS_LIMSUP FATOU_INTEGRABLE FATOU_NN_EXPECTATION FILTRATION_MONO FINITE_SIGMA_ATOMS FINITE_UNION_BOUNDED_BY_INFSUM FINITE_UNION_CONVERGENCE FINITE_UPCROSSINGS_AS FIN_INTERS_PI_SYSTEM FIRST_BOREL_CANTELLI FOUR_AB_LE_APB_SQ FTC_SQUARE FTC_SQUARE_DERIV GAP_LIMIT GAUSSIAN_ANTIDERIV_BOUND GAUSSIAN_COS_INTEGRABLE GAUSSIAN_COS_INTEGRAL_HAS_DERIV GAUSSIAN_EXP_DECAY GAUSSIAN_FT GAUSSIAN_FT_ANTIDERIV_DERIV GAUSSIAN_FT_IBP GAUSSIAN_FT_SIN GAUSSIAN_INTEGRAL GAUSSIAN_INTEGRAL_SCALED GAUSSIAN_INTEGRAL_TRIG_POLY GAUSSIAN_QUARTER_INTEGRABLE GAUSSIAN_T2_INTEGRABLE GAUSSIAN_T2_POINTWISE_BOUND GAUSSIAN_T_SIN_INTEGRABLE GAUSS_2D_CONTINUOUS GAUSS_INNER_REWRITE GAUSS_INTEGRAL_DERIV GAUSS_SQ_FTC GAUSS_SUBSTITUTION GENERAL_CLT GEN_CDF_BOUNDS GEN_CDF_LE_EXPECTATION GEN_CDF_SIMPLE_AGREE GEN_CHAR_FN_ADD_INDEP_IM GEN_CHAR_FN_ADD_INDEP_RE GEN_CHAR_FN_DETERMINES_NORMAL_CDF_LIMIT GEN_CHAR_FN_IM_BOUND GEN_CHAR_FN_IM_DIV GEN_CHAR_FN_IM_SIMPLE GEN_CHAR_FN_MODULUS_LE GEN_CHAR_FN_RE_BOUND GEN_CHAR_FN_RE_DIV GEN_CHAR_FN_RE_LOWER_BOUND GEN_CHAR_FN_RE_POW_CONV_EXP GEN_CHAR_FN_RE_SIMPLE GEN_CHAR_FN_RE_UPPER_BOUND GEN_CHAR_FN_RE_ZERO GEN_CHAR_FN_SUM_IID_IM_SQ_BOUND GEN_CHAR_FN_SUM_IID_MODULUS_RV GEN_CHAR_FN_SUM_IID_RE_BOUND GEN_CLT_CHAR_FN_CONVERGENCE GEN_CLT_CHAR_FN_IM_CONVERGENCE GEN_CLT_IM_ERROR_VANISHES GEN_CLT_RE_PERTURBATION_VANISHES GEN_CONVERGES_L2_AGREE GEN_STEP_C_BOUND GEN_TRIG_POLY_WEAK_CONVERGENCE GEN_WEAK_CONVERGENCE_FROM_CHAR_FN G_SET_UNION_OF_ATOMS HALF_GAUSSIAN_CONVERGES HAS_INTEGRAL_TRIG_TERM HAS_REAL_DERIVATIVE_ZERO_CONSTANT HAS_REAL_INTEGRAL_CMUL_SIN HAS_REAL_INTEGRAL_CMUL_SIN_0_PI HAS_REAL_INTEGRAL_SIN HAS_REAL_INTEGRAL_SIN_0_PI HAS_REAL_INTEGRAL_STRETCH_UNIV HB_NONNEG HOEFFDING_ANALYTIC_LEMMA HOEFFDING_DENOM_POS HOEFFDING_EXP_L_EQ HOEFFDING_LEMMA HOEFFDING_LPRIME_AT_ZERO HOEFFDING_LPRIME_HAS_DERIV HOEFFDING_L_AT_ZERO HOEFFDING_L_HAS_DERIV HOEFFDING_L_TAYLOR_BOUND HOEFFDING_MGF_SUM_BOUND HOEFFDING_SECOND_DERIV_ABS_BOUND HOEFFDING_SECOND_DERIV_BOUND HOEFFDING_SINGLE HOEFFDING_SUM HOEFFDING_SUM_GENERAL H_INTEGRAND_INTEGRABLE H_LIMIT_ZERO H_PLUS_J IB_NONNEG IB_SQ_EQ IMAGE_LIFT_REAL_INTERVAL IMAGE_NEG_UNIV IMAGE_NEG_UNIV_REAL INCREASING_A0_DISJOINT_DIFFS INCREASING_BOUNDED_CONVERGES_TO_SUP INCREASING_MONO INCREASING_UNION_DECOMP INDEP_COMPL_INTERS_NUMSEG INDEP_COMPL_INTERS_NUMSEG_BOTH INDEP_COMPL_SINGLE_INTER INDEP_EVENTS_COMPL INDEP_EVENTS_COMPL_BOTH INDEP_EVENTS_COND_PROB INDEP_EVENTS_EMPTY INDEP_EVENTS_PROB_ONE INDEP_EVENTS_PROB_ZERO INDEP_EVENTS_SPACE INDEP_EVENTS_SYM INDEP_EXTENDS_TO_SIGMA INDEP_FIN_INTER_SIGMA_FUTURE INDEP_JOINT_CDF INDEP_LAMBDA_SYSTEM INDEP_RECT_PROB INDEP_RV_ADD_CONST INDEP_RV_DIST_FN INDEP_RV_IMP_RV INDEP_RV_MAX_CONST INDEP_RV_MIN_CONST INDEP_RV_NSFA INDEP_RV_POINT_MASS INDEP_RV_SHIFT INDEP_RV_STRICT_INEQ INDEP_RV_SYM INDICATOR_FN_DISJOINT_UNION INDICATOR_FN_ETA INDICATOR_FN_INTER INFINITE_EXTRACT_SUBSEQ INFINITE_UPCROSSINGS_NULL INNER_INTEGRAND_INTEGRABLE INNER_SUM_REINDEX INNER_VEC_CONV INNER_X_INTEGRAL INTEGRABLE_ABS INTEGRABLE_ADD INTEGRABLE_BOUNDED INTEGRABLE_CLT INTEGRABLE_CMUL INTEGRABLE_CONST INTEGRABLE_COS_CMUL INTEGRABLE_DOMINATED INTEGRABLE_INDICATOR INTEGRABLE_MAX INTEGRABLE_MIN INTEGRABLE_MUL_SQUARE INTEGRABLE_NEG INTEGRABLE_NEG_PART INTEGRABLE_NONNEG_NN_BOUNDED INTEGRABLE_POS_PART INTEGRABLE_SIMPLE INTEGRABLE_SIN_CMUL INTEGRABLE_SUB INTEGRABLE_SUM INTEGRABLE_SUM_SQUARE INTEGRABLE_TAYLOR_REMAINDER INTEGRAL_BOUNDED_LE_CDF INTEGRAND_BOUND INTEGRAND_SUM_EQ_INV INTERS_COMPL_UNIONS INTERS_IMAGE_IN_EVENTS INTERS_IMAGE_NUMSEG_SUC INTERS_TAIL_UNIONS_SUBSET_COMPL ITER_MIN_LE ITER_MIN_MONO ITER_MIN_POS JENSEN JOINT_LEVEL_SETS_DISJOINT_Y J_EQUALS_OUTER J_OUTER_INTEGRAND_INTEGRABLE KOLMOGOROV_ZERO_ONE KRONECKER_LEMMA L2_IMP_IN_PROB LAMBDA_GENERATED_GA_IS_LAMBDA LAMBDA_GENERATED_INTER_CLOSED LAMBDA_GENERATED_INTER_PI LAMBDA_GENERATED_IS_LAMBDA LAMBDA_GENERATED_MEM LAMBDA_GENERATED_MINIMAL LAMBDA_GENERATED_SUBSET LAMBDA_GENERATED_SUBSET_U LAMBDA_SYSTEM_DIFF LAMBDA_SYSTEM_EMPTY LAMBDA_SYSTEM_INTER_IMP_SIGMA LAMBDA_SYSTEM_UNION2 LEVY_CONTINUITY_CLT LE_2_EXP LIFT_DROP_FSTCART LIFT_DROP_SNDCART LIFT_EXP_DROP_CONTINUOUS LIFT_ZERO LIMINF_EVENTS_ALT LIMINF_EVENTS_IN_EVENTS LIMINF_SUBSET_LIMSUP LIMSUP_BAD_SUBSET_COMPL_CONV LIMSUP_EVENTS_ALT LIMSUP_EVENTS_IN_EVENTS LIMSUP_SUBSET_TAIL LOG_LOWER_BOUND MARKOV_INEQUALITY MARKOV_INEQUALITY_SIMPLE MARKOV_SECOND_MOMENT MARTINGALE_COND_EXP MARTINGALE_CONST MARTINGALE_CONVERGENCE_BOUNDED MARTINGALE_DIFF_CONVEX_INDICATOR MARTINGALE_DIFF_EXP_ADAPTED_BOUND MARTINGALE_DIFF_EXP_INDICATOR_BOUND MARTINGALE_DIFF_INDICATOR_ZERO MARTINGALE_EXPECTATION_CONST MARTINGALE_IMP_SUBMARTINGALE MARTINGALE_IMP_SUPERMARTINGALE MARTINGALE_STOPPED_PROCESS MARTINGALE_SUB_SUPER MCT_NN_EXPECTATION MCT_NN_EXPECTATION_RV MEASURABLE_WRT_ADD MEASURABLE_WRT_COMPOSE MEASURABLE_WRT_CONST MEASURABLE_WRT_CONSTANT_ON_ATOM MEASURABLE_WRT_EQ_ON_CARRIER MEASURABLE_WRT_EVENTS MEASURABLE_WRT_GE MEASURABLE_WRT_IF MEASURABLE_WRT_IMP_RV MEASURABLE_WRT_LEVEL_SET MEASURABLE_WRT_LT MEASURABLE_WRT_MONO MEASURABLE_WRT_STRICT_LT MEASURABLE_WRT_SUB MEASURABLE_WRT_SUM_FILTRATION_1 MIN_ABS_LIPSCHITZ MIN_CONTRACTION MIN_SIN_INTEGRAL_LONG MIN_SIN_INTEGRAL_SHORT MIN_SIN_OSCILLATION MONOTONE_EXTENDS MONO_SEQ_LE MUL_LNEG_LE NEG_DIV_NEG NN_EXPECTATION_ADD NN_EXPECTATION_ADD_GE NN_EXPECTATION_CMUL NN_EXPECTATION_CONST NN_EXPECTATION_CONST_MINUS NN_EXPECTATION_EXT NN_EXPECTATION_GE_SIMPLE NN_EXPECTATION_INTEGRABLE_BOUND NN_EXPECTATION_LE NN_EXPECTATION_LE_FROM_SIMPLE NN_EXPECTATION_MIN_LIMIT NN_EXPECTATION_MONO NN_EXPECTATION_POS NN_EXPECTATION_PRODUCT_BOUNDED_INDEP NN_EXPECTATION_SIMPLE NN_EXPECTATION_UPPER_BOUND NN_EXPECT_SET_NONEMPTY NONNEG_APPROX_INDEX_FINITE NONNEG_APPROX_INDEX_NONEMPTY NONNEG_APPROX_SET_FINITE NONNEG_APPROX_SET_NONEMPTY NONNEG_PARTIAL_SUMS_UNBOUNDED NONNEG_SIMPLE_FN_APPROX_CONVERGES NONNEG_SIMPLE_FN_APPROX_GAP NONNEG_SIMPLE_FN_APPROX_IN_GRID NONNEG_SIMPLE_FN_APPROX_LE NONNEG_SIMPLE_FN_APPROX_MONO NONNEG_SIMPLE_FN_APPROX_NONNEG NONNEG_SIMPLE_FN_APPROX_RV NONNEG_SIMPLE_FN_APPROX_SIMPLE_RV NOT_BET_GAIN_POS_PART_NONNEG NSFA_CDF_CHAR NSFA_CDF_EQUIV NULL_EVENT_COMPL NULL_EVENT_COMPL_ONE NULL_EVENT_COUNTABLE_UNION NULL_EVENT_DIFF NULL_EVENT_EMPTY NULL_EVENT_IFF_PROB_ZERO NULL_EVENT_INTER NULL_EVENT_SUBSET NULL_EVENT_UNION NUM_SQRT_EXISTS NUM_UPCROSSINGS_GE_EVENT NUM_UPCROSSINGS_MONO ONE_MINUS_COS_LE ONE_MINUS_COS_NONNEG ONE_MINUS_EXP_NEG_LE OPEN_HALFLINE_AS_UNION OPEN_HALFLINE_AS_UNION_BACKWARD OPEN_HALFLINE_AS_UNION_FORWARD OUTER_INTEGRAND_INTEGRABLE OUTER_VEC_CONV PERIODIC_REAL_BOUND POS_PART_BOUND POS_PART_INDICATOR_FORM POS_PART_LE_IFF POS_PART_NEG POS_PART_NONNEG POS_PART_POS POW_2_LE_SQRT POW_DIFF_BOUND_UNIT POW_EXP_NEG_DIFF POW_LE_EXP_NEG PROB_ADDITIVE PROB_CARRIER_IN_EVENTS PROB_CARRIER_NONEMPTY PROB_COMPL PROB_COMPL_IN_EVENTS PROB_CONTINUITY_FROM_ABOVE PROB_CONTINUITY_FROM_BELOW PROB_CONTINUITY_FROM_BELOW' PROB_CONVERGENCE_EVENTS PROB_COUNTABLE_INTERS_IN_EVENTS PROB_COUNTABLE_INTER_ONE PROB_COUNTABLE_SUBADDITIVE_INDEXED PROB_COUNTABLE_UNION_IN_EVENTS PROB_COUNTABLE_UNION_ZERO PROB_COUNTABLY_ADDITIVE PROB_DIFF PROB_DIFF_IN_EVENTS PROB_DIFF_SUBSET PROB_EMPTY PROB_EMPTY_IN_EVENTS PROB_EVENT_SUBSET PROB_FINITE_ADDITIVE PROB_FINITE_ADDITIVE_IMAGE PROB_FINITE_INDEXED_UNION_IN_EVENTS PROB_FINITE_SUBADDITIVE PROB_FINITE_SUBADDITIVE' PROB_FINITE_UNION_IN_EVENTS PROB_INCLUSION_EXCLUSION PROB_INDEXED_INTER_IN_EVENTS PROB_INDEXED_UNION_IN_EVENTS PROB_INTER_IN_EVENTS PROB_INTER_LOWER_BOUND PROB_LEVEL_SET_AS_SUM PROB_LE_1 PROB_MONO PROB_ONE_INTER PROB_ONE_UNION PROB_POINTWISE_TAIL_VANISHES PROB_POSITIVE PROB_SPACE PROB_SPACE_EXTRACT PROB_SPACE_SIGMA_ALGEBRA PROB_SUBADDITIVE PROB_SUBADDITIVE_3 PROB_SUBADDITIVE_FINITE PROB_SUBSET_DIFF PROB_SYMMETRIC_DIFFERENCE PROB_TAIL_SUBADDITIVE PROB_TOTAL_TWO PROB_UNION PROB_UNIONS_INCREASING_BOUND PROB_UNION_3 PROB_UNION_IN_EVENTS PROB_ZERO_INTER PROB_ZERO_TAC PROB_ZERO_UNION PRODUCT_ONE_MINUS_LE_EXP_NEG PRODUCT_ONE_MINUS_TENDS_TO_ZERO PROD_REARRANGE RANDOM_VARIABLE_ABS RANDOM_VARIABLE_ADD RANDOM_VARIABLE_CMUL RANDOM_VARIABLE_COMP_CONTINUOUS RANDOM_VARIABLE_CONST RANDOM_VARIABLE_COS RANDOM_VARIABLE_GE RANDOM_VARIABLE_GT RANDOM_VARIABLE_INF_SEQ RANDOM_VARIABLE_ITER_MIN RANDOM_VARIABLE_LEVEL_SET RANDOM_VARIABLE_MAX RANDOM_VARIABLE_MIN RANDOM_VARIABLE_MUL RANDOM_VARIABLE_NEG RANDOM_VARIABLE_NEG_PART RANDOM_VARIABLE_OPEN_HALFLINE RANDOM_VARIABLE_OPEN_INTERVAL RANDOM_VARIABLE_POINTWISE_LIMIT RANDOM_VARIABLE_POS_PART RANDOM_VARIABLE_POW RANDOM_VARIABLE_PREIMAGE_OPEN RANDOM_VARIABLE_SCALE RANDOM_VARIABLE_SHIFT RANDOM_VARIABLE_SIN RANDOM_VARIABLE_SQUARE RANDOM_VARIABLE_STRICT_LT RANDOM_VARIABLE_SUB RANDOM_VARIABLE_SUB_CONST RANDOM_VARIABLE_SUM RATIONAL_ENUMERATION REALLIM_1_OVER_SUC REALLIM_CONTINUOUS_FUNCTION REALLIM_COS REALLIM_EXP_NEG REALLIM_EXP_NEG_SQ REALLIM_IMP_REAL_LIMINF REALLIM_INV_SQRT_SUC REALLIM_MIN_CONST REALLIM_NULL_SQABS REALLIM_POW_EXP_NEG REALLIM_POW_EXP_NEG_PERTURB REALLIM_SIN REALLIM_SQRT_NULL REALLIM_SUBSEQUENCE REALLIM_SUBSEQUENCE_SQUARES REALLIM_SUBSEQ_SAME_LIMIT REALLIM_TRUNCATION REAL_ABS_TRIANGLE_SUB REAL_ARCH_INV_SUC REAL_CONTINUOUS_OPEN_PREIMAGE_UNIV REAL_CONVEX_ON_SUBGRADIENT REAL_DIFF_SQ_BOUND REAL_EQ_0_FROM_INV_BOUND REAL_EQ_EPSILON REAL_EQ_RDIV_CANCEL REAL_EXP_DECAY_BOUND REAL_EXP_NEG_LT_INV REAL_INTEGRAL_REFL REAL_LE_FROM_SCALE REAL_LE_INV_CROSS REAL_LE_SEQUENTIALLY REAL_LIMINF_EVENTUALLY_LBOUND REAL_LIMINF_LBOUND REAL_LIMINF_LE_LIMSUP REAL_LIMINF_LIMSUP_CONVERGES REAL_LIMINF_MONO REAL_LIMINF_UBOUND REAL_LIMSUP_EVENTUALLY_UBOUND REAL_MAX_GE REAL_MAX_MUL_NONNEG REAL_MIN_REFL REAL_MUL_4_FACTOR REAL_MUL_SUB_DECOMP REAL_MUL_SUB_REARRANGE REAL_OF_NUM_COND_01 REAL_OPEN_HALFSPACE_LT REAL_POW_DIFF_BOUND REAL_POW_POW_SWAP REAL_SQ_DIFF_FACTOR REAL_SQ_LE_ABS REAL_SUB_MUL_FACTOR RUNNING_MAX_EXCEEDS_IN_FILTRATION RV_LEVEL_GE_IN_EVENTS RV_LEVEL_GT_IN_EVENTS RV_LEVEL_LE_RV SAMPLE_MEAN_INTERPOLATION SANDWICH_ABS_BOUND SCALED_APPROX_BOUND SCHEFFE_LEMMA SECOND_BOREL_CANTELLI SET_IN_SIMP SIGMA_ALGEBRA_CARRIER SIGMA_ALGEBRA_COMPL SIGMA_ALGEBRA_DIFF SIGMA_ALGEBRA_EMPTY SIGMA_ALGEBRA_INTER SIGMA_ALGEBRA_INTERS_FINITE SIGMA_ALGEBRA_IS_PI_SYSTEM SIGMA_ALGEBRA_POWERSET SIGMA_ALGEBRA_POWERSET_CARRIER SIGMA_ALGEBRA_SUBSET SIGMA_ALGEBRA_UNION SIGMA_ALGEBRA_UNIONS_FINITE SIGMA_ALGEBRA_UNION_COUNTABLE SIGMA_ATOM_CONTAINS SIGMA_ATOM_EQUAL_OR_DISJOINT SIGMA_ATOM_IN_G SIGMA_ATOM_SAME SIGMA_ATOM_SUBSET SIGMA_ATOM_SUBSET_CARRIER SIGMA_GENERATED_CARRIER SIGMA_GENERATED_IS_SIGMA_ALGEBRA SIGMA_GENERATED_MEM SIGMA_GENERATED_MINIMAL SIGMA_GENERATED_MONO SIGMA_GENERATED_SUBSET_EVENTS SIGMA_GENERATED_SUPERSET SIMPLE_ADAPTED_STOPPED_PROCESS SIMPLE_CDF_AS_EXPECTATION SIMPLE_CDF_BOUNDS SIMPLE_CHEBYSHEV_CONVERGENCE SIMPLE_CHEBYSHEV_INEQUALITY SIMPLE_COND_EXP_ATOM_COND SIMPLE_COND_EXP_CONDITIONING SIMPLE_COND_EXP_CONSTANT_ON_ATOM SIMPLE_COND_EXP_EXISTS SIMPLE_COND_EXP_MEASURABLE_WRT_G SIMPLE_COND_EXP_PROPERTY SIMPLE_COND_EXP_RANGE_FINITE SIMPLE_COND_EXP_SIMPLE_RV SIMPLE_COND_EXP_SIMPLE_RV_WRT SIMPLE_COVARIANCE_ADD_LEFT SIMPLE_COVARIANCE_ALT SIMPLE_COVARIANCE_INDEP SIMPLE_COVARIANCE_SUM_LEFT SIMPLE_EXPECTATION_ABS_LE SIMPLE_EXPECTATION_ADD SIMPLE_EXPECTATION_CAUCHY_SCHWARZ SIMPLE_EXPECTATION_CMUL SIMPLE_EXPECTATION_CMUL_INDICATOR_PAIR SIMPLE_EXPECTATION_COMPOSE_SUM SIMPLE_EXPECTATION_CONST SIMPLE_EXPECTATION_DOUBLE_SUM SIMPLE_EXPECTATION_EXT SIMPLE_EXPECTATION_GE_ON_EVENT SIMPLE_EXPECTATION_INDICATOR SIMPLE_EXPECTATION_INDICATOR_MEASURABLE SIMPLE_EXPECTATION_LOWER_BOUND SIMPLE_EXPECTATION_MONO SIMPLE_EXPECTATION_MUL_INDICATOR_CARRIER SIMPLE_EXPECTATION_NEG SIMPLE_EXPECTATION_POS SIMPLE_EXPECTATION_POW2_DIV SIMPLE_EXPECTATION_PRODUCT_COMPOSE_INDEP SIMPLE_EXPECTATION_PRODUCT_DOUBLE_SUM SIMPLE_EXPECTATION_PRODUCT_INDEP SIMPLE_EXPECTATION_QUADRATIC SIMPLE_EXPECTATION_SQ_LE SIMPLE_EXPECTATION_SUB SIMPLE_EXPECTATION_SUM_FINITE SIMPLE_EXPECTATION_SUM_NUMSEG SIMPLE_EXPECTATION_SUM_ZERO SIMPLE_EXPECTATION_TRIG_TERM SIMPLE_EXPECTATION_UPPER_BOUND SIMPLE_JENSEN SIMPLE_LEVY_CONTINUITY_CLT SIMPLE_MCT_NN_EXPECTATION SIMPLE_MGF_ADD_INDEP SIMPLE_MGF_CONVEX_BOUND SIMPLE_MGF_NONNEG SIMPLE_PROB_SUM_ONE SIMPLE_RV_ABS SIMPLE_RV_ABS_BOUNDED SIMPLE_RV_ADD SIMPLE_RV_AGREE SIMPLE_RV_BOUNDED SIMPLE_RV_CMUL SIMPLE_RV_CMUL_INDICATOR_PAIR SIMPLE_RV_COMPOSE_SUM_INDICATOR SIMPLE_RV_CONST SIMPLE_RV_DIV SIMPLE_RV_EXP SIMPLE_RV_EXT SIMPLE_RV_GAP_BELOW SIMPLE_RV_GE_EVENT SIMPLE_RV_INDICATOR SIMPLE_RV_LEVEL_SET_INTER_IN_EVENTS SIMPLE_RV_MAX SIMPLE_RV_MIN SIMPLE_RV_MUL SIMPLE_RV_NEG SIMPLE_RV_NOT_BET_INDICATOR SIMPLE_RV_NUM_UPCROSSINGS SIMPLE_RV_POS_PART SIMPLE_RV_POS_PART_SUB SIMPLE_RV_PRODUCT_SUM_INDICATOR SIMPLE_RV_REAL_COMPOSE SIMPLE_RV_SQUARE SIMPLE_RV_STOPPED_PROCESS SIMPLE_RV_STOPPING_TIME_INDICATOR SIMPLE_RV_SUB SIMPLE_RV_SUM SIMPLE_RV_SUM_DIV SIMPLE_RV_SUM_FINITE SIMPLE_RV_SUM_NUMSEG SIMPLE_RV_SUM_NUMSEG_1 SIMPLE_RV_UPPER_BOUND SIMPLE_RV_WRT_IMP_SIMPLE_RV SIMPLE_SLLN_SUBSEQ SIMPLE_STRONG_LAW_OF_LARGE_NUMBERS SIMPLE_TIGHTNESS_FROM_SECOND_MOMENTS SIMPLE_VARIANCE_ADD SIMPLE_VARIANCE_ADD_UNCORRELATED SIMPLE_VARIANCE_ALT SIMPLE_VARIANCE_CMUL SIMPLE_VARIANCE_CONST SIMPLE_VARIANCE_MEAN_ZERO SIMPLE_VARIANCE_NONNEG SIMPLE_VARIANCE_SUM_IID SIMPLE_VARIANCE_SUM_UNCORRELATED SIMPLE_WEAK_LAW_OF_LARGE_NUMBERS SIN_APPROX_BOUND SIN_DENSITY_INTEGRABLE SIN_LIPSCHITZ SIN_MINUS_X_SQ_BOUND SIN_PERIODIC_N SIN_PI_SUB SIN_POW2_LE SIN_SCALED_ERROR_VANISHES SIN_TAYLOR_CONVERGES SKOLEM_PAIR SLLN_GAP_CONTROL SLLN_SUBSEQ SQRT_2PI_CANCEL SQRT_2PI_INV SQRT_PI_HALF_SQ STD_NORMAL_CDF_BOUNDS STD_NORMAL_CDF_CONTINUOUS STD_NORMAL_CDF_INTERVAL STD_NORMAL_CDF_MONO STD_NORMAL_CHAR_FN_IM STD_NORMAL_CHAR_FN_RE STD_NORMAL_DENSITY_BOUND STD_NORMAL_DENSITY_CONTINUOUS STD_NORMAL_DENSITY_EVEN STD_NORMAL_DENSITY_INTEGRABLE STD_NORMAL_DENSITY_INTEGRABLE_HALFLINE STD_NORMAL_DENSITY_INTEGRABLE_UPPER_HALFLINE STD_NORMAL_DENSITY_INTEGRAL STD_NORMAL_DENSITY_NONNEG STD_NORMAL_DENSITY_POS STD_NORMAL_DENSITY_SYM STD_NORMAL_MEAN_ZERO STD_NORMAL_MEAN_ZERO_INTEGRAL STD_NORMAL_SECOND_MOMENT STD_NORMAL_SECOND_MOMENT_INTEGRAL STEP_C_BOUND STEP_D_BOUND STOPPED_PROCESS_INCREMENT STOPPED_PROCESS_MEASURABLE_WRT STOPPED_PROCESS_ZERO STOPPING_TIME_INDICATOR_PREDICTABLE STRICTLY_INCREASING_GE STRONG_LAW_FINITE_VARIANCE STRONG_LAW_OF_LARGE_NUMBERS STRONG_LAW_OF_LARGE_NUMBERS_SIMPLE SUBADDITIVE_TAC SUBMARTINGALE_COND_EXP_GE SUBMARTINGALE_EXPECTATION_INCREASING SUBMARTINGALE_EXPECTATION_MONO SUBMARTINGALE_LOCALIZED_INCREASING SUBMARTINGALE_OPTIONAL_STOPPING_GE SUBMARTINGALE_POS_PART_STEP SUBMARTINGALE_STOPPED_PROCESS SUBMARTINGALE_SUB_CONST_STEP SUB_SIGMA_ALGEBRA_CARRIER_IN SUB_SIGMA_ALGEBRA_COMPL SUB_SIGMA_ALGEBRA_DIFF SUB_SIGMA_ALGEBRA_INTER SUB_SIGMA_ALGEBRA_IN_EVENTS SUB_SIGMA_ALGEBRA_UNION SUMMABLE_INV_SUC_SQUARES SUM_OPEN_HALFLINE_AS_RATIONAL_UNION SUM_SUPPORT_EQ SUPERMARTINGALE_EXPECTATION_DECREASING SUPERMARTINGALE_EXPECTATION_MONO SUPERMARTINGALE_OPTIONAL_STOPPING_LE SUPERMARTINGALE_STOPPED_PROCESS S_SQ_DECOMP_BOUND TAIL_INFSUM_TENDS_TO_ZERO TAIL_INTERS_INCREASING TAIL_INTERS_IN_EVENTS TAIL_UNION_DECREASING TAIL_UNION_IN_EVENTS TAIL_UNION_PROB_ONE TAYLOR_REMAINDER_EXPECTATION TIGHTNESS_FROM_SECOND_MOMENTS TRIG_POLY_WEAK_CONVERGENCE TRUNC_ABS TRUNC_SAME_SIGN UNIFORM_RECT_PROB UNIFORM_RV_BOUNDS UNIFORM_RV_CDF_HIGH UNIFORM_RV_CDF_LOW UNIFORM_RV_CDF_MID UNIFORM_RV_CDF_ZERO UNIFORM_RV_IMP_RV UNIFORM_ZERO_CDF_RANGE UNIONS_GEQ_SHIFT UNIONS_IMAGE_NUMSEG_FULL UPCROSSING_BOUND UPCROSSING_BOUND_INVARIANT UPCROSSING_COUNT_AT_TRANSITION UPCROSSING_COUNT_INCREASING UPCROSSING_COUNT_INCREMENT UPCROSSING_COUNT_ITERATE UPCROSSING_COUNT_MONO UPCROSSING_COUNT_PHASE1_INCREMENT UPCROSSING_COUNT_SHIFT UPCROSSING_EXPECTATION_BOUND UPCROSSING_INEQUALITY_POINTWISE UPCROSSING_PHASE_BELOW UPCROSSING_PHASE_BINARY UPCROSSING_PHASE_SET_IN_FILTRATION UPCROSSING_PHASE_SHIFT UPCROSSING_PHASE_SUC_0 UPCROSSING_PHASE_SUC_1 UPCROSSING_PHASE_TRANSITION_1 UPCROSSING_POINTWISE_SUM_BOUND UPCROSSING_PROB_BOUND VARIANCE_ADD VARIANCE_ADD_INDEPENDENT VARIANCE_ADD_SIMPLE VARIANCE_ALT VARIANCE_CMUL VARIANCE_CONST VARIANCE_MEAN_ZERO VARIANCE_NONNEG VARIANCE_SHIFT VARIANCE_SIMPLE VARIANCE_SUM_IID VARIANCE_SUM_UNCORRELATED VARIANCE_SUM_UNCORRELATED_SIMPLE WEAK_CONVERGENCE_FROM_CHAR_FN WEAK_LAW_OF_LARGE_NUMBERS WEAK_LAW_OF_LARGE_NUMBERS_SIMPLE WLLN_CONVERGENCE X2_GAUSSIAN_HAS_INTEGRAL X2_MINUS_1_GAUSSIAN_HAS_INTEGRAL_0 X_GAUSSIAN_INTEGRABLE

aqjune-aws and others added 15 commits January 29, 2026 08:37

Merge pull request jrh13#151 from aqjune-aws/unify_refl

c87954f

Add UNIFY_REFL_TAC to unify metavariables in equality

Merge pull request jrh13#153 from jargh/master

9b73aef

Rabin's irreducibility test for polynomials over finite fields

Merge remote-tracking branch 'hol-light/master'

7f38a57

dnezam merged commit 7005f23 into master Mar 24, 2026
1 check failed

dnezam deleted the merge-hol-light branch March 24, 2026 01:28

Navigation Menu

Uh oh!

Merge in current HOL Light - #6

Merge in current HOL Light#6
dnezam merged 15 commits into
masterfrom
merge-hol-light

dnezam commented Mar 24, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

dnezam commented Mar 24, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants