THE TACTIC BACKGROUND TABLE

every rate, against the band that says whether it means anything

Scoring a tactic by how often its proofs carry a removable dependence on choice looks like it should find the tactics at fault. The number it produces is mostly a property of the theorems the tactic gets used on.

The calibration is the whole table. A known-negative is a tactic that cannot introduce a classical instance at all — rfl, intro, exfalso — so whatever rate it shows is the background of its population. In Mathlib that background spans 5.8–28.2% across 30 controls; in Lean core 45.0–100.0%. The variation inside one library is as large as the variation between libraries, so no threshold survives normalisation.

Measured with gonzalgo · Lean 4.32.1 with Mathlib v4.32.1 · four libraries, two attribution rules, cells with at least 20 proofs

library	rule	tactic	role	proofs	classical	eligible	rate	vs band
Batteries	loose	grind	candidate	182	179	149	83.2%	above band
Batteries	loose	refine	known-negative	36	11	9	81.8%	inside band
Batteries	loose	cases	known-negative	111	39	30	76.9%	inside band
Batteries	loose	induction	known-negative	171	68	51	75.0%	inside band
Batteries	loose	apply	known-negative	94	54	38	70.4%	inside band
Batteries	loose	simp_all	candidate	32	10	7	70.0%	inside band
Batteries	loose	simp	candidate	616	222	151	68.0%	inside band
Batteries	loose	omega	candidate	24	19	12	63.2%	inside band
Batteries	loose	rw	known-negative	229	99	58	58.6%	inside band
Batteries	loose	exact	known-negative	133	54	30	55.6%	inside band
Batteries	loose	unfold	known-negative	49	18	9	50.0%	inside band
Batteries	loose	rfl	known-negative	145	39	19	48.7%	inside band
Batteries	loose	funext	known-negative	37	8	3	37.5%	inside band
Batteries	loose	ext	known-negative	30	17	6	35.3%	inside band
Batteries	loose	obtain	known-negative	22	10	3	30.0%	inside band
Batteries	loose	intro	known-negative	34	13	3	23.1%	inside band
Batteries	loose	simpa	not examined	40	23	5	21.7%	below band
Batteries	strict	grind	candidate	74	74	69	93.2%	above band
Batteries	strict	rw	known-negative	28	12	10	83.3%	inside band
Batteries	strict	simp	candidate	165	57	42	73.7%	below band
Init	loose	trivial	known-negative	23	2	2	100.0%	inside band
Init	loose	norm_cast	candidate	46	28	28	100.0%	inside band
Init	loose	subst	known-negative	516	175	164	93.7%	inside band
Init	loose	assumption	known-negative	150	58	52	89.7%	inside band
Init	loose	rcases	known-negative	923	338	300	88.8%	inside band
Init	loose	constructor	known-negative	367	153	128	83.7%	inside band
Init	loose	left	known-negative	38	12	10	83.3%	inside band
Init	loose	intro	known-negative	866	348	285	81.9%	inside band
Init	loose	right	known-negative	42	11	9	81.8%	inside band
Init	loose	decide	candidate	302	52	41	78.8%	inside band
Init	loose	ext	known-negative	377	141	107	75.9%	inside band
Init	loose	contradiction	known-negative	103	36	27	75.0%	inside band
Init	loose	rintro	known-negative	318	113	84	74.3%	inside band
Init	loose	grind	candidate	42	32	23	71.9%	inside band
Init	loose	cases	known-negative	1,721	220	158	71.8%	inside band
Init	loose	omega	candidate	1,144	654	462	70.6%	inside band
Init	loose	simp_all	candidate	838	202	141	69.8%	inside band
Init	loose	apply	known-negative	964	306	210	68.6%	inside band
Init	loose	induction	known-negative	966	133	91	68.4%	inside band
Init	loose	funext	known-negative	150	25	17	68.0%	inside band
Init	loose	rfl	known-negative	1,488	398	261	65.6%	inside band
Init	loose	rwa	known-negative	179	51	33	64.7%	inside band
Init	loose	exact	known-negative	1,285	468	289	61.8%	inside band
Init	loose	refine	known-negative	324	145	89	61.4%	inside band
Init	loose	rw	known-negative	3,339	1,222	735	60.1%	inside band
Init	loose	simpa	not examined	831	407	238	58.5%	inside band
Init	loose	obtain	known-negative	285	103	60	58.3%	inside band
Init	loose	show	known-negative	203	117	67	57.3%	inside band
Init	loose	unfold	known-negative	143	30	17	56.7%	inside band
Init	loose	simp	candidate	8,428	3,115	1,519	48.8%	inside band
Init	loose	change	known-negative	64	20	9	45.0%	inside band
Init	strict	omega	candidate	66	35	35	100.0%	above band
Init	strict	simp_all	candidate	39	8	8	100.0%	above band
Init	strict	exact	known-negative	22	6	5	83.3%	inside band
Init	strict	grind	candidate	20	20	16	80.0%	inside band
Init	strict	rw	known-negative	788	209	98	46.9%	inside band
Init	strict	simpa	not examined	160	70	28	40.0%	inside band
Init	strict	simp	candidate	2,677	1,212	315	26.0%	inside band
Init	strict	rfl	known-negative	23	1	0	0.0%	inside band
Mathlib	loose	grind	candidate	2,761	2,733	1,061	38.8%	above band
Mathlib	loose	decide	candidate	338	290	101	34.8%	above band
Mathlib	loose	exfalso	known-negative	74	71	20	28.2%	inside band
Mathlib	loose	contradiction	known-negative	172	148	38	25.7%	inside band
Mathlib	loose	tauto	candidate	360	324	81	25.0%	inside band
Mathlib	loose	cases	known-negative	2,446	1,664	411	24.7%	inside band
Mathlib	loose	right	known-negative	617	558	120	21.5%	inside band
Mathlib	loose	constructor	known-negative	2,633	2,291	493	21.5%	inside band
Mathlib	loose	induction	known-negative	3,418	2,561	519	20.3%	inside band
Mathlib	loose	use	known-negative	1,638	1,532	309	20.2%	inside band
Mathlib	loose	assumption	known-negative	301	240	48	20.0%	inside band
Mathlib	loose	rintro	known-negative	4,555	3,953	785	19.9%	inside band
Mathlib	loose	rcases	known-negative	4,512	4,126	793	19.2%	inside band
Mathlib	loose	obtain	known-negative	8,251	7,700	1,475	19.2%	inside band
Mathlib	loose	fin_cases	not examined	195	194	37	19.1%	inside band
Mathlib	loose	omega	candidate	67	53	10	18.9%	inside band
Mathlib	loose	injection	known-negative	51	28	5	17.9%	inside band
Mathlib	loose	exact	known-negative	25,561	23,555	4,085	17.3%	inside band
Mathlib	loose	rwa	known-negative	3,036	2,838	472	16.6%	inside band
Mathlib	loose	aesop	candidate	1,192	956	155	16.2%	inside band
Mathlib	loose	rfl	known-negative	12,979	11,098	1,793	16.2%	inside band
Mathlib	loose	refine	known-negative	13,164	12,517	2,011	16.1%	inside band
Mathlib	loose	trivial	known-negative	319	276	44	15.9%	inside band
Mathlib	loose	intro	known-negative	8,117	7,510	1,191	15.9%	inside band
Mathlib	loose	simpa	not examined	10,490	9,671	1,524	15.8%	inside band
Mathlib	loose	simp_all	candidate	1,204	1,041	163	15.7%	inside band
Mathlib	loose	left	known-negative	733	674	103	15.3%	inside band
Mathlib	loose	rw	known-negative	39,322	35,239	5,214	14.8%	inside band
Mathlib	loose	linear_combination	not examined	230	170	25	14.7%	inside band
Mathlib	loose	subst	known-negative	880	708	103	14.5%	inside band
Mathlib	loose	simp_rw	known-negative	5,720	5,278	759	14.4%	inside band
Mathlib	loose	unfold	known-negative	739	644	87	13.5%	inside band
Mathlib	loose	simp	candidate	38,681	32,913	4,408	13.4%	inside band
Mathlib	loose	apply	known-negative	9,577	8,835	1,165	13.2%	inside band
Mathlib	loose	show	known-negative	1,287	1,220	155	12.7%	inside band
Mathlib	loose	funext	known-negative	544	425	53	12.5%	inside band
Mathlib	loose	ext	known-negative	10,202	8,432	903	10.7%	inside band
Mathlib	loose	nlinarith	candidate	78	77	8	10.4%	inside band
Mathlib	loose	change	known-negative	1,334	1,246	120	9.6%	inside band
Mathlib	loose	cat_disch	not examined	709	638	60	9.4%	inside band
Mathlib	loose	delta	known-negative	189	164	14	8.5%	inside band
Mathlib	loose	gcongr	not examined	1,118	1,062	84	7.9%	inside band
Mathlib	loose	norm_cast	candidate	699	663	52	7.8%	inside band
Mathlib	loose	ring_nf	not examined	256	246	16	6.5%	inside band
Mathlib	loose	ring	candidate	985	915	55	6.0%	inside band
Mathlib	loose	exact_mod_cast	known-negative	175	172	10	5.8%	inside band
Mathlib	loose	norm_num	candidate	412	400	20	5.0%	below band
Mathlib	loose	field_simp	candidate	147	147	7	4.8%	below band
Mathlib	loose	linarith	candidate	558	556	21	3.8%	below band
Mathlib	loose	positivity	candidate	977	975	34	3.5%	below band
Mathlib	loose	push_cast	not examined	245	240	7	2.9%	below band
Mathlib	loose	bound	not examined	132	131	3	2.3%	below band
Mathlib	strict	induction	known-negative	29	24	21	87.5%	inside band
Mathlib	strict	grind	candidate	770	768	483	62.9%	inside band
Mathlib	strict	decide	candidate	77	58	33	56.9%	inside band
Mathlib	strict	norm_cast	candidate	25	25	9	36.0%	inside band
Mathlib	strict	rwa	known-negative	125	99	32	32.3%	inside band
Mathlib	strict	grw	not examined	41	22	6	27.3%	inside band
Mathlib	strict	simpa	not examined	1,935	1,686	383	22.7%	inside band
Mathlib	strict	simp_rw	known-negative	686	554	118	21.3%	inside band
Mathlib	strict	classical	not examined	109	108	21	19.4%	inside band
Mathlib	strict	rw	known-negative	5,634	4,454	815	18.3%	inside band
Mathlib	strict	simp	candidate	7,822	5,995	981	16.4%	inside band
Mathlib	strict	simp_all	candidate	44	31	5	16.1%	inside band
Mathlib	strict	aesop	candidate	180	99	11	11.1%	inside band
Mathlib	strict	fun_prop	not examined	20	19	2	10.5%	inside band
Mathlib	strict	exact	known-negative	40	37	3	8.1%	inside band
Mathlib	strict	convert!	not examined	34	26	2	7.7%	inside band
Mathlib	strict	cat_disch	not examined	83	78	2	2.6%	inside band
Mathlib	strict	apply	known-negative	95	81	1	1.2%	inside band
Mathlib	strict	linear_combination	not examined	23	21	0	0.0%	inside band
Mathlib	strict	rfl	known-negative	208	145	0	0.0%	inside band
Std	loose	simpa	not examined	734	667	512	76.8%	above band
Std	loose	grind	candidate	89	88	55	62.5%	above band
Std	loose	assumption	known-negative	95	78	47	60.3%	inside band
Std	loose	contradiction	known-negative	54	16	9	56.2%	inside band
Std	loose	simp	candidate	2,749	1,568	814	51.9%	inside band
Std	loose	rw	known-negative	1,747	1,075	533	49.6%	inside band
Std	loose	constructor	known-negative	89	55	27	49.1%	inside band
Std	loose	obtain	known-negative	47	14	6	42.9%	inside band
Std	loose	rintro	known-negative	42	19	8	42.1%	inside band
Std	loose	apply	known-negative	777	517	203	39.3%	inside band
Std	loose	cases	known-negative	263	106	41	38.7%	inside band
Std	loose	ext	known-negative	58	26	10	38.5%	inside band
Std	loose	intro	known-negative	482	283	103	36.4%	inside band
Std	loose	omega	candidate	130	78	28	35.9%	inside band
Std	loose	simp_all	candidate	172	60	21	35.0%	inside band
Std	loose	rcases	known-negative	109	80	27	33.8%	inside band
Std	loose	right	known-negative	40	23	7	30.4%	inside band
Std	loose	left	known-negative	41	24	7	29.2%	inside band
Std	loose	exact	known-negative	1,294	965	278	28.8%	inside band
Std	loose	rfl	known-negative	475	200	56	28.0%	inside band
Std	loose	decide	candidate	30	15	4	26.7%	inside band
Std	loose	induction	known-negative	412	99	23	23.2%	inside band
Std	loose	funext	known-negative	29	12	2	16.7%	inside band
Std	loose	rwa	known-negative	48	16	2	12.5%	inside band
Std	loose	unfold	known-negative	178	100	12	12.0%	inside band
Std	loose	refine	known-negative	247	200	23	11.5%	inside band
Std	loose	subst	known-negative	30	20	1	5.0%	inside band
Std	loose	trivial	known-negative	26	1	0	0.0%	inside band
Std	strict	apply	known-negative	25	20	18	90.0%	inside band
Std	strict	simp_to_raw	not examined	400	376	329	87.5%	inside band
Std	strict	simpa	not examined	561	546	446	81.7%	inside band
Std	strict	rw	known-negative	223	125	75	60.0%	inside band
Std	strict	simp	candidate	901	481	277	57.6%	inside band
Std	strict	simp_to_model	not examined	1,092	1,052	605	57.5%	inside band
Std	strict	simp_all	candidate	20	14	3	21.4%	inside band
Std	strict	rfl	known-negative	88	33	0	0.0%	inside band

