Declaration index

All public declarations of the codebase (and the private ones cited by the map), with the paper statements that cite them and the matching Prove2Me node of the published (private) SurfaceBlowupV2 tree when one exists. The Prove2Me match is by declaration name (plus a curated alias table) and is informational.

Filter only declarations cited by the paper

declaration	kind	file	paper	Prove2Me
`actual_blowup_restriction_exists`	theorem	Blowup/PointTransport.lean		N0261
`actual_cech_differentials_commute_with_reduction`	theorem	Blowup/Charts.lean		N0126
`actual_cech_preserves_exceptional_lattices`	theorem	Blowup/Charts.lean		N0125
`actual_cech_reductions_surjective`	theorem	Blowup/Charts.lean	Lemma 4.1, Appendix A	N0127
`actual_finite_cech_coefficient_length`	theorem	Blowup/CechStability.lean	Lemma 4.2	N0117
`actual_finite_cech_coefficient_triangular`	theorem	Blowup/CechStability.lean	Lemma 4.2	N0118
`actual_negative_layer_coker_exact`	theorem	Blowup/TwoChartCurveData.lean		N0314
`actual_negative_twist_kernel_zero`	theorem	Blowup/NilpotentGluing.lean		N0235
`actual_twisted_coker_reduction_bijective`	theorem	Blowup/CechStability.lean	Lemma 4.1, Appendix A	N0116
`adamsCoef`	def	Reciprocity/Defs.lean	(6.4)	D022
`adamsCoef_adamsCoef`	theorem	Reciprocity/Quantum.lean		N0638
`adamsCoef_one`	theorem	Reciprocity/Quantum.lean		N0639
`adamsCoef_scalar`	theorem	Reciprocity/Quantum.lean		N0633
`adamsCoef_single`	theorem	Reciprocity/Quantum.lean		N0631
`adamsRat`	def	Reciprocity/Defs.lean		D022
`adamsRat_adamsRat`	theorem	Reciprocity/Defs.lean		N0509
`adamsRat_one`	theorem	Reciprocity/Defs.lean		N0510
`adamsRat_recipRat`	theorem	Reciprocity/Defs.lean		N0508
`adamsRat_X`	theorem	Reciprocity/Defs.lean		N0506
`adamsRat_zpow_X`	theorem	Reciprocity/Defs.lean		N0511
`adamsSer`	def	Reciprocity/Defs.lean		D022
`adamsSer_clusterSer_sub_one_scongr`	theorem	Reciprocity/Defs.lean		N0516
`adamsSer_logSer`	theorem	Reciprocity/Quantum.lean		N0655
`adamsSer_one`	theorem	Reciprocity/Defs.lean		N0514
`adamsSer_sub`	theorem	Reciprocity/Defs.lean		N0515
`adic_complete_iff_of_pow_le`	theorem	Unramified/Extension.lean		N0932
`adic_congruence_rules`	theorem	Measure/AdicTransport.lean		N0410
`adic_cylinders_intersection`	theorem	Measure/AdicTransport.lean		N0411
`adic_perturb_bijective`	theorem	Measure/AdicTransport.lean		N0414
`adic_perturb_congruence_iff`	theorem	Measure/AdicTransport.lean		N0412
`adic_perturb_measurable`	theorem	Measure/AdicTransport.lean		N0416
`adic_perturb_measure_preserving`	theorem	Measure/AdicTransport.lean		N0419
`adicCongr`	def	Measure/AdicCylinders.lean
`adicCylinders`	def	Measure/AdicCylinders.lean
`adicCylinderSpace`	def	Measure/AdicCylinders.lean
`adicPerturb`	def	Measure/AdicCylinders.lean
`AdicQuotient`	abbrev	Measure/AdicCylinders.lean
`adicReduce`	def	Measure/AdicCylinders.lean
`adjoinRoot_base_change`	theorem	Algebra/AlgebraType.lean		N0053
`affine_degenerate_null`	theorem	Etale/Main.lean		N1030
`affine_divisor_count`	theorem	Assembly/TypeEvents.lean		N0106
`affine_resultant_eq`	theorem	Measure/MemberCharts.lean		N0467
`affine_type_event_primitive_density`	theorem	Assembly/MonicCells.lean		N0091
`affine_type_event_unit_scaling`	theorem	Assembly/TypeEvents.lean		N0099
`AffineDirection`	abbrev	Blowup/Directions.lean
`AffineDivisor`	def	Assembly/NullBridges.lean
`affinePolynomial`	def	Basic.lean	Projective model	D008
`affinePolynomial_coeff_last`	theorem	Etale/Main.lean		N1026
`affinePolynomial_natDegree_of_last`	theorem	Etale/Main.lean		N1027
`affinePolynomial_snoc_one`	theorem	Etale/Main.lean		N1028
`affineTypeEvent`	def	Assembly/NullBridges.lean
`algebra_product_congruence`	theorem	Measure/AdicCylinders.lean		N0393
`algebra_type_algEquiv`	theorem	Algebra/AlgebraType.lean		N0062
`algebra_type_children_exists`	theorem	Measure/Haar.lean		N0434
`algebra_type_of_generic_fibre_equiv`	theorem	Algebra/AlgebraType.lean		N0063
`algebra_type_pi`	theorem	Algebra/AlgebraType.lean		N0064
`algebra_type_unique`	theorem	Algebra/FactorInvariant.lean		N0075
`algebra_type_unramified_descent`	theorem	Unramified/DescentTypes.lean	(6.4)	N0925
`algebraMap_chart_eq_chartBase`	theorem	Blowup/NilpotentGluing.lean		N0232
`algebraMap_injective_of_tower`	theorem	Algebra/AlgebraType.lean		N0049
`Allowed`	def	Basic.lean	Allowed residue ideals, cells, occupied points, (4.7)–(4.8)	D008
`allowed_pattern_of_divisor`	theorem	Recursion/Termination.lean		N0785
`allowed_pattern_of_divisor_unique`	theorem	Recursion/Members.lean		N0736
`allowedPatterns`	def	Basic.lean		D008
`AllPoints`	abbrev	Blowup/Charts.lean
`array_enumeration`	theorem	Assembly/TypeEvents.lean		N0100
`arrayLaw`	def	Assembly/NullBridges.lean
`availablePoints`	def	Basic.lean	(6.3)	D008
`axis_ideal_pow_mem_iff`	theorem	Surfaces/Lengths.lean
`axis_pow_mul_mem_span_cancel`	theorem	Surfaces/Lengths.lean		N0850
`axis_quotient_length_top`	theorem	Surfaces/Lengths.lean		N0845
`axis_span_isPrime`	theorem	Surfaces/Lengths.lean		N0849
`axisQuotientLength`	def	Surfaces/TruncatedSeries.lean
`axisQuotientLength_eq`	theorem	Surfaces/TruncatedSeries.lean		N0915
`axisQuotientLength_eq_iff`	theorem	Surfaces/TruncatedSeries.lean		N0916
`axisQuotientLength_eq_top`	theorem	Surfaces/TruncatedSeries.lean		N0914
`axisT`	def	Surfaces/Lengths.lean
`axisX`	def	Surfaces/Lengths.lean
`bad_exit_null`	theorem	Recursion/Events.lean	Proof of Theorem 6.2	N0726
`base_ideal_coordinates`	theorem	Unramified/Extension.lean		N0933
`base_ideal_maximal_local`	theorem	Unramified/FrobeniusDescent.lean		N0970
`base_ideal_pure`	theorem	Unramified/Extension.lean		N0934
`baseChange_bijective_of_finite_cokernel`	theorem	Recursion/Members.lean		N0737
`baseChangeUnit`	def	Surfaces/Lengths.lean
`BaseField`	abbrev	Basic.lean		D008
`baseIdeal`	def	Unramified/Extension.lean
`baseReduce`	abbrev	Unramified/Extension.lean
`beta_right_chartBase`	theorem	Blowup/NilpotentGluing.lean		N0233
`beta_right_chartBase_self`	theorem	Blowup/CurveSections.lean		N0160
`binary_nonEtale_null`	theorem	Etale/Main.lean	Remark 1.3	N1031
`binary_type_event_decomposition`	theorem	Assembly/TypeEvents.lean		N0101
`binaryTypeEvent`	def	Assembly/NullBridges.lean
`binomial_series_ode`	theorem	Reciprocity/Defs.lean		N0517
`block_conjugates_coprime`	theorem	Unramified/FrobeniusDescent.lean		N0980
`block_descent_bijection`	theorem	Unramified/FrobeniusDescent.lean	Lemma 7.1	N0982
`block_descent_congruence_iff`	theorem	Unramified/FrobeniusDescent.lean		N0983
`block_translation`	theorem	Unramified/PolynomialTypes.lean		N1013
`block_translation_type_iff`	theorem	Formula/TypeTransport.lean		N0379
`blockCell`	def	Unramified/Extension.lean
`blowup_chart_exceptional_point_polynomial`	theorem	Blowup/ExceptionalLayers.lean		N0195
`blowup_chart_relation`	theorem	Blowup/Charts.lean		N0120
`blowup_chart_ringHom_ext`	theorem	Blowup/Charts.lean		N0121
`blowup_chart_universal`	theorem	Blowup/Charts.lean		N0122
`blowup_exceptional_parameter_regular`	theorem	Blowup/Charts.lean		N0123
`blowup_overlap_isLocalization_right`	theorem	Blowup/PointTransport.lean		N0262
`BlowupChart`	abbrev	Blowup/Charts.lean
`blowupChart_concrete_isNoetherianRing`	theorem	Surfaces/Regularity.lean		N0898
`BlowupOverlap`	abbrev	Blowup/Charts.lean
`blowupRelation`	def	Blowup/Charts.lean
`BlowupRestriction`	structure	Blowup/Charts.lean
`boundary_chart_quotient_equiv`	theorem	Blowup/Charts.lean		N0124
`boundary_contact_length_ne_zero_iff`	theorem	Recursion/Members.lean		N0738
`boundary_contact_of_twisted_generator`	theorem	Blowup/DivisorPoints.lean		N0181
`boundaryDirections`	def	Blowup/Directions.lean
`card_mul_eq_zero_eq_card_quotient`	theorem	Surfaces/TruncatedSeries.lean		N0922
`card_pow_eq_sum_irreducible_degrees`	theorem	Surfaces/Lengths.lean	(6.2)
`card_truncIndex_axis_segment`	theorem	Surfaces/TruncatedSeries.lean		N0919
`cechInputLattice`	def	Blowup/Charts.lean
`cechInputReduction`	def	Blowup/Charts.lean
`cechInputThreadLinear`	def	Blowup/Charts.lean
`CechInputThreads`	def	Blowup/Charts.lean
`CechLevelInput`	abbrev	Blowup/Charts.lean
`CechLevelOutput`	abbrev	Blowup/Charts.lean
`cechOutputLattice`	def	Blowup/Charts.lean
`cechOutputReduction`	def	Blowup/Charts.lean
`cell_assignment_exists`	theorem	Recursion/OrderDefect.lean		N0763
`cell_child_bijOn`	theorem	Recursion/RootCellLaw.lean		N0776
`cell_child_data_exists`	theorem	Recursion/ChildMembers.lean		N0706
`cell_child_mem_stateSet`	theorem	Recursion/Members.lean		N0739
`cell_child_Phi_eq_map`	theorem	Recursion/OrderDefect.lean		N0771
`cell_datum_point_equiv`	theorem	Recursion/Members.lean		N0740
`cell_member_index_map`	theorem	Recursion/RootCellLaw.lean	Proposition 4.4	N0777
`cell_strict_transforms_agree_at_datum_points`	theorem	Blowup/StrictNormalizer.lean		N0300
`cell_transport_preimage`	theorem	Formula/TypeTransport.lean		N0384
`CellAssignment`	structure	Recursion/Members.lean
`CellAssignment.point`	def	Recursion/Members.lean
`CellChildData`	structure	Recursion/Members.lean
`CellChildData.alpha`	def	Recursion/Members.lean
`CellChildData.mc`	abbrev	Recursion/Members.lean
`CellChildData.point`	abbrev	Recursion/Members.lean
`CellChildData.Φ`	def	Recursion/Members.lean
`cellMeasure`	def	Unramified/Extension.lean
`cellMeasure_apply_of_measurableSet`	theorem	Formula/TypeTransport.lean		N0382
`cellMeasure_cell_inter`	theorem	Formula/TypeTransport.lean		N0383
`chart_cell_law_generic`	theorem	Recursion/Members.lean		N0741
`chart_child_completion_equiv`	theorem	Surfaces/ChartCompletions.lean		N0803
`chart_child_completion_map_exists`	theorem	Surfaces/Regularity.lean		N0900
`chart_child_completion_map_local`	theorem	Surfaces/Regularity.lean		N0901
`chart_image_measurable_chart_sigma`	theorem	Measure/AdicTransport.lean		N0413
`chart_layer_polynomial_coordinates`	theorem	Blowup/ExceptionalLayers.lean	(4.1)	N0201
`chart_measure_total_mass`	theorem	Measure/HenselProducts.lean		N0457
`chart_nonrational_point_span_eq_comap`	theorem	Surfaces/ChartCompletions.lean		N0807
`chart_point_eq_directionPoint`	theorem	Blowup/ExceptionalLayers.lean		N0196
`chart_point_isMaximal_of_residue_surjective`	theorem	Surfaces/Lengths.lean		N0855
`chartBase`	def	Blowup/Charts.lean
`chartBase_apply_eq_algebraMap`	theorem	Surfaces/ConcreteAtlas.lean		N0829
`chartBase_x_eq`	theorem	Blowup/H0Comparison.lean		N0207
`chartExceptional`	def	Blowup/Charts.lean
`chartMeasure`	def	Measure/AdicCylinders.lean
`ChartPair`	abbrev	Blowup/Charts.lean
`chartSlope`	def	Blowup/Charts.lean
`chartSubst`	def	Surfaces/Lengths.lean
`chartSubst_apply_generators`	theorem	Surfaces/Lengths.lean		N0851
`chartSubst_surfaceRelation_base_change_and_x_chart`	theorem	Surfaces/Lengths.lean		N0853
`chartSubst_surfaceRelation_origin_and_unit_point`	theorem	Surfaces/Lengths.lean		N0854
`child_coordinate_map_scaled`	theorem	Blowup/Charts.lean		N0130
`child_coordinate_preimage_measure`	theorem	Assembly/NullBridges.lean		N0094
`child_degree_le`	theorem	Formula/LawAlgebra.lean		N0327
`child_ideal_generator_transverse_finite`	theorem	Blowup/PointTransport.lean		N0274
`child_ideal_set_map_iff_stateSet`	theorem	Recursion/Termination.lean		N0793
`child_ideals_curve_datum`	theorem	Blowup/DivisorPoints.lean	Lemma 4.3	N0183
`child_order_equiv_linear`	theorem	Blowup/TwoChartCurveData.lean		N0309
`child_order_index_and_kernel`	theorem	Measure/MemberCharts.lean	Proposition 4.4	N0473
`child_series_eval_comp_chart_subst`	theorem	Surfaces/Regularity.lean		N0913
`child_volume_ratio`	theorem	Measure/AdicCylinders.lean	Proposition 6.1	N0394
`childCoordinateMap`	def	Blowup/Charts.lean
`childIdealSet`	def	Blowup/Charts.lean
`ChildMember`	structure	Recursion/Members.lean
`childOrder`	def	Blowup/Charts.lean
`childOrderMap`	def	Blowup/Charts.lean
`children`	def	Basic.lean	(4.7)–(4.8)	D008
`children_degree_identity`	theorem	Formula/LawAlgebra.lean	(6.5)	N0325
`children_residue_degree_pos`	theorem	Formula/LawAlgebra.lean		N0326
`children_valid`	theorem	Formula/LawAlgebra.lean		N0328
`chooseTwo`	def	Basic.lean		D008
`chooseTwo_add`	theorem	Reciprocity/Defs.lean		N0501
`ClosedDirection`	abbrev	Blowup/Directions.lean
`closure_finite_ascent`	theorem	Algebra/AlgebraType.lean		N0051
`closure_finite_ascent_root`	theorem	Algebra/AlgebraType.lean		N0056
`closure_finite_descent`	theorem	Algebra/AlgebraType.lean		N0050
`closure_finite_of_separable`	theorem	Algebra/AlgebraType.lean		N0057
`cluster_formula_regular`	theorem	Cluster/Main.lean	Theorem 1.1	N1022
`cluster_reciprocity`	theorem	Reciprocity/Main.lean	Proof of monic/cluster reciprocity, Theorem 9.3	N0550
`cluster_reciprocity_one`	theorem	Reciprocity/Patterns.lean	Proof of monic/cluster reciprocity	N0579
`cluster_reciprocity_step` private	theorem	Reciprocity/Main.lean	Proof of monic/cluster reciprocity
`clusterCell`	def	Cluster/Defs.lean
`clusterDensity`	def	Cluster/Defs.lean	Theorem 1.1
`clusterDensity_eq_etale`	theorem	Cluster/Main.lean	Theorem 1.1, Remark 1.3	N1021
`clusterExpr`	def	Cluster/Defs.lean	Theorem 1.1
`clusterSer`	def	Reciprocity/Defs.lean	(7.5)	D022
`clusterSer_eq_pPow`	theorem	Reciprocity/Plethysm.lean	(9.4)	N0619
`codilate`	def	Reciprocity/Defs.lean		D022
`codilate_dilate`	theorem	Reciprocity/Quantum.lean		N0678
`codilate_pPow`	theorem	Reciprocity/Quantum.lean		N0683
`Coef`	abbrev	Reciprocity/Defs.lean	Type variables Z_{e,f}	D022
`coeff_adamsSer`	theorem	Reciprocity/Defs.lean		N0512
`coeff_clusterSer_eq_coeff_qact`	theorem	Reciprocity/Main.lean	(S) = (7.11), (8.9), (9.4)	N0549
`coeff_codilate`	theorem	Reciprocity/Quantum.lean		N0676
`coeff_dilate`	theorem	Reciprocity/Quantum.lean		N0675
`coeff_euler_families_eq_patternSum`	theorem	Reciprocity/Plethysm.lean		N0626
`coeff_eulerSer`	theorem	Reciprocity/Patterns.lean	lem-7.2, (G) = (7.9)	N0575
`coeff_expSer_sub_of_scongr`	theorem	Reciprocity/Defs.lean		N0525
`coeff_formalPow`	theorem	Reciprocity/Plethysm.lean		N0588
`coeff_lawCoef`	theorem	Reciprocity/Plethysm.lean		N0627
`coeff_lawCoef_globalLaw_false`	theorem	Reciprocity/Patterns.lean		N0557
`coeff_lawCoef_globalLaw_true`	theorem	Reciprocity/Patterns.lean		N0558
`coeff_logSer_sub_of_scongr`	theorem	Reciprocity/Defs.lean		N0526
`coeff_one_clusterSer`	theorem	Reciprocity/Plethysm.lean		N0612
`coeff_one_dilate_recipSer_clusterSer`	theorem	Reciprocity/Plethysm.lean		N0616
`coeff_one_eulerSer_zero`	theorem	Reciprocity/Patterns.lean		N0578
`coeff_pPow_sub_of_scongr`	theorem	Reciprocity/Plethysm.lean	Pow_v and the first-difference rule	N0593
`coeff_qact_crossingQ_gaussPhi_eulerSer`	theorem	Reciprocity/Patterns.lean	(S) = (7.11)	N0580
`coeff_qact_gaussPhi`	theorem	Reciprocity/Defs.lean		N0534
`coeff_qact_gaussPhi_of_lt`	theorem	Reciprocity/Defs.lean	(8.10)	N0535
`coeff_recipCoef_lawCoef`	theorem	Reciprocity/Patterns.lean		N0560
`coeff_recipSer`	theorem	Reciprocity/Quantum.lean		N0672
`coeff_subst_eq_sum`	theorem	Reciprocity/Defs.lean		N0523
`coeff_substAlgHom_kill`	theorem	Surfaces/Lengths.lean		N0846
`coeff_succ_clusterSer`	theorem	Reciprocity/Plethysm.lean		N0611
`coeff_zero_clusterSer`	theorem	Reciprocity/Plethysm.lean		N0609
`coeff_zero_dilate_recipSer_clusterSer`	theorem	Reciprocity/Plethysm.lean		N0615
`coeff_zero_eulerSer`	theorem	Reciprocity/Plethysm.lean		N0614
`coefficient_cylinder_mass`	theorem	Measure/HenselProducts.lean		N0455
`coefficient_measure_pi_one`	theorem	Recursion/Members.lean		N0742
`coefficient_measure_probability`	theorem	Measure/HenselProducts.lean		N0456
`coefficient_space_strict_instances`	theorem	Blowup/Charts.lean		N0129
`coefficient_uniformizer_cylinder_mass`	theorem	Measure/HenselProducts.lean		N0458
`coefficientMeasure`	def	Basic.lean	Monic model	D008
`coefficientMeasure_zero_null`	theorem	Measure/MemberCharts.lean		N0469
`coeffVec`	def	Unramified/Extension.lean
`colored_subset_count`	theorem	Measure/AdicCylinders.lean		N0395
`common_vertical_exponent`	theorem	Measure/AdicCylinders.lean		N0396
`commonKernel`	def	Blowup/Charts.lean
`commonLevelIdeal`	def	Blowup/Charts.lean
`commonMultiplicity`	def	Blowup/Charts.lean
`compact_injective_image_measure`	theorem	Measure/StateVolumes.lean		N0498
`complete_domain_finite_quotient_local`	theorem	Unramified/Extension.lean
`completed_point_power_contraction`	theorem	Blowup/Charts.lean		N0131
`completed_point_transport_left`	theorem	Blowup/PointTransport.lean		N0268
`completed_point_transport_right`	theorem	Blowup/PointTransport.lean		N0269
`CompletedLocalAt`	abbrev	Blowup/Charts.lean
`completedPointMap`	def	Blowup/Charts.lean
`concrete_chart_point_span_form`	theorem	Surfaces/ConcretePoints.lean		N0832
`concrete_crossing_state_atlas_exists`	theorem	Surfaces/ConcreteAtlas.lean		N0827
`concrete_crossing_state_eq_union_cells`	theorem	Surfaces/Lengths.lean		N0861
`concrete_crossing_state_volume`	theorem	Surfaces/ConcreteStrictTransforms.lean	Proposition 3.3	N0840
`concrete_curve_order_index`	theorem	Measure/MemberCharts.lean	Proposition 4.4	N0474
`concrete_index_map_reindexed`	theorem	Recursion/Termination.lean		N0781
`concrete_infinity_boundary_contact`	theorem	Blowup/NilpotentGluing.lean	(4.6)	N0249
`concrete_infinity_point_completion`	theorem	Surfaces/ConcretePoints.lean		N0836
`concrete_infinity_strict_transform_multiplicity`	theorem	Blowup/PointTransport.lean		N0275
`concrete_infinity_strict_transform_transverse_finite`	theorem	Surfaces/ConcretePoints.lean		N0838
`concrete_left_point_completion_instances`	theorem	Surfaces/ConcretePoints.lean		N0834
`concrete_left_point_completion_is_surface`	theorem	Surfaces/ConcretePoints.lean		N0833
`concrete_left_point_exceptional_regular`	theorem	Surfaces/ConcretePoints.lean		N0835
`concrete_member_cell_measurable`	theorem	Recursion/Members.lean		N0745
`concrete_member_cells_cover`	theorem	Recursion/RootCellLaw.lean	Proposition 6.1	N0778
`concrete_member_cells_disjoint`	theorem	Recursion/ChildMembers.lean		N0708
`concrete_member_charts`	theorem	Recursion/Members.lean		N0744
`concrete_member_curve_order_free`	theorem	Recursion/Members.lean	Lemma 2.1	N0755
`concrete_member_data_exists`	theorem	Recursion/Members.lean		N0746
`concrete_member_division_chart_measure`	theorem	Recursion/Members.lean		N0753
`concrete_member_division_module_isAdicComplete`	theorem	Recursion/Members.lean		N0743
`concrete_member_divisor_count`	theorem	Recursion/OrderDefect.lean		N0764
`concrete_member_measure_finite_support`	theorem	Recursion/Members.lean		N0748
`concrete_member_mul_t_injective`	theorem	Recursion/Members.lean		N0749
`concrete_member_one_le_degree`	theorem	Recursion/Members.lean		N0750
`concrete_member_state_generator_contact_length`	theorem	Recursion/Members.lean		N0751
`concrete_member_state_generator_division`	theorem	Recursion/Members.lean		N0756
`concrete_member_state_generator_regular`	theorem	Recursion/Members.lean		N0752
`concrete_member_state_generator_transverse`	theorem	Recursion/Members.lean		N0754
`concrete_member_stateSet_measurable`	theorem	Recursion/Members.lean		N0747
`concrete_member_terminal_type`	theorem	Recursion/ChildMembers.lean	Lemma 2.2	N0713
`concrete_member_volume`	theorem	Recursion/Termination.lean		N0792
`concrete_residue_ideal_chart_exists`	theorem	Surfaces/ChartCompletions.lean		N0805
`concrete_single_state_atlas_exists`	theorem	Surfaces/ConcreteAtlas.lean		N0828
`concrete_single_state_eq_union_cells`	theorem	Surfaces/Lengths.lean		N0862
`concrete_single_state_volume`	theorem	Surfaces/ConcreteStrictTransforms.lean	Proposition 3.3	N0841
`concrete_strict_transform_generators`	theorem	Blowup/PointTransport.lean		N0276
`concrete_strict_transform_multiplicity`	theorem	Blowup/StrictNormalizer.lean	(4.6)	N0279
`concrete_strict_transform_residue_series`	theorem	Blowup/NilpotentGluing.lean		N0244
`concrete_strict_transform_transverse_finite`	theorem	Blowup/StrictNormalizer.lean		N0278
`concrete_strict_transforms_are_prescribed`	theorem	Surfaces/ConcreteStrictTransforms.lean		N0844
`concrete_surface_base_injective`	theorem	Surfaces/PowerSeries.lean		N0888
`concrete_surface_contact_eq_special_fiber_contact`	theorem	Surfaces/Lengths.lean		N0860
`concrete_surface_curve_basis`	theorem	Surfaces/Regularity.lean		N0911
`concrete_surface_curve_free_of_length`	theorem	Surfaces/Regularity.lean	Lemma 2.1	N0912
`concrete_surface_curve_isAdicComplete`	theorem	Surfaces/Completeness.lean		N0824
`concrete_surface_data_exists_unconditional`	theorem	Surfaces/Regularity.lean		N0910
`concrete_surface_equiv_curve_length_and_regular`	theorem	Surfaces/PowerSeries.lean		N0890
`concrete_surface_equiv_instances`	theorem	Surfaces/Regularity.lean		N0904
`concrete_surface_equiv_regular_pair`	theorem	Surfaces/Regularity.lean		N0906
`concrete_surface_isAdicComplete_maximalIdeal`	theorem	Surfaces/Completeness.lean		N0822
`concrete_surface_isAdicComplete_parameterIdeal`	theorem	Surfaces/Completeness.lean		N0821
`concrete_surface_isAdicComplete_span_pi`	theorem	Surfaces/Completeness.lean		N0823
`concrete_surface_isAdicComplete_span_pi_base`	theorem	Surfaces/Completeness.lean		N0825
`concrete_surface_isDomain`	theorem	Surfaces/Regularity.lean		N0903
`concrete_surface_isLocalRing`	theorem	Surfaces/PowerSeries.lean		N0897
`concrete_surface_isNoetherianRing`	theorem	Surfaces/Lengths.lean		N0856
`concrete_surface_isRegularLocalRing`	theorem	Surfaces/Regularity.lean		N0908
`concrete_surface_maximalIdeal_eq`	theorem	Surfaces/PowerSeries.lean		N0893
`concrete_surface_parameterIdeal_isMaximal`	theorem	Surfaces/PowerSeries.lean		N0892
`concrete_surface_pi_regular`	theorem	Surfaces/PowerSeries.lean		N0887
`concrete_surface_quotient_parameters_equiv`	theorem	Surfaces/PowerSeries.lean		N0891
`concrete_surface_quotient_T_equiv`	theorem	Surfaces/Completeness.lean		N0813
`concrete_surface_regular_pair_tx`	theorem	Surfaces/Regularity.lean		N0902
`concrete_surface_regular_pair_xt`	theorem	Surfaces/Regularity.lean		N0905
`concrete_surface_residue_regular_of_special_fiber`	theorem	Surfaces/Lengths.lean		N0857
`concrete_surface_residueField_equiv`	theorem	Surfaces/PowerSeries.lean		N0894
`concrete_surface_ringHom_ext_of_isNilpotent`	theorem	Surfaces/Completeness.lean		N0817
`concrete_surface_ringKrullDim_eq_two`	theorem	Surfaces/Regularity.lean		N0909
`concrete_surface_single_curve_free`	theorem	Blowup/StrictNormalizer.lean		N0289
`concrete_surface_span_T_isPrime`	theorem	Surfaces/Completeness.lean		N0814
`concrete_surface_spanFinrank_le_two`	theorem	Surfaces/PowerSeries.lean		N0895
`concrete_surface_special_fiber_equiv`	theorem	Surfaces/PowerSeries.lean	Lemma 2.1	N0889
`concrete_surface_special_fiber_equiv_parameters`	theorem	Surfaces/Lengths.lean		N0858
`concrete_surface_special_fiber_length_transport`	theorem	Blowup/Charts.lean		N0133
`concrete_surface_sub_constantCoeff_mem_parameterIdeal`	theorem	Surfaces/PowerSeries.lean		N0884
`concrete_surface_vertical`	theorem	Surfaces/Lengths.lean		N0859
`concrete_two_chart_glued_generators_exist`	theorem	Blowup/FixedTangentCellBijection.lean	Lemma 4.3	N0204
`concrete_type_add_of_index_map`	theorem	Recursion/Members.lean		N0757
`concrete_universe_exists`	theorem	Recursion/RootCellLaw.lean	Theorem 6.2	N0779
`concrete_zero_boundary_contact`	theorem	Blowup/NilpotentGluing.lean	(4.6)	N0250
`ConcreteMember`	structure	Recursion/Members.lean
`ConcreteMember.cellIndex`	abbrev	Recursion/Members.lean
`ConcreteMember.R`	abbrev	Recursion/Members.lean
`ConcreteMember.toMeasured`	def	Recursion/Members.lean
`ConcreteSurface`	abbrev	Surfaces/Lengths.lean	(2.1)
`congruence_bijection_measurable`	theorem	Measure/AdicCylinders.lean		N0397
`congruence_bijection_measure_preserving`	theorem	Measure/StateVolumes.lean		N0497
`conjugate_roots_distinct`	theorem	Unramified/PolynomialTypes.lean		N1014
`conjugateFactor`	def	Unramified/Extension.lean
`conjugateProduct`	def	Unramified/Extension.lean
`constantCoeff_adamsSer`	theorem	Reciprocity/Defs.lean		N0513
`constantCoeff_clusterSer`	theorem	Reciprocity/Plethysm.lean		N0610
`constantCoeff_eulerSer`	theorem	Reciprocity/Plethysm.lean		N0613
`constantCoeff_expSer`	theorem	Reciprocity/Defs.lean		N0518
`constantCoeff_logSer`	theorem	Reciprocity/Defs.lean		N0521
`constantCoeff_moebiusSum`	theorem	Reciprocity/Quantum.lean		N0663
`constantCoeff_plethSum`	theorem	Reciprocity/Quantum.lean		N0662
`constantCoeff_pPow`	theorem	Reciprocity/Plethysm.lean		N0590
`contact`	def	Surfaces/Lengths.lean
`contact_fiberT_eq_axisQuotientLength`	theorem	Surfaces/TruncatedSeries.lean		N0917
`contact_fiberX_eq_axisQuotientLength`	theorem	Surfaces/TruncatedSeries.lean		N0918
`continuousOn_of_congruence_compatible`	theorem	Formula/PatternCounts.lean		N0364
`contracted_ideal_map_localization_top`	theorem	Blowup/Charts.lean		N0132
`contractedLocalCurveIdeal`	def	Blowup/Charts.lean
`coordinate_constraint_count`	theorem	Measure/AdicCylinders.lean		N0398
`coordinate_coset_representatives_exist`	theorem	Blowup/Charts.lean		N0128
`coordinate_cylinder_clopen`	theorem	Formula/LawAlgebra.lean		N0352
`coordinate_hyperplane_null`	theorem	Formula/TypeTransport.lean	Discriminant locus is null	N0385
`coordinate_ideal_cell_bijection`	theorem	Measure/Atlas.lean	Proposition 3.2	N0423
`coordinate_ideal_in_residue_cell`	theorem	Measure/AdicCylinders.lean		N0399
`coordinate_ideal_injective`	theorem	Measure/Normalizer.lean		N0478
`coordinate_ideal_measurable_chart_sigma`	theorem	Surfaces/ConcreteStrictTransforms.lean		N0839
`coordinate_ideal_measurableEmbedding`	theorem	Recursion/Members.lean		N0758
`coordinate_module_pi_quotient_length`	theorem	Measure/AdicCylinders.lean		N0400
`coordinate_remainder_raises_order`	theorem	Measure/AdicCylinders.lean		N0401
`coordinate_scale_measure`	theorem	Blowup/StrictNormalizer.lean		N0284
`coordinate_transition_congruence`	theorem	Measure/Normalizer.lean	Lemma 3.1	N0476
`coordinateCoset`	def	Blowup/Charts.lean
`coordinateIdeal`	def	Measure/AdicCylinders.lean
`coordinateLift`	def	Measure/AdicCylinders.lean
`coordinateLift_smul_eq_mul`	theorem	Measure/AdicCylinders.lean		N0390
`coordinateLinear`	def	Blowup/Charts.lean
`coordinateRemainder`	def	Measure/AdicCylinders.lean
`coordinateScale`	def	Blowup/Charts.lean
`coprime_family_linear_injective`	theorem	Unramified/Extension.lean		N0935
`coprime_family_type_iff`	theorem	Formula/TypeTransport.lean		N0380
`coprime_of_coprime_residue_dvr`	theorem	Unramified/Extension.lean		N0936
`coprime_of_monic_reduction_one`	theorem	Formula/LawAlgebra.lean		N0353
`count_normalizedFactors_divisorAffinePolynomial`	theorem	Blowup/Directions.lean		N0180
`countSum`	def	Reciprocity/Defs.lean		D022
`crossing_residue_ideal_count`	theorem	Measure/Normalizer.lean	Proposition 3.3	N0479
`crossing_special_fiber_length`	theorem	Unramified/LocalDescent.lean	Lemma 2.1	N0991
`crossing_state_volume`	theorem	Measure/Normalizer.lean	Proposition 3.3	N0480
`crossingQ`	def	Reciprocity/Defs.lean	(7.5), (8.2)	D022
`crossingQ_eq_qmul_qplus_qdiag_qminus`	theorem	Reciprocity/Patterns.lean	(T) = (7.12), Lemma 8.2	N0576
`crossingQ_symm`	theorem	Reciprocity/Patterns.lean	(H) = (7.4)	N0574
`crossingQ_zero_zero`	theorem	Reciprocity/Patterns.lean		N0573
`crossingResidueIdeals`	def	Surfaces/Lengths.lean	Allowed residue ideals, cells, occupied points
`curve_datum_of_parent_function`	theorem	Surfaces/ConcreteAtlas.lean		N0831
`curve_datum_surj_and_inf_clauses`	theorem	Blowup/NilpotentGluing.lean		N0239
`curve_ideal_lattice_eq_kernels`	theorem	Blowup/CurveOrders.lean		N0134
`curve_ideal_lattice_le_sections`	theorem	Blowup/CurveOrders.lean		N0135
`curve_lattices_antitone`	theorem	Blowup/CurveOrders.lean		N0136
`curve_limit_equiv_product_threads`	theorem	Blowup/TwoChartCurveData.lean		N0308
`curve_limit_level_map_exists`	theorem	Blowup/CurveOrders.lean		N0137
`curve_limit_level_map_surjective`	theorem	Blowup/CurveSections.lean	Lemma 4.1	N0166
`curve_limit_range_of_stable_level`	theorem	Blowup/CechStability.lean		N0119
`curve_quotient_complete_equiv_threads`	theorem	Blowup/CurveOrders.lean		N0139
`curve_section_connecting_class_zero_iff`	theorem	Blowup/H0Comparison.lean		N0220
`curve_sections_connecting_map_exists`	theorem	Recursion/Members.lean		N0759
`curve_sections_cover_overlap`	theorem	Blowup/CurveSections.lean		N0167
`curve_sections_quot_equiv_product`	theorem	Blowup/TwoChartCurveData.lean		N0307
`curve_sections_quot_reduction_exists`	theorem	Blowup/CurveOrders.lean		N0138
`curveDataDegree`	def	Blowup/Charts.lean
`curveIdealLattice`	def	Blowup/Charts.lean
`curveLimitMk`	def	Blowup/Charts.lean
`curveNull`	def	Blowup/Charts.lean
`curveNullThreads`	def	Blowup/Charts.lean
`CurveOrderLimit`	def	Blowup/Charts.lean
`curveProduct`	abbrev	Blowup/Charts.lean
`curveProductReduction`	def	Blowup/Charts.lean
`curveProductThreads`	def	Blowup/Charts.lean
`curveSections`	def	Blowup/Charts.lean
`curveSectionsQuot`	def	Blowup/Charts.lean
`curveThreads`	def	Blowup/Charts.lean
`density_value_arith`	theorem	Formula/LawAlgebra.lean		N0331
`densityValue`	abbrev	Basic.lean		D008
`derivative_expSer`	theorem	Reciprocity/Defs.lean		N0519
`descend_block_mem_cell`	theorem	Unramified/FrobeniusDescent.lean		N0976
`descendBlock`	def	Unramified/Extension.lean
`descendCoeff`	def	Unramified/Extension.lean
`descended_block_type_iff`	theorem	Assembly/TypeEvents.lean		N0102
`descended_polynomial_type`	theorem	Unramified/DescentTypes.lean	Lemma 7.1	N0930
`digitIter`	def	Measure/AdicCylinders.lean
`dilate`	def	Reciprocity/Defs.lean		N0681
`dilate_codilate`	theorem	Reciprocity/Quantum.lean		N0679
`dilate_mul`	theorem	Reciprocity/Quantum.lean		N0677
`dilate_pPow`	theorem	Reciprocity/Quantum.lean	(7.6)	N0682
`dilate_recipSer_eulerSer_eq_pPow`	theorem	Reciprocity/Plethysm.lean		N0620
`dilate_recipSer_eulerSer_mul_scongr_one`	theorem	Reciprocity/Plethysm.lean		N0617
`direction_child_member_exists`	theorem	Recursion/ChildMembers.lean		N0705
`direction_point_maximal`	theorem	Blowup/ExceptionalLayers.lean		N0197
`direction_point_overlap_maximal`	theorem	Blowup/ExceptionalLayers.lean		N0198
`directionDegree`	def	Blowup/Directions.lean
`directionDegree_pos`	theorem	Formula/PatternCounts.lean
`directionPoint`	def	Blowup/Charts.lean
`directionPoint_isPrime`	instance	Blowup/Charts.lean
`directionPoint_properties`	theorem	Blowup/CurveOrders.lean		N0150
`discAffine`	def	Measure/MemberCharts.lean
`distinct_monic_irreducible_coprime`	theorem	Unramified/Extension.lean		N0937
`division_chart_preimage_image_measurable`	theorem	Measure/Atlas.lean		N0427
`division_chart_rank_eq_of_residue_ideal_eq`	theorem	Measure/AdicCylinders.lean		N0402
`division_chart_same_cell_recenter`	theorem	Measure/AdicCylinders.lean		N0404
`division_coordinate_module_isAdicComplete`	theorem	Surfaces/Completeness.lean		N0826
`division_data_same_cell_recenter`	theorem	Measure/AdicCylinders.lean		N0403
`division_data_vertical_perturbation`	theorem	Recursion/Termination.lean		N0782
`division_equiv_child_coordinates`	theorem	Blowup/CurveOrders.lean		N0158
`division_linear_equivalence`	theorem	Measure/AdicCylinders.lean	Lemma 3.1	N0405
`division_quotient_basis_equiv`	theorem	Recursion/Termination.lean		N0783
`divisionMap`	def	Measure/AdicCylinders.lean
`divisor_affine_polynomial_normalized_factors`	theorem	Recursion/Termination.lean		N0784
`divisor_array_exists_unique`	theorem	Assembly/TypeEvents.lean		N0103
`divisor_count_eval_of_point_count`	theorem	Assembly/TypeEvents.lean		N0105
`divisor_count_of_point_set`	theorem	Assembly/TypeEvents.lean		N0104
`divisor_count_safe`	theorem	Formula/LawAlgebra.lean		N0332
`divisor_form_cell_law`	theorem	Assembly/MonicCells.lean		N0088
`divisor_probability_pos`	theorem	Formula/StateCombinatorics.lean		N0373
`divisor_probability_safe`	theorem	Formula/LawAlgebra.lean		N0333
`divisor_vector_properties`	theorem	Assembly/TypeEvents.lean		N0107
`divisorAffinePolynomial`	def	Blowup/Directions.lean
`divisorBoundary`	def	Blowup/Charts.lean
`DivisorContactCondition`	abbrev	Recursion/Termination.lean
`divisorCount`	def	Basic.lean	(6.3)	D008
`divisorException`	def	Blowup/Charts.lean
`divisorFromSurface`	def	Recursion/Members.lean
`divisorLocalRing`	def	Blowup/Charts.lean
`divisorLocalRing_commRing`	instance	Blowup/Charts.lean
`divisorProbability`	def	Basic.lean	Proposition 6.1	D008
`divisorStrictTransform`	def	Blowup/Charts.lean
`divisorSupport`	def	Blowup/Directions.lean
`divisorSupport_finite`	instance	Blowup/Directions.lean
`divisorVector`	def	Assembly/NullBridges.lean
`dropCoord`	def	Unramified/Extension.lean
`dvr_algEquiv_ramification_inertia`	theorem	Unramified/FactorCells.lean		N0951
`dvr_extension_maximalIdeal_map_eq_pow`	theorem	Unramified/Extension.lean		N0938
`dvr_isAdicComplete_span_uniformizer`	theorem	Surfaces/Lengths.lean		N0863
`dvr_maximalIdeal_pow_injective`	theorem	Unramified/Extension.lean		N0939
`eminusOne`	def	Basic.lean		D008
`eq_of_mul_derivative_eq_mul`	theorem	Reciprocity/Plethysm.lean		N0584
`eq_zero_of_scalar_mul_eq_zero`	theorem	Reciprocity/Quantum.lean		N0692
`equiv_of_fiber_card_eq`	theorem	Recursion/Termination.lean		N0786
`etale_adjoinRoot_of_separable`	theorem	Etale/Algebra.lean		N1024
`etale_invariant_children`	theorem	Recursion/OrderDefect.lean		N0762
`etale_type_event_eq_term`	theorem	Recursion/Termination.lean		N0799
`etale_type_event_measurable`	theorem	Recursion/Events.lean		N0734
`etaleMonicDensity`	def	Etale/Defs.lean
`etaleMonicDensity_eq_algebraType`	theorem	Etale/Algebra.lean	Remark 1.3	N1025
`etaleProjectiveDensity`	def	Etale/Defs.lean
`eulerSer`	def	Reciprocity/Defs.lean	lem-7.2, (7.10)	D022
`eval_at_pow_card`	theorem	Unramified/Extension.lean		N0940
`eval₂_C_X_eq_algebraMap`	theorem	Reciprocity/Defs.lean
`exceptional_chart_is_affine_line`	theorem	Blowup/CurveOrders.lean		N0145
`exceptional_line_equiv_chart_exceptional`	theorem	Blowup/CurveOrders.lean		N0146
`exceptional_line_equiv_residue_field`	theorem	Blowup/CurveOrders.lean		N0147
`exceptional_overlap_is_laurent_line`	theorem	Blowup/CurveOrders.lean		N0148
`ExceptionalChartLevel`	abbrev	Blowup/Charts.lean
`exceptionalDegree`	def	Blowup/Directions.lean
`ExceptionalDivisor`	abbrev	Blowup/Directions.lean
`exceptionalLevelIdeal`	def	Blowup/Charts.lean
`ExceptionalOverlapLevel`	abbrev	Blowup/Charts.lean
`exists_pow_le_span_pair_transport`	theorem	Blowup/CurveSections.lean		N0171
`exists_separable_monic`	theorem	Measure/MemberCharts.lean		N0468
`exists_unique_selfPattern_single`	theorem	Reciprocity/Plethysm.lean	(6.6)	N0596
`exists_unramified_lift`	theorem	Formula/TypeTransport.lean		N0381
`exit_cell_coeff_nonneg`	theorem	Recursion/Events.lean		N0721
`exit_cell_type_mass`	theorem	Recursion/Events.lean		N0722
`exit_event_succ_mass`	theorem	Recursion/Events.lean	Proof of Theorem 6.2	N0724
`exit_event_zero_mass`	theorem	Recursion/Events.lean		N0727
`exitLaw`	def	Formula/StateCombinatorics.lean	(6.6)
`Expr`	inductive	Basic.lean	Type variables Z_{e,f}	D008
`Expr.allSafe`	def	Basic.lean		D008
`Expr.eval`	def	Basic.lean		D008
`Expr.fraction`	def	Basic.lean		D008
`Expr.fraction_snd_ne_zero`	theorem	Reciprocity/Plethysm.lean		N0600
`Expr.neg`	def	Basic.lean		D008
`Expr.pow`	def	Basic.lean		N0699
`Expr.prod`	def	Basic.lean		D008
`Expr.rational`	def	Basic.lean		D008
`Expr.rational_add`	theorem	Reciprocity/Plethysm.lean		N0601
`Expr.rational_const`	theorem	Reciprocity/Plethysm.lean		N0604
`Expr.rational_inv`	theorem	Reciprocity/Plethysm.lean		N0603
`Expr.rational_mul`	theorem	Reciprocity/Plethysm.lean		N0602
`Expr.rational_pow`	theorem	Reciprocity/Plethysm.lean		N0622
`Expr.rational_sub`	theorem	Reciprocity/Plethysm.lean		N0623
`Expr.rational_sum`	theorem	Reciprocity/Plethysm.lean		N0621
`Expr.rational_var`	theorem	Reciprocity/Plethysm.lean		N0605
`Expr.safe`	def	Basic.lean		D008
`Expr.sub`	def	Basic.lean		D008
`Expr.subst`	def	Basic.lean		D008
`Expr.sum`	def	Basic.lean		D008
`Expr.wf`	def	Reciprocity/Defs.lean		D022
`Expr.wf_pow`	theorem	Reciprocity/Plethysm.lean		N0598
`expression_fraction`	theorem	Formula/LawAlgebra.lean		N0321
`expression_pow_eval`	theorem	Formula/LawAlgebra.lean
`expression_pow_safe`	theorem	Formula/LawAlgebra.lean		N0318
`expression_prod_eval`	theorem	Formula/LawAlgebra.lean		N0319
`expression_regular`	theorem	Formula/LawAlgebra.lean		N0322
`expression_sum_eval`	theorem	Formula/LawAlgebra.lean
`expression_sum_safe`	theorem	Formula/LawAlgebra.lean		N0320
`expSer`	def	Reciprocity/Defs.lean		N0702
`expSer_add`	theorem	Reciprocity/Plethysm.lean		N0585
`expSer_logSer`	theorem	Reciprocity/Plethysm.lean	(7.6)	N0586
`expSer_zero`	theorem	Reciprocity/Defs.lean		N0520
`factor_cell_product_measure`	theorem	Unramified/PolynomialTypes.lean		N1010
`factor_cells_measure_preserving`	theorem	Unramified/HomogeneousCells.lean	Lemma 7.1	N0985
`factor_invariant_algEquiv`	theorem	Algebra/FactorInvariant.lean		N0071
`factor_invariant_unramified_scale`	theorem	Unramified/DescentTypes.lean		N0928
`factor_product_bijection`	theorem	Unramified/FactorCells.lean		N0954
`factor_product_congruence_iff`	theorem	Unramified/PolynomialTypes.lean		N1006
`factor_product_continuous`	theorem	Unramified/Extension.lean		N0941
`factorInvariant`	def	Basic.lean	Monic model	D008
`factorProduct`	def	Unramified/Extension.lean
`FactorType`	abbrev	Basic.lean	Type of degree n	D008
`falling`	def	Basic.lean	(6.3)	D008
`fiberT`	def	Surfaces/Lengths.lean
`fiberX`	def	Surfaces/Lengths.lean
`field_invariant_algEquiv`	theorem	Algebra/FactorInvariant.lean		N0070
`field_invariant_unramified_tower`	theorem	Unramified/DescentTypes.lean	(6.4)	N0924
`fieldInvariant`	def	Algebra/AlgebraType.lean	Reduced-algebra type convention
`finite_colength_completion_ideal_descent`	theorem	Unramified/LocalDescent.lean		N0994
`finite_completed_point_quotient_surjective`	theorem	Unramified/LocalDescent.lean		N0995
`finite_coordinate_adic_congruence`	theorem	Measure/AdicCylinders.lean		N0406
`finite_coordinate_borel_cylinders`	theorem	Measure/AdicCylinders.lean		N0408
`finite_coordinate_cylinder_basis`	theorem	Measure/AdicCylinders.lean		N0407
`finite_coordinate_linear_continuous`	theorem	Measure/AdicCylinders.lean		N0409
`finite_curve_support_kernel_saturated`	theorem	Blowup/CurveOrders.lean		N0157
`finite_field_card_primePower`	theorem	Formula/FiniteFieldCounts.lean		N0316
`finite_field_frobenius_fixed_points`	theorem	Unramified/Extension.lean		N0942
`finite_field_irreducible_count`	theorem	Formula/FiniteFieldCounts.lean	(6.2)
`finite_flat_local_ramification_degree`	theorem	Formula/LawAlgebra.lean		N0355
`finite_free_adic_complete`	theorem	Unramified/Extension.lean
`finite_free_residue_quotient`	theorem	Unramified/Extension.lean
`finite_length_module_card`	theorem	Formula/FiniteFieldCounts.lean		N0317
`finite_measures_from_cylinders`	theorem	Measure/AdicTransport.lean		N0417
`finite_module_length_card`	theorem	Measure/Normalizer.lean		N0481
`finite_quotient_event_mass`	theorem	Measure/AdicTransport.lean		N0420
`finite_quotient_fiber_mass`	theorem	Measure/AdicTransport.lean		N0418
`finite_support_completion_recovers`	theorem	Blowup/CurveOrders.lean		N0152
`finite_support_generators_compatible`	theorem	Blowup/CurveOrders.lean		N0155
`finite_support_kernel_localize`	theorem	Blowup/PointTransport.lean		N0253
`finite_support_level_generator_regular`	theorem	Blowup/NilpotentGluing.lean		N0242
`finite_support_level_kernels_principal`	theorem	Blowup/NilpotentGluing.lean		N0236
`finite_support_quotient_equiv`	theorem	Blowup/CurveOrders.lean	Lemma 4.3	N0156
`finite_support_quotient_surjective`	theorem	Blowup/CurveOrders.lean		N0154
`finite_support_quotient_surjective_of_isPrime`	theorem	Blowup/CurveOrders.lean		N0153
`finite_types_of_degree`	theorem	Formula/LawAlgebra.lean
`finiteCechDifferential`	def	Blowup/Charts.lean
`FiniteContact`	abbrev	Blowup/Charts.lean
`finiteLocalCurveIdeal`	def	Blowup/Charts.lean
`finiteSupportKernel`	def	Blowup/Charts.lean
`finiteSupportLevelKernel`	def	Blowup/Charts.lean
`finiteSupportQuotientMap`	def	Blowup/Charts.lean
`fixed_tangent_cell_chart_measurable`	theorem	Blowup/H0Comparison.lean		N0226
`fixed_tangent_cell_chart_partition`	theorem	Blowup/H0Comparison.lean		N0225
`fixed_tangent_cell_curve_datum`	theorem	Blowup/DivisorPoints.lean		N0185
`fixed_tangent_cell_generator_coefficients`	theorem	Blowup/PointTransport.lean		N0256
`fixedTangentCell`	def	Blowup/Charts.lean
`form_cell_monic_identification`	theorem	Unramified/HomogeneousCells.lean		N0986
`form_cell_product_measure`	theorem	Unramified/FactorCells.lean		N0957
`form_cells_measure_preserving`	theorem	Unramified/HomogeneousCells.lean	Lemma 7.1	N0988
`form_product_bijection`	theorem	Unramified/PolynomialTypes.lean		N1003
`form_product_congruence_reflects`	theorem	Unramified/PolynomialTypes.lean		N1002
`form_product_maps_to_and_preserves`	theorem	Unramified/Extension.lean		N0944
`form_product_measurable`	theorem	Unramified/HomogeneousCells.lean		N0987
`form_product_type_event_law`	theorem	Assembly/TypeEvents.lean		N0114
`formalPow`	def	Reciprocity/Defs.lean		D022
`formPoly`	def	Unramified/Extension.lean
`formPoly_add`	theorem	Unramified/Extension.lean		N0943
`formPoly_natDegree_le`	theorem	Assembly/TypeEvents.lean		N0108
`formProd`	def	Unramified/Extension.lean
`forms_linear_bijective`	theorem	Unramified/Extension.lean		N0946
`forms_linear_injective`	theorem	Unramified/Extension.lean		N0945
`FormsCoprime`	def	Unramified/Extension.lean
`FormulaRegular`	def	Basic.lean		D008
`frobenius_fixed_ring`	theorem	Unramified/FrobeniusDescent.lean	Standard facts	N0973
`frobenius_fraction_extension`	theorem	Unramified/DescentTypes.lean		N0926
`frobenius_pow_degree_eq_id`	theorem	Unramified/FrobeniusDescent.lean		N0974
`frobeniusIter`	def	Unramified/Extension.lean
`frobeniusRoot`	def	Unramified/Extension.lean
`full_rank_free_submodule_finite_length`	theorem	Recursion/Termination.lean		N0787
`fullCechDifferential`	def	Blowup/Charts.lean
`gaussPhi`	def	Reciprocity/Defs.lean	(7.10)	D022
`gaussPhi_dilate`	theorem	Reciprocity/Quantum.lean		N0685
`gaussPhi_dilate_recipSer_clusterSer` private	theorem	Reciprocity/Main.lean	(9.4)
`gaussPhi_qactRecip_gaussPhiInv`	theorem	Reciprocity/Quantum.lean	Lemma 9.1	N0687
`gaussPhi_sub`	theorem	Reciprocity/Quantum.lean		N0686
`gaussPhiInv`	def	Reciprocity/Defs.lean		D022
`generatorNormalForm`	def	Measure/AdicCylinders.lean
`generic_closure_free_of_type`	theorem	Recursion/Termination.lean		N0798
`GenericClosure`	def	Algebra/AlgebraType.lean
`genericClosureVal`	def	Algebra/AlgebraType.lean
`geometric_exit_sum`	theorem	Formula/LawAlgebra.lean	Proof of Theorem 6.2	N0356
`global_coefficients_safe`	theorem	Formula/StateCombinatorics.lean		N0376
`global_formula_regular`	theorem	Formula/StateCombinatorics.lean	Theorem 1.1, Theorem 6.2	N0377
`global_function_has_tangent_divisor`	theorem	Blowup/DivisorPoints.lean		N0190
`global_function_mem_cell`	theorem	Blowup/DivisorPoints.lean		N0191
`global_function_of_two_chart_curve_data`	theorem	Recursion/Termination.lean		N0788
`global_function_strict_transform_at_right_point`	theorem	Blowup/TwoChartCurveData.lean		N0311
`global_law_safe`	theorem	Formula/StateCombinatorics.lean		N0375
`global_rational_eval`	theorem	Formula/RationalEval.lean		N0365
`globalLaw`	def	Basic.lean	(1.5), (7.3)	D008
`glued_function_exists_unique`	theorem	Blowup/H0Comparison.lean	Lemma 4.2	N0222
`glued_function_initial_form`	theorem	Blowup/H0Comparison.lean		N0217
`glued_function_left_chart`	theorem	Blowup/CurveOrders.lean		N0140
`glued_function_order`	theorem	Blowup/H0Comparison.lean		N0216
`glued_function_pair_closed`	theorem	Blowup/CurveOrders.lean		N0142
`glued_function_pair_compatible`	theorem	Blowup/CurveOrders.lean		N0143
`glued_function_right_chart`	theorem	Blowup/CurveOrders.lean		N0141
`glued_generators_exist`	theorem	Blowup/CurveSections.lean	Lemma 4.3	N0168
`glued_generators_level_one`	theorem	Blowup/CurveOrders.lean		N0144
`glued_generators_of_two_chart_curve_data`	theorem	Blowup/TwoChartCurveData.lean		N0310
`glued_level_one_normalization`	theorem	Blowup/ExceptionalLayers.lean		N0192
`gluedFunctionPair`	def	Blowup/Charts.lean
`GluedGenerators`	structure	Blowup/Charts.lean
`has_multiplicity_initial_form`	theorem	Recursion/Termination.lean		N0789
`has_tangent_divisor_multiplicity`	theorem	Blowup/H0Comparison.lean		N0209
`HasAlgebraType`	def	Algebra/AlgebraType.lean	Reduced-algebra type convention
`HasArray`	def	Assembly/NullBridges.lean
`HasBinaryType`	def	Basic.lean	Projective model	D008
`HasBinaryTypeF`	def	Basic.lean		D008
`HasHomogeneousDivisor`	def	Blowup/Directions.lean
`HasMultiplicity`	def	Surfaces/Lengths.lean
`HasPattern`	def	Blowup/Directions.lean
`HasPolynomialType`	def	Basic.lean	Monic model	D008
`HasPolynomialTypeF`	def	Basic.lean	Reduced-algebra type convention, Remark 6.3	D008
`HasPolynomialTypeF.to_original`	theorem	Algebra/AlgebraType.lean		N0058
`hasPolynomialTypeF_iff_of_separable`	theorem	Algebra/AlgebraType.lean		N0059
`HasTangentDivisor`	def	Blowup/Charts.lean	Allowed residue ideals, cells, occupied points, (4.6)
`hensel_factor_unique_of_dvd`	theorem	Unramified/Extension.lean		N0947
`hensel_family_exists`	theorem	Measure/HenselProducts.lean		N0436
`hensel_family_unique`	theorem	Unramified/Extension.lean		N0948
`hensel_family_unique_mod_pow`	theorem	Unramified/PolynomialTypes.lean		N1004
`hensel_pair_exists`	theorem	Measure/HenselProducts.lean		N0435
`hensel_pair_unique`	theorem	Measure/HenselProducts.lean		N0438
`homogeneous_divisor_boundary_multiplicities`	theorem	Recursion/Termination.lean	(4.6)	N0791
`homogeneous_divisor_of_polynomial`	theorem	Recursion/Termination.lean		N0790
`homogeneous_form_not_mem_pow_succ`	theorem	Blowup/CurveOrders.lean		N0151
`ideal_chart_pushforward_independent`	theorem	Measure/Atlas.lean	Proposition 3.2	N0426
`ideal_chart_transition_haar`	theorem	Measure/Atlas.lean	Proposition 3.2	N0425
`ideal_closed_noetherian_local`	theorem	Surfaces/Lengths.lean		N0865
`ideal_contact_generator`	theorem	Blowup/CurveOrders.lean		N0159
`IdealAtlas`	structure	Measure/AdicCylinders.lean
`IdealChart`	structure	Measure/AdicCylinders.lean	Proposition 3.2
`IdealChart.isDivisionChart`	theorem	Measure/AdicCylinders.lean		N0391
`idealChartSigma`	def	Measure/AdicCylinders.lean	Proposition 3.2
`idealContact`	def	Surfaces/Lengths.lean
`idealTransition`	def	Measure/AdicCylinders.lean
`iInf_sup_pow_eq_of_isLocalRing`	theorem	Surfaces/Lengths.lean		N0864
`image_measurable_of_continuousOn_injOn_compact`	theorem	Formula/LawAlgebra.lean		N0357
`inertiaDeg_unramified_tower`	theorem	Unramified/FrobeniusDescent.lean		N0965
`infinity_block_event_law`	theorem	Assembly/MonicCells.lean		N0087
`infinity_point_child_member`	theorem	Recursion/Termination.lean		N0794
`infinity_point_maximal`	theorem	Blowup/ExceptionalLayers.lean		N0199
`infinityBlockEvent`	def	Assembly/NullBridges.lean
`infinityDirection`	def	Blowup/Directions.lean
`infinityPoint`	def	Blowup/Charts.lean
`initial_form_has_tangent_divisor`	theorem	Recursion/Termination.lean	(4.6)	N0795
`initial_form_lift_independent`	theorem	Blowup/H0Comparison.lean		N0210
`insertOne`	def	Unramified/Extension.lean
`instance@L213`	instance	Blowup/Charts.lean
`instance@L217`	instance	Blowup/Charts.lean
`instance@L588`	instance	Blowup/Charts.lean
`instance@L591`	instance	Blowup/Charts.lean
`instance@L594`	instance	Blowup/Charts.lean
`instance@L597`	instance	Blowup/Charts.lean
`instance@L686`	instance	Blowup/Charts.lean
`instance@L692`	instance	Blowup/Charts.lean
`instance@L83`	instance	Algebra/AlgebraType.lean
`instance@L87`	instance	Algebra/AlgebraType.lean
`integral_closure_algEquiv`	theorem	Algebra/AlgebraType.lean		N0065
`integral_closure_finite_free`	theorem	Algebra/AlgebraType.lean	Standard facts
`integral_closure_invariants_degree`	theorem	Algebra/AlgebraType.lean		N0066
`integral_closure_is_dedekind`	theorem	Algebra/AlgebraType.lean
`integral_closure_is_dvr`	theorem	Measure/PrimitiveLocus.lean	Standard facts
`integral_closure_is_local`	theorem	Measure/PrimitiveLocus.lean
`integral_closure_not_field`	theorem	Algebra/AlgebraType.lean
`integral_closure_own_adic_complete`	theorem	Measure/PrimitiveLocus.lean		N0490
`integral_local_extension_unique_prime`	theorem	Formula/LawAlgebra.lean		N0354
`integralClosureTowerEquiv`	def	Algebra/AlgebraType.lean
`invariant_orbit_factors`	theorem	Unramified/Extension.lean		N0949
`invSelf_pow_eq_selfZPow`	theorem	Blowup/NilpotentGluing.lean		N0231
`irreducible_count_moebius`	theorem	Surfaces/Lengths.lean	(6.2)
`isAdicComplete_of_isAdicComplete_maximalIdeal`	theorem	Surfaces/Lengths.lean		N0866
`isAdicComplete_pi`	theorem	Measure/HenselProducts.lean		N0439
`isAdicComplete_prod`	theorem	Surfaces/Lengths.lean		N0867
`isAdicComplete_quotient_of_iInf_sup_pow`	theorem	Surfaces/Lengths.lean		N0868
`isCoprime_of_isCoprime_map_residue`	theorem	Measure/HenselProducts.lean		N0437
`IsDivisionChart`	def	Measure/AdicCylinders.lean
`isDomain_of_regular_prime_element`	theorem	Surfaces/Lengths.lean		N0869
`IsEtaleForm`	def	Etale/Defs.lean	Remark 1.3
`isEtaleForm_of_good`	theorem	Etale/Main.lean		N1029
`isUnit_mk_truncIdeal_iff`	theorem	Surfaces/TruncatedSeries.lean		N0921
`IsUnramifiedLift`	def	Unramified/Extension.lean
`killT`	def	Surfaces/Lengths.lean
`killTFamily`	def	Surfaces/Lengths.lean
`killTFamily_hasSubst`	theorem	Surfaces/Lengths.lean
`killX`	def	Surfaces/Lengths.lean
`killXFamily`	def	Surfaces/Lengths.lean
`killXFamily_hasSubst`	theorem	Surfaces/Lengths.lean
`laurent_isUnit_iff_monomial`	theorem	Blowup/CurveOrders.lean		N0149
`laurent_nonnegative_twist_kernel`	theorem	Blowup/ExceptionalLayers.lean		N0193
`laurent_split_nonnegative_twist`	theorem	Blowup/ExceptionalLayers.lean		N0194
`Law`	abbrev	Basic.lean	Type variables Z_{e,f}	D008
`law_coeff_descend`	theorem	Formula/LawAlgebra.lean		N0334
`law_coeff_flatMap`	theorem	Formula/LawAlgebra.lean		N0342
`law_coeff_mul`	theorem	Formula/LawAlgebra.lean		N0343
`law_coeff_nonneg_closure`	theorem	Formula/LawAlgebra.lean		N0348
`law_coeff_prod_descend`	theorem	Formula/LawAlgebra.lean		N0345
`law_coeff_prod_formula`	theorem	Formula/LawAlgebra.lean		N0346
`law_coeff_scale`	theorem	Formula/LawAlgebra.lean		N0347
`law_safe_descend`	theorem	Formula/LawAlgebra.lean		N0349
`law_safe_mul`	theorem	Formula/LawAlgebra.lean		N0350
`law_safe_scale`	theorem	Formula/LawAlgebra.lean		N0351
`lawAtom`	def	Basic.lean		D008
`lawCoef`	def	Reciprocity/Defs.lean	Type variables Z_{e,f}	D022
`lawCoef_flatMap`	theorem	Reciprocity/Plethysm.lean		N0608
`lawCoef_globalLaw_false`	theorem	Reciprocity/Patterns.lean	(G) = (7.9)	N0565
`lawCoef_globalLaw_false_eq_recipCoef`	theorem	Reciprocity/Main.lean	Theorem 1.2, Lemma 9.2	N0551
`lawCoef_globalLaw_true`	theorem	Reciprocity/Patterns.lean	(G) = (7.9)	N0566
`lawCoef_lawProd`	theorem	Reciprocity/Plethysm.lean		N0618
`lawCoef_lawScale`	theorem	Reciprocity/Plethysm.lean		N0607
`lawCoef_nil`	theorem	Reciprocity/Plethysm.lean		N0606
`lawCoef_single_self_term`	theorem	Reciprocity/Patterns.lean	(S) = (7.11)	N0581
`lawCoef_single_term`	theorem	Reciprocity/Patterns.lean		N0567
`lawCoeff`	def	Basic.lean	Type variables Z_{e,f}	D008
`lawDescend`	def	Basic.lean	(6.4)	D008
`lawInterp`	def	Formula/LawAlgebra.lean
`lawInterp_append`	theorem	Formula/LawAlgebra.lean		N0336
`lawInterp_coeff`	theorem	Formula/LawAlgebra.lean		N0341
`lawInterp_flatMap`	theorem	Formula/LawAlgebra.lean		N0337
`lawInterp_lawMul`	theorem	Formula/LawAlgebra.lean		N0338
`lawInterp_lawProd`	theorem	Formula/LawAlgebra.lean		N0340
`lawInterp_lawScale`	theorem	Formula/LawAlgebra.lean		N0339
`lawInterp_nil`	theorem	Formula/LawAlgebra.lean		N0335
`lawMul`	def	Basic.lean	Type variables Z_{e,f}	D008
`lawOne`	def	Basic.lean		D008
`lawProd`	def	Basic.lean		D008
`LawSafe`	def	Basic.lean		D008
`LawSafe.lawWf`	theorem	Reciprocity/Plethysm.lean		N0628
`lawScale`	def	Basic.lean		D008
`LawWf`	def	Reciprocity/Defs.lean		D022
`LawWf.wf_lawCoeff`	theorem	Reciprocity/Plethysm.lean		N0629
`lawWf_globalLaw`	theorem	Reciprocity/Patterns.lean		N0556
`lawWf_stateLaw`	theorem	Reciprocity/Patterns.lean		N0555
`leftCurveIdeal`	def	Blowup/Charts.lean
`leftData`	def	Blowup/Charts.lean
`leftKernel`	def	Blowup/Charts.lean
`leftLevelIdeal`	def	Blowup/Charts.lean
`leftLevelKernel`	def	Blowup/Charts.lean
`leftMultiplicity`	def	Blowup/Charts.lean
`leftPoint`	def	Blowup/Charts.lean
`leftPoint_isPrime`	instance	Blowup/Charts.lean
`leftResidueDegree`	def	Blowup/Charts.lean
`length_double_quotient_eq`	theorem	Surfaces/Lengths.lean		N0870
`length_quotient_sup_mul_eq_add`	theorem	Surfaces/Lengths.lean		N0871
`length_quotient_sup_pow_eq_mul`	theorem	Surfaces/Lengths.lean		N0872
`length_scaling_of_residue_card`	theorem	Measure/Normalizer.lean		N0482
`level_one_kernel_polynomial`	theorem	Blowup/DivisorPoints.lean		N0186
`levelBase`	def	Blowup/Charts.lean
`levelOverlapMap`	def	Blowup/Charts.lean
`levelReduction`	def	Blowup/Charts.lean
`levelSlope`	def	Blowup/Charts.lean
`linear_composition_index`	theorem	Blowup/PointTransport.lean		N0251
`linear_image_bound_from_cokernel_length`	theorem	Measure/HenselProducts.lean		N0442
`linear_map_preserves_adic_congruence`	theorem	Measure/HenselProducts.lean		N0440
`list_get_fiber_card`	theorem	Formula/LawAlgebra.lean		N0358
`list_get_fiber_card_count`	theorem	Recursion/Termination.lean		N0796
`local_algEquiv_maximalIdeal`	theorem	Unramified/Extension.lean		N0950
`local_completion_finite_quotient`	theorem	Unramified/LocalDescent.lean		N0993
`local_law_safe`	theorem	Formula/StateCombinatorics.lean	Theorem 6.2	N0374
`LocalCompletion`	abbrev	Blowup/Charts.lean
`localCompletionMap`	def	Blowup/Charts.lean
`localCurve`	def	Blowup/Charts.lean
`localException`	def	Blowup/Charts.lean
`localFromSurface`	def	Blowup/Charts.lean
`localization_principal_quotient_commute`	theorem	Blowup/PointTransport.lean		N0254
`LocallyTransverse`	abbrev	Blowup/Charts.lean
`localQuotient`	abbrev	Blowup/Charts.lean
`localRing`	def	Blowup/Charts.lean
`localRing_commRing`	instance	Blowup/Charts.lean
`localSection`	def	Blowup/Charts.lean
`logSer`	def	Reciprocity/Defs.lean		N0703
`logSer_expSer`	theorem	Reciprocity/Plethysm.lean	(7.6)	N0587
`main_dvr`	theorem	Main.lean	Theorem 1.1, Remark 1.3	N0387
`main_dvr_cluster`	theorem	Cluster/Main.lean	Theorem 1.1, Remark 1.3	N1017
`main_dvr_etale`	theorem	Etale/Main.lean	Theorem 1.1, Remark 1.3	N1034
`main_field_form`	theorem	Main.lean	Theorem 1.1	N0388
`main_field_form_ramified`	theorem	Main.lean	Theorem 1.1	N0389
`map_maximalIdeal_localCompletion`	theorem	Blowup/CurveSections.lean		N0172
`map_maximalIdeal_localCompletion_comap_le`	theorem	Blowup/CurveSections.lean		N0174
`map_maximalIdeal_localCompletion_transport`	theorem	Blowup/CurveSections.lean		N0173
`matches_divisor_degree`	theorem	Blowup/DivisorPoints.lean	Lemma 4.3	N0184
`matches_divisor_level_one_polynomial`	theorem	Blowup/DivisorPoints.lean		N0188
`MatchesDivisor`	structure	Blowup/Charts.lean
`maximal_ideal_power_kills`	theorem	Measure/HenselProducts.lean		N0441
`maximalIdeal_twoSeries`	theorem	Surfaces/TruncatedSeries.lean
`measurableEmbedding_pi`	theorem	Measure/HenselProducts.lean		N0443
`measurableSet_inter_of_bijOn`	theorem	Assembly/TypeEvents.lean		N0111
`measurableSet_smul_image`	theorem	Assembly/NullBridges.lean		N0093
`measure_eq_sum_prod_of_preimage`	theorem	Assembly/TypeEvents.lean		N0112
`MeasuredSurface`	structure	Recursion/Members.lean
`MeasuredSurface.allowedPattern`	abbrev	Recursion/Members.lean
`MeasuredSurface.cell`	def	Recursion/Members.lean
`MeasuredSurface.cellDegree`	def	Recursion/Members.lean
`MeasuredSurface.cellIndex`	abbrev	Recursion/Members.lean
`MeasuredSurface.childDelta`	def	Recursion/Members.lean
`MeasuredSurface.childIdx`	abbrev	Recursion/Members.lean
`MeasuredSurface.childList`	def	Recursion/Members.lean
`MeasuredSurface.childState`	def	Recursion/Members.lean
`MeasuredSurface.IsSelfCell`	def	Recursion/Members.lean
`MeasuredSurface.measurableSpaceIdeal`	instance	Recursion/Members.lean
`MeasuredSurface.q`	abbrev	Recursion/Members.lean
`MeasuredSurface.stateSet`	abbrev	Recursion/Members.lean
`MeasuredSurface.μ`	def	Recursion/Members.lean
`member_cell_box_measurable`	theorem	Measure/MemberBoxes.lean	Theorem 5.1	N0460
`member_cell_box_measure`	theorem	Measure/MemberBoxes.lean	(1.7), Theorem 5.1, Proposition 6.1	N0461
`member_cell_chart_coset_decomposition`	theorem	Measure/MemberCharts.lean		N0471
`member_center_linear_part`	theorem	Measure/Haar.lean	Theorem 5.1	N0433
`member_chart_translate`	theorem	Measure/MemberCharts.lean		N0462
`member_children_degree_sum`	theorem	Measure/MemberCharts.lean		N0463
`member_coefficient_measure_map_product_coordinates`	theorem	Measure/MemberCharts.lean		N0464
`member_product_chart_pushforward`	theorem	Measure/MemberCharts.lean		N0472
`mk_mem_principalLayer`	theorem	Blowup/NilpotentGluing.lean		N0234
`module_length_quotient_ringEquiv`	theorem	Surfaces/Lengths.lean		N0873
`moebiusSum`	def	Reciprocity/Defs.lean		N0583
`moebiusSum_plethSum`	theorem	Reciprocity/Quantum.lean	(7.6)	N0659
`monic_cell_law`	theorem	Assembly/MonicCells.lean	Lemma 7.1	N0089
`monic_cells_partition`	theorem	Assembly/MonicCells.lean	Lemma 7.1	N0080
`monic_coeff_sub_mem_iff`	theorem	Unramified/PolynomialTypes.lean		N1005
`monic_congruent_difference_factor`	theorem	Unramified/FactorCells.lean		N0952
`monic_inseparable_null`	theorem	Measure/MemberCharts.lean	Remark 1.3, Remark 6.3, Discriminant locus is null	N0470
`monic_poly_reconstruct`	theorem	Unramified/FactorCells.lean		N0953
`monic_polynomial_degree`	theorem	Formula/LawAlgebra.lean		N0359
`monic_polynomial_divisor`	theorem	Assembly/TypeEvents.lean		N0115
`monic_residue_polynomial_count`	theorem	Measure/HenselProducts.lean
`monic_squarefree_factors_of_reduced`	theorem	Unramified/FactorCells.lean		N0955
`monic_type_event_measurable_of_root_cell_law`	theorem	Recursion/RootCellLaw.lean		N0774
`monicDensity`	def	Basic.lean	Monic model	D008
`monicDensity_eq_etale`	theorem	Etale/Main.lean	Remark 1.3	N1032
`monicDensityF`	def	Basic.lean		D008
`monicDensityF_eq_densityValue`	theorem	Assembly/Formulas.lean	(7.3)	N0077
`monicExpr`	def	Basic.lean	Theorem 1.1, (1.5)	D008
`monicPolynomial`	def	Basic.lean	Monic model	D008
`monicPolyO`	def	Unramified/Extension.lean
`monicPolyO_map_fraction`	theorem	Unramified/Extension.lean		N0931
`monomial_span_pow`	theorem	Blowup/PointTransport.lean		N0255
`monomialIdeal`	def	Surfaces/Lengths.lean
`monomialIdeal_mem_iff`	theorem	Surfaces/PowerSeries.lean
`mul_derivative_logSer`	theorem	Reciprocity/Defs.lean		N0522
`mul_injective_quotient_transport`	theorem	Blowup/CurveSections.lean		N0169
`mvPolynomial_zero_null`	theorem	Measure/AdicCylinders.lean	Discriminant locus is null	N0392
`mvPowerSeries_fin_two_mem_variableIdeal_iff`	theorem	Surfaces/PowerSeries.lean
`mvPowerSeries_fin_two_quotient_var_regular_mod_var`	theorem	Surfaces/PowerSeries.lean		N0875
`mvPowerSeries_fin_two_span_C_var_isPrime`	theorem	Surfaces/Lengths.lean		N0848
`mvPowerSeries_mem_span_C_var_iff`	theorem	Surfaces/Lengths.lean		N0847
`mvPowerSeries_quotient_var_regular`	theorem	Surfaces/PowerSeries.lean		N0874
`negative_laurent_twist_has_no_kernel`	theorem	Blowup/PointTransport.lean		N0257
`never_return_null`	theorem	Recursion/Events.lean	Proof of Theorem 6.2	N0730
`nilpotentEval`	def	Surfaces/Lengths.lean
`nilpotentEval_apply_generators`	theorem	Surfaces/PowerSeries.lean		N0876
`nilpotentFamily`	def	Surfaces/Lengths.lean
`nilpotentFamily_hasSubst`	theorem	Surfaces/Lengths.lean
`nonboundary_direction_count`	theorem	Formula/PatternCounts.lean	(6.3)
`nonrational_point_residue_surjective`	theorem	Surfaces/Regularity.lean		N0899
`nonself_child_rank_lt`	theorem	Formula/StateCombinatorics.lean	Contact-size order, (6.6)	N0367
`nonterminating_subset_return_or_bad`	theorem	Recursion/Termination.lean	Proof of Theorem 6.2	N0800
`nonzerodivisor_survives_localization`	theorem	Blowup/PointTransport.lean		N0258
`normalization_linear_part_cokernel_length_eq`	theorem	Blowup/PointTransport.lean		N0259
`normalizationCorrection`	def	Blowup/Charts.lean
`normalizationLinearPart`	def	Blowup/Charts.lean
`normalizationQuadratic`	def	Blowup/Charts.lean
`normalizeAt`	def	Unramified/Extension.lean
`normalized_form_cell_cylinder_mass`	theorem	Unramified/FactorCells.lean		N0956
`normalizedFormCell`	def	Unramified/Extension.lean
`normalizedGenerator`	def	Measure/AdicCylinders.lean
`normalizedIdeal`	def	Measure/AdicCylinders.lean
`normalizer_generator_equation`	theorem	Measure/Normalizer.lean		N0475
`normalizer_preserves_adic_congruence` private	theorem	Measure/Normalizer.lean	Lemma 3.1
`normalizing_factor_is_unit`	theorem	Measure/HenselProducts.lean		N0444
`one_sub_rational_returnWeight_ne_zero`	theorem	Reciprocity/Patterns.lean		N0570
`order_defect_child_le`	theorem	Recursion/OrderDefect.lean		N0761
`order_defect_children_sum`	theorem	Recursion/OrderDefect.lean		N0760
`order_defect_le_of_tower`	theorem	Recursion/Termination.lean		N0801
`order_defect_pi`	theorem	Recursion/Termination.lean		N0802
`orderDefect`	def	Algebra/AlgebraType.lean
`orderImage`	def	Algebra/AlgebraType.lean
`orig_monicDensity_eq`	theorem	Assembly/NullBridges.lean	Remark 6.3	N0097
`orig_projectiveDensity_eq`	theorem	Assembly/NullBridges.lean	Remark 6.3	N0098
`other_children_count`	theorem	Formula/LawAlgebra.lean		N0329
`otherChildren`	def	Basic.lean	(4.7)–(4.8)	D008
`overlap_exceptional_point_comap_maximal`	theorem	Blowup/PointTransport.lean		N0264
`overlap_exceptional_point_comap_maximal_right`	theorem	Blowup/PointTransport.lean		N0265
`overlap_exceptional_quotient_domain`	theorem	Blowup/PointTransport.lean		N0266
`overlap_layer_laurent_coordinates`	theorem	Blowup/NilpotentGluing.lean	(4.1)	N0229
`overlap_level_generator_regular`	theorem	Blowup/NilpotentGluing.lean		N0243
`overlap_point_residue_field_equiv`	theorem	Blowup/PointTransport.lean		N0267
`overlapCurveIdeal`	def	Blowup/Charts.lean
`overlapException`	def	Blowup/Charts.lean
`overlapSlope`	def	Blowup/Charts.lean
`padicIntegers`	abbrev	Basic.lean		D008
`padicIntegers_isDVR`	theorem	Measure/PrimitiveLocus.lean
`padicIntegers_maximal_adic_complete`	theorem	Measure/PrimitiveLocus.lean		N0492
`padicIntegers_residueField_finite`	theorem	Measure/PrimitiveLocus.lean		N0493
`PadicUnramified`	def	Basic.lean		D008
`pairwise_distinct_irreducible_pow_iInf`	theorem	Blowup/PointTransport.lean		N0270
`pairwiseDisjoint_pi_events`	theorem	Assembly/TypeEvents.lean		N0110
`parent_ideal_unique_of_level_lattice`	theorem	Blowup/CurveSections.lean		N0162
`Pattern`	abbrev	Basic.lean		D008
`pattern_divisor_count`	theorem	Formula/PatternCounts.lean	(6.3)	N0361
`pattern_entry_eq_zero_of_lt`	theorem	Reciprocity/Defs.lean		N0531
`pattern_entry_le_patternWeight`	theorem	Reciprocity/Defs.lean		N0530
`patternDivisors`	abbrev	Blowup/Directions.lean
`patternDivisors_equiv_colorings`	theorem	Formula/PatternCounts.lean	(6.3)	N0360
`patternSum`	def	Reciprocity/Defs.lean	lem-7.2	D022
`patternSum_eq_of_le`	theorem	Reciprocity/Patterns.lean		N0554
`patternWeight`	def	Basic.lean		D008
`pExp`	def	Reciprocity/Defs.lean	(7.6)	D022
`pi_algebraMap_mem_jacobson_bot`	theorem	Measure/HenselProducts.lean		N0445
`pi_field_maximal_ideals`	theorem	Algebra/AlgebraType.lean		N0067
`pi_field_quotient_equiv`	theorem	Recursion/OrderDefect.lean		N0765
`pi_fields_algEquiv_index_bijection`	theorem	Unramified/FactorCells.lean		N0958
`pi_ideal_mem_iff_map_eval`	theorem	Measure/HenselProducts.lean		N0446
`pi_mul_cokernel_length`	theorem	Measure/Normalizer.lean		N0483
`pi_quotient_span_linearEquiv`	theorem	Measure/HenselProducts.lean		N0447
`pi_strict_transform_map_eval`	theorem	Measure/Atlas.lean		N0421
`plethSum`	def	Reciprocity/Defs.lean		N0582
`plethSum_add`	theorem	Reciprocity/Quantum.lean		N0661
`plethSum_moebiusSum`	theorem	Reciprocity/Quantum.lean		N0660
`pLog`	def	Reciprocity/Defs.lean	(7.6)	D022
`point_cell_type_event`	theorem	Assembly/MonicCells.lean		N0085
`pointChart`	def	Assembly/NullBridges.lean
`pointChildState`	def	Recursion/Members.lean
`pointCount`	def	Basic.lean	(6.2)	D008
`pointCount_eval`	theorem	Surfaces/PowerSeries.lean
`polynomial_congruence_and_product`	theorem	Unramified/FactorCells.lean		N0959
`polynomial_ideal_of_irreducible_pow_le`	theorem	Blowup/PointTransport.lean		N0271
`polynomial_quotient_irreducible_pow_length`	theorem	Blowup/PointTransport.lean		N0272
`polynomial_quotient_product_equiv`	theorem	Unramified/FactorCells.lean		N0960
`polynomial_root_unique_of_derivative_isUnit`	theorem	Surfaces/PowerSeries.lean		N0879
`polynomial_type_algEquiv_iff`	theorem	Unramified/PolynomialTypes.lean		N0996
`polynomial_type_degree`	theorem	Measure/PrimitiveLocus.lean		N0491
`polynomial_type_dvd`	theorem	Algebra/AlgebraType.lean		N0061
`polynomial_type_iff_algebra_type`	theorem	Algebra/FactorInvariant.lean		N0076
`polynomial_type_map_unramified`	theorem	Unramified/DescentTypes.lean		N0929
`polynomial_type_mul_coprime`	theorem	Unramified/PolynomialTypes.lean		N0997
`polynomial_type_unique`	theorem	Unramified/PolynomialTypes.lean		N0998
`power_coordinates_transport`	theorem	Measure/HenselProducts.lean		N0448
`powerCoordinates`	def	Measure/AdicCylinders.lean
`powerSeries_quotient_length_eq_order`	theorem	Surfaces/PowerSeries.lean		N0880
`pPow`	def	Reciprocity/Defs.lean	Pow_v and the first-difference rule	D022
`pPow_mul_pPow`	theorem	Reciprocity/Plethysm.lean		N0592
`pPow_pPow`	theorem	Reciprocity/Plethysm.lean	Pow_v and the first-difference rule	N0591
`preimage_inter_pi_eq_biUnion`	theorem	Assembly/TypeEvents.lean		N0109
`prime_power_ge_two`	theorem	Formula/LawAlgebra.lean		N0324
`PrimePower`	def	Basic.lean		D008
`primitive`	def	Basic.lean	Projective model	D008
`primitive_iff_residue_ne_zero`	theorem	Unramified/PolynomialTypes.lean		N0999
`primitive_locus_mass`	theorem	Measure/PrimitiveLocus.lean		N0484
`principal_generator_orbit_count`	theorem	Measure/HenselProducts.lean		N0449
`principal_ideal_image`	theorem	Blowup/PointTransport.lean		N0273
`principal_ideal_unit_invariance`	theorem	Blowup/PointTransport.lean		N0277
`principal_layer_quotient_equiv`	theorem	Blowup/ExceptionalLayers.lean		N0200
`principal_power_unit_lift`	theorem	Blowup/NilpotentGluing.lean		N0237
`principal_residue_ideal_count`	theorem	Surfaces/TruncatedSeries.lean		N0923
`PrincipalLayer`	abbrev	Blowup/Charts.lean
`principalLayerMap`	def	Blowup/Charts.lean
`principalLayerMap_apply_eq_mk`	theorem	Blowup/NilpotentGluing.lean		N0230
`PrincipalPowerQuotient`	abbrev	Blowup/Charts.lean
`principalPowerReduction`	def	Blowup/Charts.lean
`prod_formalPow_adamsSer_clusterSer_scongr`	theorem	Reciprocity/Plethysm.lean	lem-7.2	N0589
`product_chart_projection`	theorem	Measure/Atlas.lean		N0422
`product_coordinates_exist`	theorem	Measure/HenselProducts.lean		N0450
`product_division_equiv`	theorem	Measure/HenselProducts.lean		N0451
`product_law_of_factor_laws`	theorem	Assembly/MonicCells.lean		N0081
`projective_cell_affine_type_event`	theorem	Assembly/MonicCells.lean		N0090
`projective_cell_conditional_density`	theorem	Unramified/FrobeniusDescent.lean	Lemma 7.1	N0963
`projective_cell_mass`	theorem	Unramified/FrobeniusDescent.lean		N0962
`projective_cell_normalization_pushforward`	theorem	Unramified/HomogeneousCells.lean		N0989
`projective_cells_partition`	theorem	Assembly/MonicCells.lean	Lemma 7.1	N0084
`projective_normalizer_eval`	theorem	Unramified/PolynomialTypes.lean		N1007
`projective_normalizer_positive`	theorem	Formula/LawAlgebra.lean		N0323
`projectiveCell`	def	Unramified/Extension.lean
`projectiveDensity`	def	Basic.lean	Projective model	D008
`projectiveDensity_eq_etale`	theorem	Etale/Main.lean	Remark 1.3	N1033
`projectiveDensityF`	def	Basic.lean		D008
`projectiveDensityF_eq_densityValue`	theorem	Assembly/Formulas.lean	(7.3)	N0078
`projectiveExpr`	def	Basic.lean	Theorem 1.1, (1.5)	D008
`projectiveNormalize`	def	Unramified/Extension.lean
`projectiveNormalizer`	def	Basic.lean	Lemma 7.1	D008
`projectiveNormalizer_rational_ne_zero`	theorem	Reciprocity/Quantum.lean		N0666
`pulledVariation`	def	Blowup/Charts.lean
`qact`	def	Reciprocity/Defs.lean	(8.9)	D022
`qact_gaussPhi_dilate_recipSer_scongr` private	theorem	Reciprocity/Main.lean	(9.4)
`qact_qmul`	theorem	Reciprocity/Defs.lean		N0536
`qact_qone`	theorem	Reciprocity/Defs.lean		N0537
`qact_sub`	theorem	Reciprocity/Defs.lean		N0538
`qactRecip`	def	Reciprocity/Defs.lean	Lemma 9.1	D022
`QCongr`	def	Reciprocity/Defs.lean		D022
`QCongr.mono`	theorem	Reciprocity/Defs.lean		N0539
`QCongr.qact_scongr`	theorem	Reciprocity/Defs.lean		N0533
`QCongr.qmul`	theorem	Reciprocity/Defs.lean		N0541
`QCongr.trans`	theorem	Reciprocity/Defs.lean		N0540
`qcongr_crossingQ_mul_qdagger`	theorem	Reciprocity/Patterns.lean	Lemma 8.3, Theorem 9.3	N0577
`qcongr_qdiag_mul_qdagger`	theorem	Reciprocity/Quantum.lean	Lemma 8.3	N0689
`qcongr_qminus_qone`	theorem	Reciprocity/Defs.lean		N0548
`qcongr_qplus_qone`	theorem	Reciprocity/Defs.lean		N0547
`qdagger`	def	Reciprocity/Defs.lean	(8.2)	N0650
`qdagger_qminus`	theorem	Reciprocity/Quantum.lean	Lemma 8.1	N0670
`qdagger_qmul`	theorem	Reciprocity/Quantum.lean	Lemma 8.1	N0668
`qdagger_qplus`	theorem	Reciprocity/Quantum.lean	Lemma 8.1	N0669
`qdiag`	def	Reciprocity/Defs.lean		N0542
`qdiag_mul`	theorem	Reciprocity/Quantum.lean	Lemma 8.1	N0688
`qminus`	def	Reciprocity/Defs.lean	Lemma 8.1	N0652
`qminus_qmul`	theorem	Reciprocity/Defs.lean	Lemma 8.1	N0544
`qmul`	def	Reciprocity/Defs.lean	(8.1)	N0541
`qmul_assoc`	theorem	Reciprocity/Quantum.lean	Lemma 8.1	N0671
`qmul_qplus_qdiag_qminus_apply`	theorem	Reciprocity/Defs.lean		N0546
`qmul_zero_zero`	theorem	Reciprocity/Quantum.lean		N0654
`qone`	def	Reciprocity/Defs.lean	(8.1)	D022
`qone_qmul`	theorem	Reciprocity/Defs.lean		N0545
`qplus`	def	Reciprocity/Defs.lean	Lemma 8.1	N0651
`qplus_qmul`	theorem	Reciprocity/Defs.lean	Lemma 8.1	N0543
`QPositive`	def	Reciprocity/Defs.lean		D022
`QPositive.qdagger`	theorem	Reciprocity/Quantum.lean		N0650
`QPositive.qminus`	theorem	Reciprocity/Quantum.lean		N0652
`QPositive.qmul`	theorem	Reciprocity/Quantum.lean		N0541
`QPositive.qplus`	theorem	Reciprocity/Quantum.lean		N0651
`qPositive_qdiag`	theorem	Reciprocity/Quantum.lean		N0653
`qpow`	def	Reciprocity/Defs.lean		D022
`qpow_add`	theorem	Reciprocity/Defs.lean		N0502
`qpow_natCast`	theorem	Reciprocity/Quantum.lean		N0646
`qpow_neg_mul_qpow`	theorem	Reciprocity/Quantum.lean		N0648
`qpow_one`	theorem	Reciprocity/Quantum.lean		N0647
`qpow_zero`	theorem	Reciprocity/Defs.lean		N0503
`qrecip`	def	Reciprocity/Defs.lean		D022
`QSer`	abbrev	Reciprocity/Defs.lean	(8.1)	D022
`quotient_mul_range_equiv`	theorem	Measure/HenselProducts.lean		N0452
`quotient_ring_length_intrinsic`	theorem	Measure/PrimitiveLocus.lean		N0494
`RaisesAdicOrder`	def	Measure/AdicCylinders.lean
`ramificationIdx_unramified_tower`	theorem	Unramified/FrobeniusDescent.lean		N0966
`rank_lt_of_degree_lt`	theorem	Formula/LawAlgebra.lean		N0330
`rat_smul_eq_scalar_mul`	theorem	Reciprocity/Quantum.lean		N0645
`rational_divisorCount`	theorem	Reciprocity/Plethysm.lean		N0625
`rational_divisorProbability_single`	theorem	Reciprocity/Patterns.lean	Proposition 6.1	N0568
`rational_eminusOne`	theorem	Reciprocity/Plethysm.lean		N0624
`rational_returnWeight`	theorem	Reciprocity/Patterns.lean		N0569
`recip_cluster`	theorem	Cluster/Main.lean		N1023
`recip_main`	theorem	Reciprocity/Main.lean	Theorem 1.2, Remark 1.3, Corollary 10.3	N0553
`recipCoef`	def	Reciprocity/Defs.lean		D022
`recipCoef_adamsCoef`	theorem	Reciprocity/Quantum.lean		N0637
`recipCoef_coeff`	theorem	Reciprocity/Quantum.lean		N0635
`recipCoef_lawCoef_globalLaw_true`	theorem	Reciprocity/Main.lean	Theorem 1.2, Lemma 9.2	N0552
`recipCoef_recipCoef`	theorem	Reciprocity/Quantum.lean		N0636
`recipCoef_scalar`	theorem	Reciprocity/Quantum.lean		N0634
`recipCoef_single`	theorem	Reciprocity/Quantum.lean		N0632
`recipPoly`	def	Reciprocity/Defs.lean		D022
`recipRat`	def	Reciprocity/Defs.lean		D022
`recipRat_algebraMap`	theorem	Reciprocity/Defs.lean		N0504
`recipRat_C`	theorem	Reciprocity/Defs.lean		N0505
`recipRat_projectiveNormalizer`	theorem	Reciprocity/Quantum.lean	Lemma 9.2	N0665
`recipRat_recipRat`	theorem	Reciprocity/Quantum.lean		N0630
`recipRat_X`	theorem	Reciprocity/Defs.lean		N0507
`recipSer`	def	Reciprocity/Defs.lean		D022
`recipSer_dilate`	theorem	Reciprocity/Quantum.lean		N0680
`recipSer_gaussPhi`	theorem	Reciprocity/Quantum.lean		N0684
`recipSer_mul`	theorem	Reciprocity/Quantum.lean		N0673
`recipSer_pPow`	theorem	Reciprocity/Quantum.lean	(7.6)	N0690
`recipSer_qact`	theorem	Reciprocity/Quantum.lean		N0667
`recipSer_recipSer`	theorem	Reciprocity/Quantum.lean		N0674
`recursion_crossing_law`	theorem	Recursion/Events.lean	Proof of Theorem 6.2	N0728
`recursion_events_measurable`	theorem	Recursion/Events.lean		N0725
`recursion_single_law`	theorem	Recursion/Events.lean	Proof of Theorem 6.2	N0731
`recursion_terminal_law`	theorem	Recursion/ChildMembers.lean		N0716
`reduced_form_eq_of_residue_coeff`	theorem	Blowup/NilpotentGluing.lean		N0238
`reducedFormCell`	def	Unramified/Extension.lean
`reducedFormProduct`	def	Unramified/Extension.lean
`regular_principal_generators_associated`	theorem	Measure/HenselProducts.lean		N0453
`RegularAt`	def	Basic.lean		D008
`RegularParameterPair`	def	Blowup/Charts.lean
`repeated_root_chart_type`	theorem	Recursion/OrderDefect.lean		N0769
`repeated_root_one_chart_atlas`	theorem	Recursion/OrderDefect.lean	(7.1)	N0770
`residue_basis_family_basis`	theorem	Surfaces/PowerSeries.lean		N0883
`residue_basis_family_lift_along_reduction`	theorem	Surfaces/PowerSeries.lean		N0881
`residue_basis_family_of_length`	theorem	Surfaces/PowerSeries.lean		N0882
`residue_cell_cylinder`	theorem	Unramified/PolynomialTypes.lean		N1008
`residue_cell_mass`	theorem	Unramified/PolynomialTypes.lean	Lemma 7.1	N1009
`residue_extension_equiv`	theorem	Unramified/PolynomialTypes.lean		N1011
`residue_extension_field`	theorem	Unramified/PolynomialTypes.lean		N1012
`residue_ideal_has_fixed_generator_lift`	theorem	Measure/PrimitiveLocus.lean		N0488
`residue_quotient_card`	theorem	Measure/HenselProducts.lean		N0454
`residue_vector_fiber_mass`	theorem	Unramified/PolynomialTypes.lean		N1015
`ResidueBasisFamily`	def	Surfaces/Lengths.lean
`residueCard`	abbrev	Unramified/Extension.lean
`residueCell`	def	Unramified/Extension.lean
`residueEmbed`	def	Unramified/Extension.lean
`residueExtension`	abbrev	Unramified/Extension.lean
`residueIdealCell`	def	Measure/AdicCylinders.lean
`residueKillT`	def	Surfaces/Lengths.lean
`residueKillT_apply_ker`	theorem	Surfaces/PowerSeries.lean		N0878
`residueKillT_xChartSubst`	theorem	Surfaces/ConcretePoints.lean		N0837
`residueKillX`	def	Surfaces/Lengths.lean
`residuePatterns`	def	Basic.lean	(7.3)	D008
`residuePoly`	abbrev	Unramified/Extension.lean
`residueRepresentative`	def	Blowup/Charts.lean
`residueSeries`	def	Surfaces/Lengths.lean
`residueVector`	def	Unramified/Extension.lean
`resultant_ne_zero_of_separable`	theorem	Measure/MemberCharts.lean		N0466
`return_event_mass`	theorem	Recursion/Events.lean	Proof of Theorem 6.2	N0729
`return_weight_bounds`	theorem	Formula/StateCombinatorics.lean		N0372
`returnWeight`	def	Basic.lean	(6.6)	D008
`reverse_normalized_irreducible`	theorem	Algebra/FactorInvariant.lean		N0072
`reverse_polynomial_type_iff`	theorem	Algebra/FactorInvariant.lean		N0073
`rightCurveIdeal`	def	Blowup/Charts.lean
`rightData`	def	Blowup/Charts.lean
`rightKernel`	def	Blowup/Charts.lean
`rightLevelIdeal`	def	Blowup/Charts.lean
`rightLevelKernel`	def	Blowup/Charts.lean
`rightMultiplicity`	def	Blowup/Charts.lean
`rightPoint`	def	Blowup/Charts.lean
`rightPoint_isPrime`	instance	Blowup/Charts.lean
`rightResidueDegree`	def	Blowup/Charts.lean
`ringCechDifferential`	def	Blowup/Charts.lean
`root_cell_clauses_reindex`	theorem	Recursion/OrderDefect.lean		N0766
`root_cell_law`	theorem	Recursion/RootCellLaw.lean	(1.3), Cluster model and cluster law B_n, (7.1)	N0780
`root_cell_law_at_universe_member`	theorem	Recursion/RootCellLaw.lean		N0775
`root_field_algEquiv_conjugate_orbit`	theorem	Unramified/FactorCells.lean		N0961
`rootBar`	abbrev	Unramified/Extension.lean
`RootCellLaw`	def	Assembly/NullBridges.lean	Cluster model and cluster law B_n, (7.1)
`rootEvent`	def	Assembly/NullBridges.lean
`rootLaw`	def	Basic.lean	(1.5), Cluster model and cluster law B_n	D008
`rootMultiplicity_map_eq_count_normalizedFactors`	theorem	Blowup/ExceptionalLayers.lean		N0202
`scalar`	def	Reciprocity/Defs.lean		D022
`scalar_add`	theorem	Reciprocity/Quantum.lean		N0641
`scalar_class_card`	theorem	Unramified/PolynomialTypes.lean		N1016
`scalar_eq_algebraMap`	theorem	Reciprocity/Quantum.lean		N0643
`scalar_mul`	theorem	Reciprocity/Quantum.lean		N0640
`scalar_mul_eq_smul`	theorem	Reciprocity/Quantum.lean		N0644
`scalar_mul_left_cancel`	theorem	Reciprocity/Quantum.lean		N0691
`scalar_one`	theorem	Reciprocity/Quantum.lean		N0642
`scalarClass`	def	Unramified/Extension.lean
`scale_type_valid_degree_iff`	theorem	Formula/StateCombinatorics.lean		N0378
`scaled_inverse_from_image_containment`	theorem	Blowup/StrictNormalizer.lean		N0282
`scaled_linear_image_index`	theorem	Blowup/StrictNormalizer.lean		N0283
`scaled_normalization_identity`	theorem	Measure/PrimitiveLocus.lean	Lemma 3.1	N0485
`scaled_strict_map_measurable`	theorem	Recursion/OrderDefect.lean		N0767
`scaledStrictMap`	def	Blowup/Charts.lean
`scaleType`	def	Basic.lean	(6.4)	D008
`scaleTypeHom`	def	Reciprocity/Defs.lean		D022
`scaling_image_borel_mass`	theorem	Formula/TypeTransport.lean		N0386
`SCongr`	def	Reciprocity/Defs.lean		D022
`SCongr.C_mul`	theorem	Reciprocity/Quantum.lean		N0698
`SCongr.dilate`	theorem	Reciprocity/Quantum.lean		N0681
`SCongr.expSer`	theorem	Reciprocity/Quantum.lean		N0702
`SCongr.logSer`	theorem	Reciprocity/Quantum.lean		N0703
`SCongr.moebiusSum`	theorem	Reciprocity/Plethysm.lean		N0583
`SCongr.mono`	theorem	Reciprocity/Quantum.lean		N0539
`SCongr.mul`	theorem	Reciprocity/Quantum.lean		N0697
`SCongr.of_eq`	theorem	Reciprocity/Quantum.lean		N0693
`SCongr.of_mul_right`	theorem	Reciprocity/Quantum.lean		N0700
`SCongr.plethSum`	theorem	Reciprocity/Plethysm.lean		N0582
`SCongr.pow`	theorem	Reciprocity/Quantum.lean		N0699
`SCongr.qdiag`	theorem	Reciprocity/Defs.lean		N0542
`SCongr.refl`	theorem	Reciprocity/Quantum.lean
`SCongr.symm`	theorem	Reciprocity/Quantum.lean		N0694
`SCongr.trans`	theorem	Reciprocity/Quantum.lean		N0540
`sectionsToProduct`	def	Blowup/Charts.lean
`selectBlock`	def	Unramified/Extension.lean
`self_patterns_of_single_state`	theorem	Formula/StateCombinatorics.lean	(6.6)	N0366
`SelfPattern`	def	Basic.lean		D008
`selfPattern_single_iff`	theorem	Reciprocity/Plethysm.lean		N0595
`separable_of_resultant`	theorem	Measure/MemberCharts.lean		N0465
`Ser`	abbrev	Reciprocity/Defs.lean	(7.5)	D022
`series_quotient_equiv_adjoinRoot`	theorem	Recursion/OrderDefect.lean	(7.1)	N0768
`shiftUnit`	def	Surfaces/Lengths.lean
`simple_root_derivative_unit`	theorem	Unramified/FrobeniusDescent.lean		N0971
`single_residue_ideal_count`	theorem	Measure/StateVolumes.lean	Proposition 3.3	N0495
`single_special_fiber_length`	theorem	Unramified/LocalDescent.lean	Lemma 2.1	N0992
`single_state_return_chain`	theorem	Recursion/ChildMembers.lean		N0718
`single_state_volume`	theorem	Measure/StateVolumes.lean	Proposition 3.3	N0496
`singleResidueIdeals`	def	Surfaces/Lengths.lean	Allowed residue ideals, cells, occupied points
`span_pow_mul_colon_eq`	theorem	Surfaces/ConcreteAtlas.lean		N0830
`special_fiber_crossing_contact_regular`	theorem	Blowup/StrictNormalizer.lean	Lemma 2.1	N0287
`special_fiber_single_contact_regular`	theorem	Blowup/StrictNormalizer.lean	Lemma 2.1	N0288
`SpecialFiber`	abbrev	Surfaces/Lengths.lean
`squarefree_map_of_isSeparable`	theorem	Algebra/AlgebraType.lean		N0055
`squarefree_monic_has_polynomial_type`	theorem	Algebra/AlgebraType.lean		N0060
`squarefree_of_isReduced_adjoinRoot`	theorem	Algebra/AlgebraType.lean		N0054
`State`	inductive	Basic.lean	(2.1)	D008
`State.degree`	def	Basic.lean	(2.1)	D008
`State.firstContact`	def	Formula/LawAlgebra.lean
`State.rank`	def	Basic.lean	Contact-size order	D008
`State.tag`	def	Basic.lean		D008
`State.terminal`	def	Basic.lean		D008
`State.Valid`	def	Basic.lean	(2.1)	D008
`State.weight`	def	Basic.lean		D008
`state_fuel_stable`	theorem	Formula/StateCombinatorics.lean		N0368
`state_law_coeff_nonneg`	theorem	Formula/PatternCounts.lean		N0363
`state_law_unfold`	theorem	Formula/StateCombinatorics.lean	(6.7), Theorem 6.2	N0369
`state_measure_atlas_independent`	theorem	Measure/Atlas.lean	Proposition 3.2	N0428
`state_measure_total_mass`	theorem	Measure/PrimitiveLocus.lean		N0486
`stateContactT`	def	Blowup/Charts.lean
`stateContactX`	def	Blowup/Charts.lean
`stateLaw`	def	Basic.lean	Theorem 6.2	D008
`stateLawFuel`	def	Basic.lean	(6.7)	D008
`stateMeasure`	def	Measure/AdicCylinders.lean
`StateShape`	def	Recursion/Members.lean
`StateShape.valid`	theorem	Recursion/Members.lean
`stateVolume`	def	Basic.lean	Proposition 3.3	D008
`strict_chart_coordinates_commute`	theorem	Blowup/StrictNormalizer.lean		N0293
`strict_chart_one_ball_measure`	theorem	Assembly/NullBridges.lean	Theorem 5.1	N0095
`strict_chart_preimage_set_identity`	theorem	Blowup/StrictNormalizer.lean		N0294
`strict_correction_raises_order`	theorem	Blowup/StrictNormalizer.lean		N0290
`strict_normalizer_factors_through_linear`	theorem	Blowup/StrictNormalizer.lean		N0291
`strict_normalizer_lattice_image`	theorem	Blowup/StrictNormalizer.lean		N0292
`strict_normalizer_preimage_measure`	theorem	Assembly/NullBridges.lean		N0092
`strict_normalizer_pushforward_linear`	theorem	Measure/Haar.lean		N0432
`strict_quotient_cokernel_length`	theorem	Blowup/StrictNormalizer.lean	Theorem 5.1	N0295
`strict_quotient_inclusion_exists`	theorem	Blowup/StrictNormalizer.lean		N0296
`strict_quotient_map_exists`	theorem	Blowup/StrictNormalizer.lean		N0297
`strict_quotient_map_injective`	theorem	Blowup/StrictNormalizer.lean		N0298
`strict_transform_bijOn_child_ideals`	theorem	Blowup/FixedTangentCellBijection.lean	Proposition 4.4	N0206
`strict_transform_common_point_transport`	theorem	Blowup/StrictNormalizer.lean		N0299
`strict_transform_equation_from_levels`	theorem	Blowup/StrictNormalizer.lean		N0301
`strict_transform_equation_of_kernels`	theorem	Blowup/CurveSections.lean		N0175
`strict_transform_ideal_of_generator`	theorem	Measure/Haar.lean		N0429
`strict_transform_injOn_fixed_tangent_cell`	theorem	Blowup/FixedTangentCellBijection.lean	Proposition 4.4	N0205
`strict_transform_left_point_equation`	theorem	Blowup/CurveSections.lean		N0178
`strict_transform_mapsTo_child_ideals`	theorem	Blowup/StrictNormalizer.lean	(4.7)–(4.8)	N0280
`strict_transform_translate_measure`	theorem	Assembly/NullBridges.lean		N0096
`strict_transforms_give_level_lattice_membership`	theorem	Blowup/StrictNormalizer.lean		N0302
`strictTransformAt`	def	Blowup/Charts.lean
`strictTransformIdeal`	def	Blowup/Charts.lean
`substUnit`	def	Surfaces/Lengths.lean
`sum_allowedPatterns_crossing`	theorem	Reciprocity/Defs.lean		N0528
`sum_allowedPatterns_reindex`	theorem	Reciprocity/Defs.lean		N0527
`sum_allowedPatterns_single`	theorem	Reciprocity/Plethysm.lean		N0594
`sum_C_mul_X_pow_pow`	theorem	Reciprocity/Defs.lean		N0532
`sum_divisors_moebius`	theorem	Reciprocity/Quantum.lean		N0658
`sum_divisors_sum_divisors_div`	theorem	Reciprocity/Quantum.lean		N0656
`sum_patterns_scalar_mul_eq_patternSum`	theorem	Reciprocity/Patterns.lean		N0562
`sum_prod_densityValue_eq_lawProd`	theorem	Assembly/TypeEvents.lean		N0113
`sum_triple_reindex`	theorem	Reciprocity/Plethysm.lean		N0597
`surface_state_generator_mem_maximal`	theorem	Blowup/H0Comparison.lean		N0213
`surface_state_ideal_proper`	theorem	Blowup/H0Comparison.lean		N0212
`surface_state_vertical_perturbation`	theorem	Blowup/H0Comparison.lean		N0214
`surface_threads_injective`	theorem	Blowup/H0Comparison.lean	Lemma 4.2	N0218
`surface_threads_range`	theorem	Blowup/H0Comparison.lean	Lemma 4.1, Lemma 4.2, Appendix A	N0221
`surface_to_cech_kernel`	theorem	Blowup/H0Comparison.lean		N0215
`surface_to_cech_range`	theorem	Blowup/H0Comparison.lean		N0219
`surface_to_curve_limit_exists`	theorem	Blowup/H0Comparison.lean		N0223
`surface_to_curve_limit_kernel`	theorem	Blowup/CurveSections.lean		N0163
`surface_to_curve_quotient_kernel`	theorem	Blowup/CurveSections.lean		N0161
`surface_vertical_parameter`	theorem	Blowup/H0Comparison.lean		N0224
`SurfaceData`	structure	Surfaces/Lengths.lean	(2.1)
`surfaceIdeal`	def	Surfaces/Lengths.lean
`surfaceIdeal_ne_top`	theorem	Surfaces/PowerSeries.lean		N0896
`surfaceMk`	def	Surfaces/Lengths.lean
`surfaceParameterIdeal`	def	Surfaces/Lengths.lean
`surfaceRelation`	def	Surfaces/Lengths.lean
`surfaceRelation_constantCoeff`	theorem	Surfaces/PowerSeries.lean		N0886
`surfaceStateSet`	def	Surfaces/Lengths.lean	(2.1)
`surfaceT`	def	Surfaces/Lengths.lean
`surfaceThreads`	def	Blowup/Charts.lean
`surfaceToCechInput`	def	Blowup/Charts.lean
`surfaceToChartPair`	def	Blowup/Charts.lean
`surfaceUnit`	def	Surfaces/Lengths.lean
`SurfaceUniverse`	structure	Recursion/Members.lean
`SurfaceUniverse.badExitEvent`	def	Recursion/Members.lean
`SurfaceUniverse.childBox`	def	Recursion/Members.lean
`SurfaceUniverse.ChildTypesExist`	def	Recursion/Members.lean
`SurfaceUniverse.exitCells`	def	Recursion/Members.lean
`SurfaceUniverse.exitEvent`	def	Recursion/Members.lean
`SurfaceUniverse.InvariantDecreases`	def	Recursion/Members.lean
`SurfaceUniverse.LawStatement`	def	Recursion/Members.lean	Theorem 6.2
`SurfaceUniverse.nonterminatingSet`	def	Recursion/Members.lean
`SurfaceUniverse.returnEvent`	def	Recursion/Members.lean
`SurfaceUniverse.selfCells`	def	Recursion/Members.lean
`SurfaceUniverse.termExitEvent`	def	Recursion/Members.lean
`SurfaceUniverse.Terminates`	inductive	Recursion/Members.lean
`SurfaceUniverse.terminatingSet`	def	Recursion/Members.lean
`SurfaceUniverse.termTypeEvent`	def	Recursion/Members.lean
`SurfaceUniverse.typeBox`	def	Recursion/Members.lean
`SurfaceUniverse.typeEvent`	def	Recursion/Members.lean
`surfaceX`	def	Surfaces/Lengths.lean
`t_chart_nonrational_point_child_data`	theorem	Recursion/OrderDefect.lean		N0772
`t_chart_nonrational_point_completion_equiv`	theorem	Surfaces/ChartCompletions.lean		N0808
`t_chart_origin_completion_equiv`	theorem	Surfaces/ChartCompletions.lean		N0810
`t_chart_point_child_member`	theorem	Recursion/ChildMembers.lean		N0704
`t_chart_rational_point_child_data`	theorem	Recursion/OrderDefect.lean		N0773
`t_chart_unit_point_completion_equiv`	theorem	Surfaces/ChartCompletions.lean		N0811
`tangent_count_nonneg`	theorem	Formula/PatternCounts.lean		N0362
`tangent_divisor_unique`	theorem	Recursion/ChildMembers.lean	Proposition 6.1	N0707
`tangentCount`	def	Basic.lean	(6.3)	D008
`tangentLift`	def	Blowup/Charts.lean
`TangentPattern`	structure	Basic.lean	Allowed residue ideals, cells, occupied points	D008
`tChartFamily`	def	Surfaces/Lengths.lean
`tChartFamily_hasSubst`	theorem	Surfaces/Lengths.lean
`term_type_event_cell_decomposition`	theorem	Recursion/ChildMembers.lean		N0717
`terminal_curve_order_dvr`	theorem	Recursion/ChildMembers.lean	Lemma 2.2	N0710
`terminal_field_invariant`	theorem	Recursion/ChildMembers.lean	Lemma 2.2	N0712
`terminal_law`	theorem	Formula/StateCombinatorics.lean	Lemma 2.2	N0370
`terminates_cell_decomposition`	theorem	Recursion/ChildMembers.lean		N0714
`terminates_type_unique`	theorem	Recursion/ChildMembers.lean		N0715
`Tests.clusterDensity_two_inert`	theorem	Tests/Cluster.lean	(1.3)	N1020
`Tests.clusterDensity_two_ramified`	theorem	Tests/Cluster.lean	(1.3)	N1018
`Tests.clusterDensity_two_split`	theorem	Tests/Cluster.lean	(1.3)	N1019
`Tests.crossing_left_one_law` private	theorem	Tests/Regression.lean	Lemma 2.2
`Tests.crossing_right_one_law` private	theorem	Tests/Regression.lean	Lemma 2.2
`Tests.crossing_two_two_law` private	theorem	Tests/Regression.lean	Example 9.4
`Tests.crossing_two_two_law_at_two` private	theorem	Tests/Regression.lean	Example 9.4
`Tests.instance@L104`	instance	Tests/NonVacuity.lean
`Tests.instance@L107`	instance	Tests/NonVacuity.lean
`Tests.instance@L44`	instance	Tests/NonVacuity.lean
`Tests.instance@L48`	instance	Tests/NonVacuity.lean
`Tests.instance@L52`	instance	Tests/NonVacuity.lean
`Tests.instance@L55`	instance	Tests/NonVacuity.lean
`Tests.instance@L59`	instance	Tests/NonVacuity.lean
`Tests.instance@L62`	instance	Tests/NonVacuity.lean
`Tests.isAdic_maximalIdeal_powerSeries`	theorem	Tests/NonVacuity.lean		N0001
`Tests.main_dvr_galoisField`	theorem	Tests/NonVacuity.lean		N0004
`Tests.main_dvr_powerSeries`	theorem	Tests/NonVacuity.lean	Theorem 1.1	N0002
`Tests.main_dvr_zmod`	theorem	Tests/NonVacuity.lean		N0003
`Tests.monicDensity_four_ramified_quadratic_of_card_eq_two`	theorem	Tests/Regression.lean		N0046
`Tests.monicDensity_four_totally_ramified_of_card_eq_two`	theorem	Tests/Regression.lean	Example 10.4	N0044
`Tests.monicDensity_four_two_inert_quadratics_of_card_eq_two`	theorem	Tests/Regression.lean		N0047
`Tests.monicDensity_powerSeries_zmod_two_four_totally_ramified`	theorem	Tests/Regression.lean	Example 10.4	N0048
`Tests.monicDensity_three_totally_ramified_of_card_eq_three`	theorem	Tests/Regression.lean	(10.8)	N0043
`Tests.monicDensity_two_ramified`	theorem	Tests/Regression.lean	(1.3)	N0041
`Tests.monicExpr_four_eval_two`	theorem	Tests/Regression.lean		N0031
`Tests.monicExpr_four_ramified_quadratic_eval_two`	theorem	Tests/Regression.lean		N0039
`Tests.monicExpr_four_totally_ramified_eval_two`	theorem	Tests/Regression.lean	Example 10.4	N0037
`Tests.monicExpr_four_two_inert_quadratics_eval_two`	theorem	Tests/Regression.lean		N0040
`Tests.monicExpr_three_eval`	theorem	Tests/Regression.lean		N0025
`Tests.monicExpr_three_totally_ramified_eval_three`	theorem	Tests/Regression.lean	(10.8)	N0036
`Tests.monicExpr_two_eval`	theorem	Tests/Regression.lean	(1.3), Example 7.3, (10.8), (11.8), (11.9)–(11.10)	N0020
`Tests.monicExpr_two_inert_eval_two`	theorem	Tests/Regression.lean		N0034
`Tests.monicExpr_two_ramified_eval_two`	theorem	Tests/Regression.lean	Example 7.3	N0035
`Tests.monicExpr_two_split_eval_two`	theorem	Tests/Regression.lean		N0033
`Tests.projectiveDensity_four_totally_ramified_of_card_eq_two`	theorem	Tests/Regression.lean		N0045
`Tests.projectiveDensity_two_ramified`	theorem	Tests/Regression.lean	Example 7.3	N0042
`Tests.projectiveExpr_four_eval_two`	theorem	Tests/Regression.lean		N0032
`Tests.projectiveExpr_four_totally_ramified_eval_two`	theorem	Tests/Regression.lean	Example 10.4	N0038
`Tests.projectiveExpr_two_eval`	theorem	Tests/Regression.lean	Example 7.3, (11.8)	N0021
`Tests.single_two_law`	theorem	Tests/Regression.lean	Example 6.4, Example 7.3	N0018
`Tests.stateLawFuelStep`	def	Tests/Regression.lean
`towerDelta`	def	Surfaces/Lengths.lean
`towerThreads`	def	Surfaces/Lengths.lean
`transition_unit_congruent_one`	theorem	Blowup/H0Comparison.lean		N0227
`translateBlock`	def	Unramified/Extension.lean
`transverse_of_reduction_ne_zero`	theorem	Surfaces/Completeness.lean		N0815
`tri`	def	Basic.lean		D008
`tri_chooseTwo`	theorem	Formula/StateCombinatorics.lean		N0371
`truncCoeffs`	def	Surfaces/TruncatedSeries.lean
`truncCoeffs_apply`	theorem	Surfaces/TruncatedSeries.lean		N0920
`truncExponent`	def	Surfaces/TruncatedSeries.lean
`truncIndex`	def	Surfaces/TruncatedSeries.lean
`twisted_kernel_from_surface`	theorem	Blowup/H0Comparison.lean		N0228
`two_chart_common_multiplicity_eq`	theorem	Blowup/DivisorPoints.lean		N0182
`two_chart_datum_concrete_instances`	theorem	Surfaces/ConcreteStrictTransforms.lean		N0842
`two_chart_datum_concrete_transverse`	theorem	Surfaces/ConcreteStrictTransforms.lean		N0843
`two_chart_global_function_exists`	theorem	Blowup/FixedTangentCellBijection.lean	Lemma 4.3	N0203
`two_chart_kernels_agree_on_overlap`	theorem	Blowup/TwoChartCurveData.lean		N0304
`two_chart_layer_correction`	theorem	Blowup/CurveSections.lean		N0165
`two_chart_left_data_transverse_finite`	theorem	Blowup/CurveSections.lean		N0176
`two_chart_left_generators_regular_on_overlap`	theorem	Blowup/TwoChartCurveData.lean		N0312
`two_chart_left_level_one_kernel_polynomial`	theorem	Blowup/DivisorPoints.lean		N0187
`two_chart_left_points_maximal`	theorem	Blowup/CurveSections.lean		N0177
`two_chart_level_generators_agree_on_overlap`	theorem	Blowup/TwoChartCurveData.lean		N0305
`two_chart_level_generators_exist`	theorem	Blowup/TwoChartCurveData.lean		N0313
`two_chart_right_data_transverse_finite`	theorem	Blowup/CurveSections.lean		N0179
`two_chart_right_points_maximal`	theorem	Blowup/TwoChartCurveData.lean		N0306
`two_mul_chooseTwo`	theorem	Reciprocity/Defs.lean		N0500
`two_mul_tri`	theorem	Reciprocity/Defs.lean		N0499
`two_term_coker_map_surjective`	theorem	Blowup/TwoChartCurveData.lean		N0315
`TwoChartCurveData`	structure	Blowup/Charts.lean
`TwoSeries`	abbrev	Surfaces/Lengths.lean
`twoSeries_eval_exists_of_isAdicComplete`	theorem	Surfaces/Completeness.lean		N0818
`twoSeries_ringHom_ext_of_isNilpotent`	theorem	Surfaces/Completeness.lean		N0816
`twoSeriesResidueEquiv`	def	Surfaces/TruncatedSeries.lean
`twoTermCokerMap`	def	Surfaces/Lengths.lean
`type_event_null_difference`	theorem	Recursion/Events.lean		N0733
`typeDegree`	def	Basic.lean	Type of degree n	D008
`typeEvent`	def	Assembly/NullBridges.lean
`unique_scaled_generator_normalization`	theorem	Measure/Normalizer.lean	Lemma 3.1	N0477
`units_lift_from_local_quotient`	theorem	Measure/PrimitiveLocus.lean		N0487
`universal_law_statement`	theorem	Recursion/Events.lean	Theorem 6.2	N0732
`universe_basic_facts`	theorem	Recursion/ChildMembers.lean		N0719
`unramified_coefficient_measure_haar`	theorem	Measure/PrimitiveLocus.lean		N0489
`unramified_coefficient_measure_pi`	theorem	Measure/Haar.lean	Theorem 5.1	N0431
`unramified_extension_measure_package`	theorem	Measure/Haar.lean		N0430
`unramified_fraction_base_change`	theorem	Algebra/AlgebraType.lean		N0068
`unramified_fraction_field_lift`	theorem	Unramified/FrobeniusDescent.lean		N0967
`unramified_fraction_isSeparable`	theorem	Unramified/DescentTypes.lean		N0927
`unramified_free_module`	theorem	Unramified/FrobeniusDescent.lean		N0968
`unramified_generic_fibre_ascent`	theorem	Recursion/Events.lean		N0735
`unramified_generic_fibre_witness`	theorem	Algebra/AlgebraType.lean		N0069
`unramified_is_dvr`	theorem	Unramified/FrobeniusDescent.lean	Standard facts	N0977
`unramified_lift_map_parameter_quotient_irreducible`	theorem	Surfaces/Completeness.lean		N0819
`unramified_root_isUnit_of_two_le_natDegree`	theorem	Surfaces/Completeness.lean		N0820
`unramifiedCoefficientMeasure`	def	Measure/AdicCylinders.lean
`unramifiedFrobenius`	def	Unramified/Extension.lean
`unramifiedMeasurableSpace`	def	Measure/AdicCylinders.lean
`unramifiedTopology`	def	Measure/AdicCylinders.lean
`ValidType`	def	Basic.lean	Type of degree n	D008
`variableIdeal`	def	Surfaces/Lengths.lean
`wf_returnWeight`	theorem	Reciprocity/Plethysm.lean		N0599
`x_chart_infinity_completion_equiv`	theorem	Surfaces/ChartCompletions.lean		N0812
`X_inv_sub_X_zpow_neg_tri_ne_zero`	theorem	Reciprocity/Patterns.lean	Proof of monic/cluster reciprocity	N0571
`X_sub_one_mul_crossingWeight`	theorem	Reciprocity/Defs.lean		N0529
`xChartFamily`	def	Surfaces/Lengths.lean
`xChartFamily_hasSubst`	theorem	Surfaces/Lengths.lean
`xChartSubst`	def	Surfaces/Lengths.lean
`xSubstUnit`	def	Surfaces/Lengths.lean
`zeroAffine`	def	Blowup/Directions.lean
`zeroCell`	def	Unramified/Extension.lean
`zeroDirection`	def	Blowup/Directions.lean