Merge/jrh13 master 20260825 by tanyongkiam · Pull Request #16 · CakeML/candle

tanyongkiam · 2026-08-25T16:57:43Z

No description provided.

monic and reciprocal polynomials, formal (univariate) polynomial derivatives plus actual division and remainder functions for polynomials. Much of this material was adopted from the existing formalization in 100/transcendence.ml into the main libraries, though with some notable differences as described below (in particular ring_squarefree). Added group theorems ABELIAN_QUOTIENT_GROUP_DIV and SOLVABLE_GROUP_MONOMORPHIC_PREIMAGE, as well as slightly incompatibly tweaking the statement of ABELIAN_QUOTIENT_COMMUTATOR to make its quantifier structure more harmonious with the library. Replaced List.filteri (OCaml >= 4.14) in Probability/clt.ml with subtract/el for compatibility with older OCamls. New definitions: monic poly_deriv poly_div poly_recip poly_rem ring_squarefree and theorems: ABELIAN_QUOTIENT_GROUP_DIV ALGEBRAICALLY_CLOSED_FIELD_EQ_SPLITS_ALT ALGEBRAICALLY_CLOSED_FIELD_SPLITS COEFF_0 COEFF_0_POLY_RECIP_EQ_0 COEFF_ABOVE_DEG COEFF_COMPOSE COEFF_POLY_DERIV COEFF_POLY_LMUL COEFF_POLY_MUL_ALT COEFF_POLY_MUL_VAR COEFF_POLY_MUL_VARPOW COEFF_POLY_RECIP COEFF_POLY_RMUL COEFF_POLY_VAR COEFF_POLY_VARPOW COEFF_POLY_VARPOW_MUL COEFF_POLY_VAR_MUL COPRIME_POLY_NO_COMMON_ROOT COPRIME_POLY_NO_COMMON_ROOT_I FIELD_EXTENSION_TRANS_I FIELD_MONIC_ASSOCIATE FIELD_MONIC_IRREDUCIBLE_ASSOCIATE FUN_ONE_EQ_ONE FUN_ONE_NUM_EQ INTEGER_RING_POW INTEGRAL_DOMAIN_PRIMES_COPRIME_OR_ASSOCIATES INTEGRAL_DOMAIN_PRIMES_DIVIDES_EQ_ASSOCIATES INTEGRAL_DOMAIN_PRIME_PRODUCT_DIVIDES IRREDUCIBLE_ALGEBRAICALLY_CLOSED_FIELD IRREDUCIBLE_IMP_POLY_DEG_NZ ISOMORPHIC_RING_EQ MONIC_ASSOCIATES_EQ MONIC_CMUL MONIC_DEG_0 MONIC_IMP_NONZERO MONIC_IN_TRIVIAL_RING MONIC_POLY_0 MONIC_POLY_1 MONIC_POLY_CONST MONIC_POLY_MUL MONIC_POLY_POW MONIC_POLY_PRODUCT MONIC_POLY_VAR MONIC_SUBRING_GENERATED MONOMIAL_DIVISORS_1 MONOMIAL_MUL_EQ_VAR MONOMIAL_UNIV_1 MONOMIAL_VAR_DIVIDES_MUL POLY_CONST_DIVIDES_CONST POLY_CONST_EQ_0 POLY_CONST_EQ_1 POLY_CONST_OF_NUM POLY_DEG_CMUL POLY_DEG_DERIV POLY_DEG_DERIV_LE POLY_DEG_DIVIDES_LE POLY_DEG_DIVIDES_LE_MONIC POLY_DEG_DIVIDES_LE_UNIVARIATE POLY_DEG_EQ_COEFF_EQ POLY_DEG_GE_COEFF POLY_DEG_GE_COEFF_EQ POLY_DEG_LE_COEFF_EQ POLY_DEG_MUL_MONIC POLY_DEG_MUL_UNIVARIATE POLY_DEG_RECIP POLY_DEG_RECIP_LE POLY_DEG_REM POLY_DEG_REM_ALT POLY_DERIV_0 POLY_DERIV_1 POLY_DERIV_ADD POLY_DERIV_CMUL POLY_DERIV_CONST POLY_DERIV_HOMOMORPHIC_IMAGE POLY_DERIV_IN_CARRIER POLY_DERIV_MUL POLY_DERIV_NEG POLY_DERIV_NONZERO_CHAR0 POLY_DERIV_POW POLY_DERIV_PRODUCT POLY_DERIV_SUB POLY_DERIV_SUBRING_GENERATED POLY_DERIV_SUM POLY_DERIV_VAR POLY_DERIV_VAR_POW POLY_DIV POLY_DIVIDES_RECIP POLY_DIVIDES_RECIP_EQ POLY_DIVIDES_RECIP_GALOIS POLY_DIVIDES_RECIP_RECIP POLY_DIVIDES_REM POLY_DIV_REM POLY_DIV_REM_SIMP POLY_EVALUATE_RING_SUM POLY_EVAL_RECIP POLY_EVAL_RING_SUM POLY_EXTEND_RING_SUM POLY_IN_POWSER_RING POLY_IRREDUCIBLE_IMP_SEPARABLE POLY_MUL_LEADING_COEFF POLY_MUL_RID POLY_NONCONSTANT_IRREDUCIBLE_IMP_SEPARABLE POLY_RECIP_0 POLY_RECIP_1 POLY_RECIP_CONST POLY_RECIP_EQ_0 POLY_RECIP_IN_CARRIER POLY_RECIP_MUL POLY_RECIP_MUL_GEN POLY_RECIP_NEG POLY_RECIP_RECIP POLY_RECIP_RECIP_EQ POLY_REM POLY_REM_UNIQUE POLY_ROOT_COUNT_IMP_SQUAREFREE POLY_SEPARABLE_EQ_SQUAREFREE POLY_SEPARABLE_IMP_SQUAREFREE POLY_SQUAREFREE_EXPLICIT_EQ POLY_SQUAREFREE_IMP_SEPARABLE POLY_SQUAREFREE_ROOT_COUNT POLY_SQUAREFREE_ROOT_COUNT_EQ POLY_SQUAREFREE_ROOT_COUNT_EXPLICIT POLY_SQUARE_DIVIDES_DERIV POLY_SQUARE_DIVIDES_DERIV_EQ POLY_VARPOW_RECIP_RECIP POWSER_CLAUSES POWSER_DERIV_IN_CARRIER REPEATED_ROOT_POLY_DERIV_ZERO RING_AUTOMORPHISM_I RING_AUTOMORPHISM_ID RING_COPRIME_DISTINCT_MONIC_IRREDUCIBLES RING_COPRIME_DIVISORS RING_COPRIME_HOMOMORPHIC_IMAGE RING_COPRIME_LPOW RING_COPRIME_PRODUCT RING_COPRIME_PRODUCT_DIVIDES RING_COPRIME_PRODUCT_DIVIDES_ALT RING_COPRIME_PRODUCT_EQ RING_COPRIME_RPOW RING_COPRIME_UNIT RING_DIVIDES_ALT RING_DIVIDES_MUL_EQ RING_DIVIDES_PRODUCTS RING_IRREDUCIBLES_COPRIME_OR_ASSOCIATES RING_IRREDUCIBLE_IMP_NONTRIVIAL_RING RING_IRREDUCIBLE_IMP_SQUAREFREE RING_IRREDUCIBLE_NEG RING_IRREDUCIBLE_POLY_CONST RING_IRREDUCIBLE_POLY_RECIP RING_IRREDUCIBLE_POLY_RECIP_EQ RING_IRREDUCIBLE_POLY_VAR RING_OF_NUM_POLY_RING RING_OF_NUM_POWSER_RING RING_POLYNOMIAL_DIV RING_POLYNOMIAL_POLY_DERIV RING_POLYNOMIAL_POWERSERIES_COEFF RING_POLYNOMIAL_RECIP RING_POLYNOMIAL_REM RING_POWERSERIES_POLY_DERIV RING_POWERSERIES_RECIP RING_PRIME_DIVIDES_POW RING_PRIME_IMP_NONTRIVIAL_RING RING_PRIME_IMP_SQUAREFREE RING_PRIME_MUL_DIVIDES RING_PRIME_MUL_DIVIDES_EQ RING_PRIME_NEG RING_PRIME_POLY_RECIP RING_PRIME_POLY_RECIP_EQ RING_PRIME_POLY_VAR RING_PRIME_PRODUCT_DIVIDES RING_SQUAREFREE_0 RING_SQUAREFREE_1 RING_SQUAREFREE_ALT RING_SQUAREFREE_ASSOCIATES RING_SQUAREFREE_COPRIME RING_SQUAREFREE_COPRIME_DIVISORS RING_SQUAREFREE_DECOMPOSITION RING_SQUAREFREE_DIVIDES RING_SQUAREFREE_DIVIDES_SQUARE RING_SQUAREFREE_DIVISOR RING_SQUAREFREE_DIVPOW RING_SQUAREFREE_DIVPOW_EQ RING_SQUAREFREE_GCD RING_SQUAREFREE_IMP_NONZERO RING_SQUAREFREE_IMP_NO_PRIME_SQUARE RING_SQUAREFREE_IN_CARRIER RING_SQUAREFREE_MUL_EQ RING_SQUAREFREE_MUL_IMP RING_SQUAREFREE_POW RING_SQUAREFREE_PRIME_DIVISOR_EQ RING_SQUAREFREE_PRIME_EQ RING_SQUAREFREE_PRODUCT RING_SUM_CONST RING_UNIT_IMP_SQUAREFREE RING_UNIT_POLY_RECIP RING_UNIT_POLY_RECIP_EQ RING_UNIT_POLY_RING_1 RING_UNIT_POLY_VAR SOLVABLE_GROUP_MONOMORPHIC_PREIMAGE TRIVIAL_RING_POLY_0 TRIVIAL_RING_POWSER_0 Changed theorems: ABELIAN_QUOTIENT_COMMUTATOR [reformulated] ALGEBRAICALLY_CLOSED_FIELD_EQ_SPLITS [strengthened, old = _ALT] COEFF_POLY_CONST_MUL [renamed to COEFF_POLY_LMUL] COEFF_POLY_MUL_CONST [renamed to COEFF_POLY_RMUL] POLY_MUL_VAR_COEFF_UNIVARIATE [removed, see COEFF_POLY_VAR_MUL] POLY_VAR_DIVIDES_UNIVARIATE [==> became <=>, lost hyps] RING_PRIME_POLY_CONST [==> became <=>, lost hyps] RING_PRIME_POLY_RING_MONO [lost integral_domain hyp] RING_PRIME_POLY_VAR_UNIVARIATE [==> became <=>] Incompatible changes to existing theorem statements: RING_PRIME_POLY_CONST (ringtheory.ml): strengthened from integral_domain r /\ ring_prime r p ==> ring_prime ... (poly_const ...) to the unconditional equivalence ring_prime (poly_ring r s) (poly_const r p) <=> ring_prime r p RING_PRIME_POLY_VAR_UNIVARIATE (ringtheory.ml): strengthened from integral_domain r ==> ring_prime (poly_ring r (:1)) (poly_var r one) to the equivalence ring_prime (poly_ring r (:1)) (poly_var r one) <=> integral_domain r RING_PRIME_POLY_RING_MONO (ringtheory.ml): lost integral_domain r hypothesis (primality in a sub-polynomial-ring now unconditionally lifts to the larger polynomial ring). POLY_VAR_DIVIDES_UNIVARIATE (ringtheory.ml): strengthened from integral_domain r /\ f IN carrier ==> (x divides f <=> f(0) = 0) to the unconditional equivalence ring_divides ... (poly_var r one) p <=> ring_polynomial r p /\ coeff 0 p = ring_0 r COEFF_POLY_CONST_MUL renamed to COEFF_POLY_LMUL (same statement). COEFF_POLY_MUL_CONST renamed to COEFF_POLY_RMUL (same statement). POLY_MUL_VAR_COEFF_UNIVARIATE removed, subsumed by COEFF_POLY_VAR_MUL. ALGEBRAICALLY_CLOSED_FIELD_EQ_SPLITS (fieldtheory.ml): hypothesis strengthened from ~(poly_deg k p = 0) to ~(p = poly_0 k). The old statement (with the degree condition) is preserved as ALGEBRAICALLY_CLOSED_FIELD_EQ_SPLITS_ALT. ABELIAN_QUOTIENT_COMMUTATOR (grouptheory.ml): universally quantified variables x, y moved from conclusion into main quantifier/conjunction: Old: !G n. ... ==> !x y. x IN ... ==> ... IN n New: !G n x y. ... /\ x IN ... ==> ... IN n Same logical content but different shape for SPECL/matching. ring_squarefree (100/transcendence.ml): definition changed from "a | b^2 ==> a | b" to "no non-unit has its square dividing a". Some downstream theorems in that file have gained hypotheses: ring_squarefree_if_prime now requires integral_domain r; ring_squarefree_if_product_coprime_primes(_indexed) now require UFD r.