rate is eligible over classical: of the proofs using this tactic that depend on Classical.choice, the share whose statement is choice-free, so the proof introduced the dependence. rule is how a proof is attributed — strict counts only proofs where the tactic is the sole tactic, loose counts every proof it appears in. role marks whether a tactic is a known-negative control, one of the 15 candidates the paper tests, or a tactic that was measured but never examined.

Get the data

tactic-bands.json · tactic-bands.csv · CC-BY-4.0 · version 2026-08-12

One of the gonzalgo indexes — standing measurements of what formal libraries rest on, remeasured as the libraries move.

Reproduce it

python analysis/final_table.py

Code and derived data: 10.5281/zenodo.21853489. The bands here are recomputed from the cells and checked against the ones the archive stores, so a row and its band cannot come from different runs.

What escapes, and why it does not help

7 of the examined candidates rise above their own library's band. Four of the seven are grind, which proves by refuting the negation and is therefore classical by construction rather than by defect. One is omega, whose avoidable dependence is real and independently established — and simp_all ties it at exactly 100.0% in the same library under the same rule, so even there the rate does not single it out.

norm_num carries a genuinely avoidable dependence, demonstrated by direct construction in the controlled experiment. It sits at 5.0% in Mathlib, below the known-negative floor, beneath rfl and exfalso and every other tactic that cannot introduce choice at all. The instrument ranks the one tactic with a proven defect beneath tactics incapable of the defect.

Widening the rule does not rescue it. Under strict, induction reaches 87.5% and widens Mathlib's band until nothing escapes at all. The instrument either fires on the wrong tactic or does not fire.

One cell the paper did not test

The published count of seven is over the 15 candidate tactics its script examines. Rates were computed for every tactic meeting the threshold, and one more escapes: simpa in Std under loose at 76.8% against a 60.3% band, over 734 proofs. It is neither a known-negative nor on the candidate list, so nothing in the pipeline looked at it.

It does not disturb the conclusion — an extra escape that nobody has a mechanism for is more evidence that the rate is not selecting on defectiveness — but it is in the data and belongs on the page rather than in a drawer.

Why the unit is wrong, not just the statistic

In the generated corpus interval_cases scores 100%. Its proofs close with <;> norm_num, and the score belongs to norm_num. A surface tactic inherits the axiom behaviour of whatever it delegates to, so attributing a proof to the tactic named in it is the wrong unit regardless of which statistic is computed over it. That is the finding this table exists to support.