…ctions; add printer_tests (jrh13#178) * printer.ml: factor pp_print_term special-form chain into separate functions; add printer_tests Decompose pp_print_term's try-with chain into separate functions organised as four phases: Phase A (shape): try_user_printers, print_numeral, print_string_or_list, top-level is_gabs Phase B (name): print_empty_set, print_universal_set, print_finite_set, print_set_comprehension, print_let_term, print_decimal, print_match, print_function, print_cond Phase C (parser): print_prefix_app, print_binder_app, print_infix_app Phase D (default): print_atom, print_generic_app Each function raises Failure on non-applicability; the high-level structure is still a flat try-with chain. Move unit_tests.ml to UnitTests/basic_tests.ml and add UnitTests/printer_tests.ml with 85 cases covering all four phases. Both basic_tests and printer_tests build .byte and .native targets. Native targets go through ./hol.sh inline-load / compile / link; bytecode targets call ocamlfind ocamlc directly because hol.sh has no byte mode. The default Makefile target builds all four binaries, clean removes them, and CI (test2 OCaml 4.14, test3 OCaml 5.4) runs all four. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * Try to fix CI --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

The send_and_wait() function sends user code followed by a sentinel Printf as the next toplevel phrase. When the user code raises an exception (e.g. a failed proof or missing file), the OCaml toplevel catches it, prints the error, and continues to the next phrase, so the sentinel always appears regardless of success or failure. This means make_checkpoint.py silently creates checkpoints of broken or partial states. Fix: wrap each expression in try/with that emits a unique error sentinel (HOL_MCP_LOAD_ERROR) on exception. wait_for_line() detects this sentinel and reports the exception with a clear error message before the script can proceed to checkpointing. Also reject expressions containing ';;' (multiple toplevel phrases) upfront, since try/with can only wrap a single expression. The error message guides the user to place composite inputs in a file and load with needs or loadt instead. This does not affect the MCP server's interactive use, where the LLM reads the full output and sees exception messages directly. It only affects make_checkpoint.py's batch usage, where intermediate output is discarded and only sentinel arrival is checked.

Bumps [python-multipart](https://github.com/Kludex/python-multipart) from 0.0.24 to 0.0.27. - [Release notes](https://github.com/Kludex/python-multipart/releases) - [Changelog](https://github.com/Kludex/python-multipart/blob/main/CHANGELOG.md) - [Commits](Kludex/python-multipart@0.0.24...0.0.27) --- updated-dependencies: - dependency-name: python-multipart dependency-version: 0.0.27 dependency-type: indirect ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

Under print_types_of_subterms := 2 (or := 1 with invented type variables), pp_print_term wraps a head h as "(s:type)". When s ends in a symbolic character, e.g. "&", the printed text "&:num->real" would lex back as a single Ident ("&:" is one token per lex), so the round trip parse_term o string_of_term failed. print_atom now inserts a single space before the ":" when the printed name ends in a symbolic character; for prefix/infix/binder names that are wrapped as "(op)" the trailing ")" suppresses this and printing is unchanged. The initial fix was authored by Balaji Rao in kings-crown/hol-light@281d03ec ("Made the printer insert a space between a symbolic printed head and the following type annotation colon"). This commit adopts that one-line check and surrounds it with regression tests. UnitTests/printer_tests.ml: add show_types regression cases for &n, -- &n, &1 + &2, plus a check_roundtrip helper that builds terms via mk_const/mk_comb/mk_numeral/mk_binop and verifies aconv equality of the reparse with print_types_of_subterms := 2 — independent of the parser surface syntax. Also broaden the associativity coverage that surrounds these cases: - num: add EXP, DIV, MOD left-associativity tests (correct the comment that called subtraction the only left-associative num arith op). - int: add div, rem, pow associativity tests and note that int has no MOD or EXP and that zpow is real-only. - real: add /, pow, zpow associativity tests with the same notes. 107/107 printer tests pass. Co-authored-by: Balaji Rao <brao@stevens.edu> Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Bumps [idna](https://github.com/kjd/idna) from 3.11 to 3.15. - [Release notes](https://github.com/kjd/idna/releases) - [Changelog](https://github.com/kjd/idna/blob/master/HISTORY.md) - [Commits](kjd/idna@v3.11...v3.15) --- updated-dependencies: - dependency-name: idna dependency-version: '3.15' dependency-type: indirect ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

complementing the existing Euclidean-specific "borel" (on real^N) already in topology.ml. In metric.ml, defined "borel_in top" inductively as the smallest family of subsets of the topspace containing the open sets and closed under countable union and under complement (relative to the topspace). Developed the basic sigma-algebra calculus and its behaviour under subtopologies, continuous maps and homeomorphisms: borel_in_RULES borel_in_INDUCT borel_in_CASES OPEN_IMP_BOREL_IN BOREL_IN_COMPLEMENT BOREL_IN_COMPLEMENT_EQ BOREL_IN_UNIONS BOREL_IN_SUBSET_TOPSPACE BOREL_IN_TOPSPACE BOREL_IN_EMPTY BOREL_IN_INTERS BOREL_IN_UNION BOREL_IN_INTER BOREL_IN_DIFF CLOSED_IMP_BOREL_IN FSIGMA_IMP_BOREL_IN GDELTA_IMP_BOREL_IN OPEN_IN_SUBTOPOLOGY_BOREL_IN CLOSED_IN_SUBTOPOLOGY_BOREL_IN BOREL_IN_SUBTOPOLOGY BOREL_FROM_SUBTOPOLOGY BOREL_IN_INTER_SUBTOPOLOGY BOREL_IN_SUBTOPOLOGY_EQ BOREL_IN_CONTINUOUS_MAP_PREIMAGE BOREL_IN_HOMEOMORPHIC_MAP_IMAGE BOREL_IN_HOMEOMORPHIC_MAPS_IMAGE_EQ BOREL_IN_HOMEOMORPHIC_MAP_IMAGE_EQ Also in metric.ml, defined "borel_measurable_map (top1,top2) f" as a function mapping top1 into top2 where the preimage of every "borel_in top2" set is "borel_in top1", with the expected closure properties, the most non-trivial being closure under pointwise sequential limits, assuming a metrizable codomain: borel_measurable_map BOREL_MEASURABLE_MAP_OPEN_IN BOREL_MEASURABLE_MAP_CLOSED_IN BOREL_MEASURABLE_MAP_IMAGE_SUBSET_TOPSPACE CONTINUOUS_IMP_BOREL_MEASURABLE_MAP BOREL_MEASURABLE_MAP_ID BOREL_MEASURABLE_MAP_CONST BOREL_MEASURABLE_MAP_EQ BOREL_MEASURABLE_MAP_COMPOSE BOREL_MEASURABLE_MAP_FROM_SUBTOPOLOGY BOREL_MEASURABLE_MAP_INTO_SUBTOPOLOGY BOREL_MEASURABLE_MAP_LIMIT In topology.ml, connected the general notions back to the existing Euclidean ones. BOREL_IN_EUCLIDEAN shows "borel_in euclidean = borel", so all the existing real^N results about "borel" transfer to the general theory as the Euclidean instance, and vice versa. The identification for the measurable maps is a little more delicate than for the sets, because the existing Euclidean Borel-measurability predicate "f borel_measurable_on s" (topology.ml) is defined quite differently, as a Baire function, i.e. inductively as the closure of the continuous functions under pointwise sequential limits. These are proved equivalent but only under the assumption that the domain is a Borel set, including the special case of the whole of real^N. BOREL_IN_EUCLIDEAN BOREL_MEASURABLE_MAP_EUCLIDEAN BOREL_MEASURABLE_MAP_EUCLIDEAN_SUBTOPOLOGY

are: (1) reworking measurability of random variables around the new general Borel sigma-algebra "borel_in" (Multivariate/metric.ml), in place of the previous hand-rolled half-line level-set lemmas; (2) building out the GENERAL conditional expectation "gen_cond_exp" into a usable calculus (linearity, monotone and dominated convergence, "taking out what is known", Cauchy-Schwarz, Jensen) and adding conditional variance; (3) adding the law/distribution (pushforward) of a random variable and the joint distribution function of a pair; (4) the Levy inversion theorem and characteristic-function uniqueness; (5) a new file ergodic.ml with the Birkhoff/maximal-ergodic material; and (6) a much fuller distributions.ml with densities, CDFs and characteristic functions for the standard distributions. As with everying in the Probability subdirectory, this was entirely generated (statements and proofs) by Claude Code, a mix of Opus 4.6 and 4.8. New definitions: cond_variance distribution ergodic exponential_cdf exponential_density exponential_distributed fejer_kernel_real geometric_distributed has_density has_pmf invariant_event joint_distribution_fn measure_preserving normal_cdf normal_density normal_distributed poisson_distributed real_halflines uniform_cdf uniform_density uniform_distributed and theorems: ABEL_SUMMATION_CONVERGENCE ABS_CONT ABS_LIM ABS_MUL_GE_SPLIT ABS_MUL_GE_SPLIT_BOUND ABS_MUL_LT_SQRT ADAPTIVE_SELECTOR_DEP ARCHIMEDEAN_INV_BOUND AS_IMP_IN_DIST AS_IMP_IN_PROB ATN_PI2_BOUND AVG_GT_IMP_MAXSUM_POS AVG_GT_IMP_SUM_POS AVG_LT_IMP_SUM_POS AVG_SHIFT_DIFF BERNOULLI_CHAR_FN_IM BERNOULLI_CHAR_FN_RE BINOMIAL_CHAR_FN_IM BINOMIAL_CHAR_FN_RE BIRKHOFF_ERGODIC BIRKHOFF_ERGODIC_BOUNDED BIRKHOFF_ERGODIC_BOUNDED_L1 BIRKHOFF_ERGODIC_L1 BIRKHOFF_ERGODIC_THEOREM BIRKHOFF_ERGODIC_THEOREM_BOUNDED BIRKHOFF_LIMIT_INVARIANT BIRKHOFF_OSCILLATION_CONTAINMENT BOREL_IN_EUCLIDEANREAL_EQ_SIGMA_GENERATED BOREL_IN_SIGMA_ALGEBRA BOUNDED_LIMSUP_LIMINF_CONVERGE CDF_MONO CDF_RIGHT_CONTINUOUS CHAR_FN_IM_BINOMIAL_RV CHAR_FN_IM_CONTINUOUS CHAR_FN_IM_EXPONENTIAL_DIST CHAR_FN_IM_GEOMETRIC_DIST CHAR_FN_IM_NORMAL_DIST CHAR_FN_IM_POISSON_DIST CHAR_FN_IM_UNIFORM_DIST CHAR_FN_RE_BINOMIAL_RV CHAR_FN_RE_CONTINUOUS CHAR_FN_RE_EXPONENTIAL_DIST CHAR_FN_RE_GEOMETRIC_DIST CHAR_FN_RE_NORMAL_DIST CHAR_FN_RE_POISSON_DIST CHAR_FN_RE_UNIFORM_DIST CHAR_FN_UNIQUENESS COND_EXP_INDICATOR_BOUNDED_AE COND_EXP_L2_CONTRACTION COND_EXP_TAKE_OUT CONTINUOUS_COMPOSE_SEQ CONTINUOUS_MAP_EUCLIDEANREAL CONVERGES_AS_FROM_RATE CONVERGES_IN_PROB_ABS CONVERGES_IN_PROB_ADD CONVERGES_IN_PROB_AE_SUBSEQUENCE CONVERGES_IN_PROB_BOUNDED_MUL CONVERGES_IN_PROB_CMUL CONVERGES_IN_PROB_CONST CONVERGES_IN_PROB_CONTINUOUS_COMPOSE CONVERGES_IN_PROB_DIFF_ZERO CONVERGES_IN_PROB_MAX CONVERGES_IN_PROB_MIN CONVERGES_IN_PROB_MUL CONVERGES_IN_PROB_NEG CONVERGES_IN_PROB_NULL_ADD CONVERGES_IN_PROB_NULL_MUL CONVERGES_IN_PROB_SUB CONVERGES_IN_PROB_SUBSEQUENCE CONVERGES_IN_PROB_SUBSEQUENCE_PRINCIPLE CONVERGES_IN_PROB_UNIQUE CONVEX_AFFINE_MINORANT_SUP CONVEX_CONT_AT COS_DIFF_HAS_REAL_INTEGRAL_HALFLINE COS_DIFF_HAS_REAL_INTEGRAL_HALFLINE_FULL COS_DIFF_HAS_REAL_INTEGRAL_HALFLINE_GEN COS_HAS_REAL_INTEGRAL DECOMPOSITION_UNBOUNDED_IFF DECR_INTEGRAL_TENDS_0 DECR_INTEGRAL_TENDS_0_AE DIRICHLET_INTEGRAL DIRICHLET_INTEGRAL_SCALED DIRICHLET_INTEGRAL_SCALED_NEG DIRICHLET_TAIL_BOUND DISCRIMINANT_NONNEG DISTRIBUTION_CDF DISTRIBUTION_COUNTABLY_ADDITIVE DISTRIBUTION_EMPTY DISTRIBUTION_FN_CONTINUOUS_PROB_ZERO DISTRIBUTION_IN_EVENTS DISTRIBUTION_LE_1 DISTRIBUTION_MONO DISTRIBUTION_POS DISTRIBUTION_UNIV DYADIC_APPROX_BOUND DYADIC_BOUND DYADIC_CONV DYADIC_LEVEL DYADIC_MEASURABLE DYADIC_SIMPLE ERGODIC_AVG_BOUNDED ERGODIC_AVG_DIFF_BOUND ERGODIC_AVG_EXPECTATION ERGODIC_AVG_INTEGRABLE ERGODIC_AVG_INTEGRABLE_POW2 ERGODIC_AVG_VARIANCE_BOUND ERGODIC_LIMINF_NULL ERGODIC_LIMINF_SHIFT ERGODIC_LIMSUP_NULL ERGODIC_LIMSUP_SHIFT ERGODIC_MAXSUM_GE_SUM ERGODIC_MAXSUM_INTEGRABLE ERGODIC_MAXSUM_KEY_INEQ ERGODIC_MAXSUM_MONO ERGODIC_MAXSUM_POS ERGODIC_MAXSUM_POS_EVENT ERGODIC_MAXSUM_RV ERGODIC_OSCILLATION_INVARIANT ERGODIC_OSCILLATION_MEASURABLE ERGODIC_OSCILLATION_NULL ERGODIC_SUM_EXPECTATION ERGODIC_SUM_INTEGRABLE ERGODIC_SUM_SHIFT ERGODIC_TRUNCATION_ABS_BOUND ERGODIC_TRUNCATION_INTEGRABLE ERGODIC_TRUNCATION_L1 ERGODIC_TRUNCATION_POINTWISE ERROR_INTEGRAL_BOUND EXPECTATION_ABS_FROM_SQUARE EXPECTATION_AE_ZERO EXPECTATION_COMP_PRESERVED EXPECTATION_EQ_TAIL_SUM EXPECTATION_EXPONENTIAL_DIST EXPECTATION_GEOMETRIC_DIST EXPECTATION_ITER_COMP_PRESERVED EXPECTATION_MONO_AE EXPECTATION_MUL_INDICATOR_CONULL EXPECTATION_NONNEG_ZERO_AE_ZERO EXPECTATION_NORMAL_DIST EXPECTATION_POISSON_DIST EXPECTATION_SQ_ORTHOGONAL EXPECTATION_UNIFORM_DIST EXPECTATION_ZERO_AE_BOUNDED_MEASURABLE EXPECTATION_ZERO_BOUNDED_MEASURABLE EXPECTATION_ZERO_HALVING EXPONENTIAL_CDF_LE_1 EXPONENTIAL_CDF_NONNEG EXPONENTIAL_CDF_ZERO EXPONENTIAL_CHAR_FN_IM EXPONENTIAL_CHAR_FN_RE EXPONENTIAL_DENSITY_INTEGRABLE_NONNEG EXPONENTIAL_DENSITY_INTEGRAL EXPONENTIAL_DENSITY_NONNEG EXPONENTIAL_DENSITY_POS EXPONENTIAL_DENSITY_ZERO EXPONENTIAL_HAS_REAL_DERIVATIVE EXPONENTIAL_HAS_REAL_DERIVATIVE_WITHIN EXPONENTIAL_INTEGRABLE_INTERVAL EXPONENTIAL_INTEGRAL_INTERVAL EXPONENTIAL_INTEGRAL_SEQ_TENDS_1 EXPONENTIAL_LIMIT_POSINFINITY EXPONENTIAL_LINEAR_DECAY_SEQ EXPONENTIAL_MEAN EXPONENTIAL_MEAN_ANTIDERIV EXPONENTIAL_MEAN_INTEGRAL EXPONENTIAL_MEAN_INTEGRAL_INTERVAL EXPONENTIAL_MEAN_SEQ_TENDS EXPONENTIAL_MEMORYLESS EXPONENTIAL_PRODUCT_DECAY_SEQ EXPONENTIAL_QUADRATIC_DECAY_SEQ EXPONENTIAL_REAL_CONTINUOUS EXPONENTIAL_SECOND_MOMENT EXPONENTIAL_SECOND_MOMENT_ANTIDERIV EXPONENTIAL_SECOND_MOMENT_INTEGRAL EXPONENTIAL_SECOND_MOMENT_INTEGRAL_INTERVAL EXPONENTIAL_SECOND_MOMENT_SEQ_TENDS EXPONENTIAL_VARIANCE_INTEGRAL EXP_AFFINE_DECOMP EXP_COS_ANTIDERIV EXP_COS_INTEGRAL_INTERVAL EXP_DECAY_INTEGRAL EXP_INTEGRAL_REP EXP_SIMPLE_MUL_DECOMP EXP_SIN_ANTIDERIV EXP_SIN_INTEGRAL_INTERVAL FEJER_KERNEL_REAL_COSINE FEJER_KERNEL_REAL_EQ_SINC_SQUARED FEJER_KERNEL_REAL_INTEGRAL FEJER_KERNEL_REAL_POS FEJER_KERNEL_REAL_TAIL_BOUND GAUSSIAN_FT_HALFLINE GEN_COND_EXP_ABS_BOUND GEN_COND_EXP_AFFINE GEN_COND_EXP_CAUCHY_SCHWARZ GEN_COND_EXP_DCT GEN_COND_EXP_DECR_TENDS_0 GEN_COND_EXP_JENSEN GEN_COND_EXP_JENSEN_EXP GEN_COND_EXP_L2_CONTRACTION GEN_COND_EXP_LINEAR3 GEN_COND_EXP_MCT GEN_COND_EXP_SEQ_MONO_AE GEN_COND_EXP_SUB GEN_COND_EXP_TAKE_OUT_AFFINE GEN_COND_EXP_TAKE_OUT_BOUNDED GEN_COND_EXP_TAKE_OUT_INDICATOR GEN_COND_EXP_TAKE_OUT_SIMPLE GEN_COND_EXP_TRIANGLE GEOMETRIC_CHAR_FN_IM GEOMETRIC_CHAR_FN_RE HALFLINES_SUBSET_UNIV HAS_DENSITY_INTEGRABLE HAS_DENSITY_INTEGRAL_ONE HAS_DENSITY_INTERVAL_PROB HAS_DENSITY_NONNEG HAS_DENSITY_RV HAS_PMF_NONNEG HAS_PMF_PROB HAS_PMF_RV HAS_PMF_SUMS_ONE HAS_REAL_INTEGRAL_AFFINITY_UNIV IDENTITY_HAS_REAL_INTEGRAL IID_SLLN_L1_VIA_BIRKHOFF IID_SLLN_VIA_BIRKHOFF INDEP_RV_JOINT_DISTRIBUTION INDICATOR_SUM_BOUNDED INDICATOR_SUM_COMPENSATOR_IDENTITY INDICATOR_SUM_COND_EXP_STEP INDICATOR_SUM_SUBMARTINGALE INF_PERTURB_BOUND INF_SUBSET_LE INNER_INTEGRAL_T INNER_INTEGRAL_U INTEGRABLE_ABS_INDICATOR INTEGRABLE_AFFINE_IND_MUL INTEGRABLE_BOUNDED_POW2 INTEGRABLE_COMP_MP INTEGRABLE_MUL_BOUNDED INTEGRABLE_PRODUCT_INDICATOR INTEGRABLE_TRUNCATION INTEGRAL_EXPECTATION_EXCHANGE INTEGRAL_GAP_TENDS_0 INTEGRAL_INV_ONE_PLUS_SQ INTEGRAL_SPLIT_NUMSEG INVARIANT_EVENTS_SUB_SIGMA_ALGEBRA INVERSION_FUBINI INVERSION_KERNEL_BOUNDED INVERSION_KERNEL_BOUNDED_NZ INVERSION_KERNEL_CONVERGES_AT_A INVERSION_KERNEL_CONVERGES_AT_B INVERSION_KERNEL_CONVERGES_INSIDE INVERSION_KERNEL_CONVERGES_OUTSIDE INVERSION_KERNEL_RV INVERSION_KERNEL_UNIFORM_BOUND INVERSION_SINC_EVEN INVERSION_TRIG_IDENTITY IN_SIGMA_GENERATED_GEN ITER_1 ITER_ADD ITER_IN_INVARIANT JOINT_DISTRIBUTION_LE_MARGINAL_X JOINT_DISTRIBUTION_SYM JOINT_RECTANGLE_IN_EVENTS KOLMOGOROV_SLLN' KRONECKER_RESCALED L2_IMP_IN_DIST LAPLACE_SIN LAW_OF_TOTAL_VARIANCE LEVY_CONDITIONAL_BOREL_CANTELLI LEVY_INVERSION LHS_INTEGRABLE LIFT_INTEGRAL_BRIDGE LIMSUP_EVENTS_IFF_SUM_UNBOUNDED LOTUS_BOUNDED_CONTINUOUS LOTUS_CONTINUOUS LOTUS_COS LOTUS_NONNEG_CONTINUOUS LOTUS_PMF_COS LOTUS_PMF_INTEGRABLE LOTUS_PMF_SIN LOTUS_SIN MARTINGALE_DIFF_ORTHOGONAL MAXIMAL_ERGODIC_INFINITE MAXIMAL_ERGODIC_LEMMA MEAN_ERGODIC_BOUNDED MEAN_ERGODIC_THEOREM MEASURABLE_WRT_INDICATOR MEASURABLE_WRT_INV_GE_ONE MEASURABLE_WRT_MAX_CONST MEASURABLE_WRT_MIN_CONST MEASURABLE_WRT_MUL MEASURABLE_WRT_MUL_INDICATOR MEASURABLE_WRT_POW2 MEASURABLE_WRT_REALLIM MEASURABLE_WRT_SUM MEASURE_AGREE_LAMBDA_SYSTEM MEASURE_PRESERVING_CARRIER MEASURE_PRESERVING_EVENTS MEASURE_PRESERVING_ITER MEASURE_PRESERVING_PROB MEASURE_UNIQUE_ON_PI_SYSTEM MEL_INVARIANT_SET MWRT_AFFINE NN_EXPECTATION_COMP_PRESERVED NN_EXPECTATION_COMP_PRESERVED_BOUNDED NORMAL_CDF_BOUNDS NORMAL_CDF_COMPLEMENT NORMAL_CDF_CONTINUOUS NORMAL_CDF_LIMIT_NEG NORMAL_CDF_LIMIT_POS NORMAL_CDF_MEAN NORMAL_CDF_MONO NORMAL_CDF_STANDARD NORMAL_CHAR_FN_IM NORMAL_CHAR_FN_RE NORMAL_DENSITY_INTEGRABLE NORMAL_DENSITY_INTEGRAL NORMAL_DENSITY_NONNEG NORMAL_DENSITY_POS NORMAL_DENSITY_STANDARD NORMAL_DENSITY_STANDARDIZE NORMAL_DENSITY_SYM NORMAL_MEAN NORMAL_MEAN_HELPER NORMAL_MEAN_INTEGRAL NORMAL_SHIFTED_COS_INTEGRAL NORMAL_SHIFTED_SIN_INTEGRAL NORMAL_VARIANCE NORMAL_VARIANCE_INTEGRAL NOT_CONVERGENT_OSCILLATION OFF_LIMSUP_CONVERGES ONE_MINUS_COS_HAS_REAL_INTEGRAL_HALFLINE ONE_MINUS_COS_HAS_REAL_INTEGRAL_UNIV ONE_MINUS_COS_SCALED_HAS_REAL_INTEGRAL_HALFLINE POISSON_CHAR_FN_IM POISSON_CHAR_FN_RE POISSON_MEAN_SERIES POISSON_PMF_RECURSION POISSON_SECOND_FACTORIAL_MOMENT POISSON_SECOND_MOMENT POISSON_VARIANCE_SERIES POW2_SHRINK_ZERO PROB_ABS_GE_TENDS_TO_ZERO PROB_STRICT_INEQ_LIMIT RADON_NIKODYM_UNIQUE RANDOM_VARIABLE_BOREL_MEASURABLE_COMPOSE RANDOM_VARIABLE_COMP_MP RANDOM_VARIABLE_CONTINUOUS_MAP_COMPOSE RANDOM_VARIABLE_DIV_POS RANDOM_VARIABLE_GT_SUFFICIENT RANDOM_VARIABLE_ITER_COMP_MP RANDOM_VARIABLE_LIMIT RANDOM_VARIABLE_PREIMAGE_BOREL_IN RANDOM_VARIABLE_REAL_LIMSUP_DOMINATED RANDOM_VARIABLE_SUP_SEQ_FN RANDOM_VARIABLE_TRUNCATION RATIONAL_DISCRIMINANT RATIONAL_DISCRIMINANT_DENSITY REALLIM_AT_POSINFINITY_FROM_SUBSEQUENCES REALLIM_AT_POSINFINITY_IMP_SEQUENTIALLY REAL_ABS_DIV_LE REAL_CONTINUOUS_ATREAL_SEQUENTIALLY REAL_CONVEX_SUPPORTING_LINE REAL_DIV_ABS_LE_1 REAL_EQ_EPSILON REAL_EQ_FROM_APPROX REAL_EXP_QUADRATIC_BOUND REAL_HALFLINE_LE_IN_SIGMA REAL_HALFLINE_LT_IN_SIGMA REAL_INTEGRAL_EVEN_SYMMETRIC REAL_INTERVAL_IN_SIGMA REAL_LE_EPSILON REAL_LIMINF_LE_LIMSUP_ABS REAL_LIMINF_LE_PERTURB REAL_LIMINF_LT_EXISTS_BOUNDED REAL_LIMINF_PERTURB_NULL REAL_LIMSUP_GT_EXISTS_BOUNDED REAL_LIMSUP_LE_PERTURB REAL_LIMSUP_LE_SUP' REAL_LIMSUP_NEG REAL_LIMSUP_PERTURB_NULL REAL_OPEN_COUNTABLE_UNION_REAL_INTERVAL REAL_OPEN_IN_SIGMA RESCALED_INDICATOR_CONVERGENCE RESCALED_INDICATOR_CONVERGENCE_MAX RESCALED_MAX_L2_BOUNDED RESCALED_MAX_MARTINGALE RESCALED_TRUNCATED_L2 REVERSE_FATOU_DOMINATED RHS_INTEGRABLE RIEMANN_SUM_CONVERGES RIGHT_CONTINUOUS_MONOTONE_AGREE RV_LEVEL_SET_EVENT RV_LIMIT_GT_EQ RV_PREIMAGE_GE RV_PREIMAGE_GT RV_PREIMAGE_LE RV_PREIMAGE_LT RV_PREIMAGE_LT_EQ_UNIONS RV_PREIMAGE_REAL_INTERVAL RV_PREIMAGE_REAL_OPEN RV_STRICT_INEQ_EVENT SHIFTED_FILTRATION SIGMA_ALGEBRA_INTERS_COUNTABLE SIGMA_ALGEBRA_SIGMA_GENERATED_HALFLINES SIGMA_ALGEBRA_SYM_DIFF SIMPLE_CHAR_FN_IM_CONTINUOUS SIMPLE_CHAR_FN_RE_CONTINUOUS SIMPLE_EXPECTATION_COMP_PRESERVED SIMPLE_EXPECTATION_TRAPEZOIDAL_FOURIER SIMPLE_RV_COMP_MP SIMPLE_RV_SUM_INDICATOR SIN2X_INV_X_SUBSTITUTION SINC_DECOMPOSITION SINC_EXP_DECAY_BOUND SINC_EXP_DECAY_INTEGRABLE SINC_EXP_EQ SINC_INTEGRAL_BOUND SINC_INTEGRAL_BOUND_ALL SINC_INTEGRAL_IDENTITY SINC_INTEGRAL_SPLIT SINC_INTEGRAL_UNIFORM_BOUND SINC_INV_INTEGRABLE SINC_LE_ONE SINC_MUL_INTEGRABLE SINC_SCALED_DIFF_INTEGRABLE SINC_SCALED_INTEGRABLE SINC_SCALED_INTEGRABLE_NZ SINC_SCALED_NEG_INTEGRABLE SINC_SQUARED_CONTINUOUS SINC_SQUARED_HAS_REAL_INTEGRAL_HALFLINE SINC_SQUARED_HAS_REAL_INTEGRAL_UNIV SINC_SQUARED_IDENTITY SINC_SQUARED_INTEGRABLE SINC_SQUARED_INTEGRAL SINC_SQUARED_INTEGRAL_BOUND SINC_SQUARED_LE_ONE SIN_EXP_2D_CONTINUOUS SIN_EXP_FUBINI SIN_HAS_REAL_INTEGRAL SIN_SQUARED_IBP SIN_SQUARED_INV_LE SIN_TAYLOR2_BOUND SMOOTHING_INTEGRAND_INTEGRABLE SMOOTHING_INTEGRAND_MEASURABLE SQUARE_HAS_REAL_INTEGRAL SQ_SUM_BOUND STD_NORMAL_CDF_COMPLEMENT STD_NORMAL_CDF_LIMIT_NEG STD_NORMAL_CDF_LIMIT_POS STD_NORMAL_CDF_SEQ_TENDS_1 STD_NORMAL_CDF_ZERO STD_NORMAL_INTEGRAL_INTERVAL_TENDS_1 SUMMATION_BY_PARTS SUM_INDICATOR_EQ_NAT SUM_SQUARE_CAUCHY_SCHWARZ SUM_TRIG_FACTOR SUPPORTING_SLOPE SUP_PERTURB_BOUND SUP_SEQ_VIA_INF SUP_SUBSET_GE SUP_TAIL_TENDS_0 TAIL_SUM_EQ_NN_EXPECTATION TELESCOPING_STEP TELESCOPING_SUM_BOUND TELESCOPING_SUM_BOUND_SIMPLE TELESCOPING_VARIANCE_BOUND TELESCOPING_VARIANCE_BOUND_SIMPLE THREE_SLOPES TO_POINTWISE TRAPEZOIDAL_ALG_IDENTITY TRAPEZOIDAL_FOURIER_IDENTITY TRIG_COS_DIFF_EXPAND TRUNCATED_DIFF_EXPECTATION_ZERO TRUNCATED_DIFF_SQ_BOUND TRUNCATION_ABS_DIFF TRUNCATION_L2_CONVERGENCE TRUNCATION_PRESERVES_LIMIT T_COS_HAS_REAL_INTEGRAL UI_MARTINGALE_CLOSURE UI_POINTWISE_L1_AE UNIFORM_CDF_BOUNDS UNIFORM_CDF_LEFT UNIFORM_CDF_MONO UNIFORM_CDF_RIGHT UNIFORM_CHAR_FN_IM UNIFORM_CHAR_FN_RE UNIFORM_DENSITY_INTEGRABLE UNIFORM_DENSITY_INTEGRAL UNIFORM_DENSITY_NONNEG UNIFORM_DENSITY_POS UNIFORM_DENSITY_VALUE UNIFORM_DENSITY_ZERO UNIFORM_MEAN UNIFORM_MEAN_INTEGRAL UNIFORM_SECOND_MOMENT UNIFORM_SECOND_MOMENT_INTEGRAL UNIFORM_VARIANCE_INTEGRAL UNIONS_SIGMA_GENERATED_HALFLINES VARIANCE_EXPONENTIAL_DIST VARIANCE_GEOMETRIC_DIST VARIANCE_NORMAL_DIST VARIANCE_POISSON_DIST VARIANCE_UNIFORM_DIST WIENER_MAXIMAL_INEQUALITY X2_CONVEX One existing theorem name THREE_SERIES_CONDITION1 now resolves to a strictly more general statement, by de-duplication. Eight theorems present previously are removed. Four are the bespoke half-line measurability lemmas, now subsumed by the single Borel-preimage characterization RANDOM_VARIABLE_PREIMAGE_BOREL_IN RANDOM_VARIABLE_GE RANDOM_VARIABLE_GT RANDOM_VARIABLE_STRICT_LT RANDOM_VARIABLE_OPEN_HALFLINE (The specific direction still needed in one place is retained/restated as RANDOM_VARIABLE_GT_SUFFICIENT.) The other four were ad-hoc analytic utilities, now removed as redundant with library facts or with local replacements: COS_TAYLOR_CONVERGES SIN_TAYLOR_CONVERGES POW_2_LE_SQRT REAL_CONTINUOUS_OPEN_PREIMAGE_UNIV Numerous existing proofs were also streamlined to go through RANDOM_VARIABLE_PREIMAGE_BOREL_IN and the general Borel machinery rather than re-deriving measurability of level sets by hand, but those leave the theorem statements untouched.

polynomial and power series rings (the latter via Cohen's prime-ideal criterion and Kaplansky's lemma), prime ideal correspondence under localization, and the preservation by localization of the Noetherian, Bezout, PID and von Neumann regular properties. Also added a ring definition of multiplicative order ("ring_order") with many elementary properties, and many other miscellaneous technical lemmas, as well as streamlining rabin_test.ml. New definition: ring_order and new theorems: BEZOUT_RING BEZOUT_RING_LOCALIZATION COEFF_POWSER_SUM FINITELY_GENERATED_IDEAL_LOCALIZATION FINITELY_GENERATED_IDEAL_SUBSET IDEAL_GENERATED_BY_HOMOMORPHIC_IMAGE IDEAL_GENERATED_EXPLICIT IDEAL_GENERATED_FINITARY IDEAL_GENERATED_FINITARY_ALT IDEAL_GENERATED_FINITE IDEAL_GENERATED_FINITE_IMAGE IDEAL_GENERATED_RING_LOCALIZATION IDEAL_GENERATED_SCALE IDEAL_GENERATED_SETADD_SUBSET IDEAL_LOCALIZATION_CONTRACTION KAPLANSKY_LEMMA LOCALEQUIV_MUL_LCANCEL LOCALEQUIV_MUL_RCANCEL MAXIMAL_NONFG_IMP_PRIME_IDEAL NOETHERIAN_LOCAL_RING_LOCALIZATION NOETHERIAN_POLY_RING NOETHERIAN_POLY_RING_1 NOETHERIAN_POWSER_RING NOETHERIAN_POWSER_RING_1 NOETHERIAN_RING_EQ_FG_PRIME_IDEALS NOETHERIAN_RING_LOCALIZATION PID_RING_LOCALIZATION POLY_ADD_RZERO POLY_DEG_EQ_FROM_LE POLY_DEG_LT_FROM_LE POLY_DEG_MUL_VAR POLY_DEG_MUL_VARPOW POLY_DEG_VARPOW_MUL POLY_DEG_VAR_MUL POLY_MUL_VAR POLY_RING_EPIMORPHISM_COEFF_0 POLY_RING_HOMOMORPHISM_COEFF_0 POLY_VAR_MUL POWSER_EVALUATE_AT_0 POWSER_EVAL_AT_0 POWSER_EXTEND_AT_0 POWSER_MUL_0 POWSER_MUL_MONOMIAL_1 POWSER_MUL_VAR POWSER_RING_EPIMORPHISM_COEFF_0 POWSER_RING_HOMOMORPHISM_COEFF_0 POWSER_VARPOW_MUL_EQ_0 POWSER_VAR_MUL POWSER_VAR_MUL_EQ_0 PRIME_IDEAL_LOCALIZATION PRIME_IDEAL_LOCALIZATION_CONTRACTION PRIME_IDEAL_LOCALIZATION_EXISTS PRINCIPAL_IDEAL_LOCALIZATION PROPER_IDEAL_LOCALIZATION RING_EPIMORPHISM_POWSER_EVALUATE_AT_0 RING_EPIMORPHISM_POWSER_EVAL_AT_0 RING_GEOM_SERIES RING_GEOM_SERIES_GEN RING_HOMOMORPHISM_IN_CARRIER RING_HOMOMORPHISM_POWSER_EVALUATE_AT_0 RING_HOMOMORPHISM_POWSER_EVAL_AT_0 RING_HOMOMORPHISM_POWSER_EXTEND_AT_0 RING_IDEAL RING_IDEAL_LOCALIZATION RING_IDEAL_SCALE RING_LOCALEQUIV_IN_LOCALIZED_IDEAL RING_LOCALEQUIV_REFL RING_LOCALEQUIV_SPLIT RING_LOCALEQUIV_SPLIT_EXPLICIT RING_LOCALIZATION_HOMOMORPHISM_UNIQUE RING_LOCALIZATION_PRIME_IDEAL_CORRESPONDENCE RING_LOCALIZATION_UNIQUE RING_MUL_LCANCEL RING_MUL_RCANCEL RING_NEG_SUB RING_ORDER_1 RING_ORDER_EQ_0 RING_ORDER_EQ_1 RING_ORDER_MUL RING_ORDER_MUL_DIVIDES RING_ORDER_MUL_DIVIDES_GEN RING_ORDER_MUL_DIVIDES_LCM RING_ORDER_POW RING_ORDER_POW_DIVIDES RING_ORDER_POW_GEN RING_ORDER_UNIQUE RING_ORDER_UNIQUE_PRIME RING_POW_COPRIME_EQ_1 RING_POW_EQ_1 RING_POW_GCD_EQ_1 RING_POW_MOD_ORDER RING_POW_MOD_ORDER_GEN RING_POW_RING_ORDER RING_PRODUCT_0 RING_PRODUCT_CASES RING_PRODUCT_NSUM RING_SCALE_SETMUL RING_SUM_DIFFS RING_SUM_DIFFS_ALT RING_UNIT_IDEMPOTENT_EQ_1 VNREGULAR_RING_LOCALIZATION The following are incompatible changes to existing theorems: COEFF_POLY_SUM -> COEFF_POWSER_SUM (COEFF_POLY_SUM is now re-used for the polynomial case) LOCALEQUIV_MUL_CANCEL -> LOCALEQUIV_MUL_RCANCEL (now with a dual LOCALEQUIV_MUL_LCANCEL) POLY_DEG_EQ_COEFF_FROM_LE -> POLY_DEG_EQ_FROM_LE (old name removed) POLY_EVALUATE_AT_0 (additional quantification)

* nets.ml: speed up discrimination-net lookup Replace the single (term_label * 'a net) list of edges in each net node with a record that splits children by label kind: a direct vnet field for the catchall Vnet edge plus persistent Map.Make balanced trees for Cnet/Lcnet (keyed by name+arity) and Lnet (keyed by arity). This is an algorithmic improvement to discrimination-net lookup: - Vnet branch is O(1) instead of an O(n) scan over edges. - Other lookups are O(log n) per bucket via balanced trees. - Comparators are monomorphic (String.compare / int compare) so the speedup is visible in bytecode as well as native code. Tips remain a sorted list because they are read in bulk (tryfind in REWRITES_CONV) and typically very short. Also annotate the head-classifier helpers (label_to_store / label_for_lookup) and net_update / follow with explicit term_label types so that grepping for term_label finds every place it flows. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * Fix holtest.mk's TacticTrace so that it sets up HOLLIGHT_DIR by itself --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

The mcp directory holds the local MCP-server dev tooling, not code that ships or affects the prover. Its transitive dependency graph churns often, and Dependabot was opening a steady stream of routine version-bump PRs for it (pyjwt, starlette, cryptography, python-multipart, pydantic-settings, ...), several of which edit uv.lock and so cannot be merged independently. Set open-pull-requests-limit: 0 on that ecosystem so Dependabot no longer raises *version* update PRs for /mcp. Security updates are governed separately and are unaffected: real advisories will still open PRs (as long as "Dependabot security updates" is enabled under Settings -> Code security), so we stay covered without chasing the bleeding edge. Also switch that block's ecosystem from "pip" to "uv" to match the actual lockfile (uv.lock), and drop the old allow: mcp/pytest filter, which did not restrict the transitive graph as intended and is moot once version PRs are suppressed. The github-actions updates are left flowing unchanged (rare and low-noise).

Bumps [actions/checkout](https://github.com/actions/checkout) from 6 to 7. - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md) - [Commits](actions/checkout@v6...v7) --- updated-dependencies: - dependency-name: actions/checkout dependency-version: '7' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

originating from work done in 2014 but both of them only now cleaned up and included in the HOL Light distribution using AI assistance (Claude and Codex, respectively). 1. Examples/apery.ml is a proof of Apery's theorem, the irrationality of zeta(3). This originates in 2014, when I was inspired by a presentation from Assia Mahboubi of a proof project in Coq, which was eventually completed and published as A. Mahboubi and T. Sibut-Pinote, "A Formal Proof of the Irrationality of zeta(3)" (2021). At that time the A and B recurrences had been proved in Coq following Bruno Salvy's computer algebra proof http://algo.inria.fr/libraries/autocomb/Apery2-html/apery.html but there was no machinery to provide the lcm(1..n) estimate needed for the full result. I decided to derive them from the HOL Light proof of the Prime Number Theorem (which is overkill). At that time I also formalized almost all other parts of the Apery proof including the A recurrence, but ground to a halt on the B recurrence which seemed to require much more work. I eventually revived this in 2026 and had Claude Opus 4.8 complete the B recurrence proof, following Salvy again. 2. WZ/* is a formal implementation of the Wilf-Zeilberger algorithm for hypergeometric summation, one which largely avoids akwardnesses over zero denominators and special cases by an interpretion using real gamma function limits. This was fully implemented back in 2014 and described in the paper: John Harrison "Formal Proofs of Hypergeometric Sums" Journal of Automated Reasoning 55 (2015) https://www.cl.cam.ac.uk/~jrh13/papers/wz.html The setup has belatedly been made available having been cleaned up and extended, mainly with a cleaner Maxima certificate-generation interface and a few more examples, by Codex using gpt-5.6-sol (xhigh). Among the automatic examples is the A recurrence that is proved more manually in the recently added Examples/apery.ml proof.

results formalized entirely autonomously by AI systems. Initially this contains two such formalizations: 1. three_squares.ml is a formalization by Claude Opus 4.8 of the classic Legendre three-squares theorem characterizing those integers representable as a sum of three integer squares, as well as the corollary that every integer is a sum of three triangular numbers. 2. sarkovskii.ml is a formalization by GPT-5.6-sol of Sarkovskii's theorem on periodic points of functions on real intervals. It is initially proved for functions real->real, then that core result is generalized using elementary topological machinery to arbitrary intervals. Also added a fix to handle degenerate SDPs with an empty constraint in REAL_SOS. This Claude-written change was based on a bug report and suggested fix from Daniel Nezamabadi. The issue is that real_positivnullstellensatz_general eliminates the linear monoid-matching equations in an essentially arbitrary order (via choose), then treats the remaining free variables as the SDP decision variables. Depending on that order, a free variable can turn out not to occur in any semidefinite block, so its constraint matrix mk_matrix is identically zero. CSDP rejects such a problem outright with "Constraint k is empty" and return code 206, rather than solving it. This is order-dependent: HOL Light's choose happens to pick an order that avoids it on the existing examples, but a differently-ordered dictionary implementation (e.g. Candle's) can hit it, e.g. on `a1 >= &0 /\ a2 >= &0 /\ (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + &2) /\ (a1 * b1 + a2 * b2 = &0) ==> a1 * a2 - b1 * b2 >= &0`;; The elimination is otherwise fine: the number of free variables (the affine solution dimension) is invariant across orders, so feasibility and the optimum are unchanged. Only the split of the free variables into "occurs in a block" vs "does not" varies, and an unlucky order leaves one decoupled. The fix is that before calling CSDP, we now drop any free variable whose constraint matrix is zero, solve the reduced SDP, and set the dropped variable to zero in the result. This is lossless: a variable absent from every block also has a zero objective coefficient (the objective is built from diagonal block entries), so it is genuinely unconstrained and irrelevant to the optimum. When no matrix is empty the reduced problem is identical to the original. This update also separately makes the "deepen" iterative deepending search function robust to genuinely malformed problems: CSDP return codes are now classified so that infeasibility (1,2) and numerical trouble (4-9) remain retryable Failures for the iterative deepening / tryfind search (some proofs, e.g. the Chebyshev and Zeng examples, legitimately rely on retrying past a numerical failure), while a structural rejection raises a new Csdp_error that deepen does not catch. Previously such a rejection was either swallowed as "no certificate at this degree", causing "deepen" to loop to ever higher degrees, or surfaced as a confusing missing-output-file error.

The carleson.ml formalization, produced by Claude Opus 4.8, proves Carleson's theorem that the Fourier series of a square-integrable periodic function converges almost everywhere. The development follows Fremlin's presentation of the Lacey-Thiele time-frequency proof in "Measure Theory" volume 2 (sec 286), including the Hardy-Littlewood maximal estimates, tile and tree arguments, and the Carleson maximal inequality. Its supporting Fourier-transform library develops Fourier analysis on the real line, including inversion, Schwartz functions, Plancherel's theorem and the L2 transform, again following Fremlin's, "Measure Theory" volume 2, the earlier sections 283-285. A few small additions and tweaks are made to existing files as part of this formalization (e.g. adding the complex inner product to lpspaces.ml). The fifteen_theorem.ml formalization, produced by GPT-5.6-sol (xhigh), proves the Conway-Schneeberger Fifteen Theorem: a positive-definite integral quadratic form is universal exactly when it represents every positive integer up to 15. The proof follows Bhargava's treatment using truants, escalator lattices, the nine ternary escalators and a finite rank-four analysis, together with classical ternary-form results and checked finite computations.

Merge upstream at 4334778. Adapt the discrimination-net optimization to Candle's verified Cake.Map while preserving polymorphic empty_net, retain Candle-specific CI workflow deletions, and adapt the upstream printer refactor to Candle's runtime.

jrh13 and others added 17 commits May 18, 2026 06:15

pa_j: accept camlp5 8.05 for OCaml 5.4 (jrh13#181)

6c23212

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Merge jrh13/hol-light master

c093a4c

Merge upstream at 4334778. Adapt the discrimination-net optimization to Candle's verified Cake.Map while preserving polymorphic empty_net, retain Candle-specific CI workflow deletions, and adapt the upstream printer refactor to Candle's runtime.

Navigation Menu

Uh oh!

Merge/jrh13 master 20260825 - #16

Merge/jrh13 master 20260825#16
tanyongkiam wants to merge 17 commits into
masterfrom
merge/jrh13-master-20260825

tanyongkiam commented Aug 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Uh oh!

Conversation

tanyongkiam commented Aug 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants