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		N315
`actual_cech_differentials_commute_with_reduction`	theorem	Blowup/Charts.lean		N318
`actual_cech_preserves_exceptional_lattices`	theorem	Blowup/Charts.lean		N316
`actual_cech_reductions_surjective`	theorem	Blowup/Charts.lean	Lemma 4.1, Appendix A	N317
`actual_finite_cech_coefficient_length`	theorem	Blowup/CechStability.lean	Lemma 4.2	N328
`actual_finite_cech_coefficient_triangular`	theorem	Blowup/CechStability.lean	Lemma 4.2	N329
`actual_negative_layer_coker_exact`	theorem	Blowup/TwoChartCurveData.lean		N324
`actual_negative_twist_kernel_zero`	theorem	Blowup/NilpotentGluing.lean		N323
`actual_twisted_coker_reduction_bijective`	theorem	Blowup/CechStability.lean	Lemma 4.1, Appendix A	N321
`adamsCoef`	def	Reciprocity/Defs.lean	(6.4)	N1145
`adamsCoef_adamsCoef`	theorem	Reciprocity/Quantum.lean
`adamsCoef_one`	theorem	Reciprocity/Quantum.lean
`adamsCoef_scalar`	theorem	Reciprocity/Quantum.lean
`adamsCoef_single`	theorem	Reciprocity/Quantum.lean
`adamsRat`	def	Reciprocity/Defs.lean		N1144
`adamsRat_adamsRat`	theorem	Reciprocity/Defs.lean
`adamsRat_one`	theorem	Reciprocity/Defs.lean
`adamsRat_recipRat`	theorem	Reciprocity/Defs.lean
`adamsRat_X`	theorem	Reciprocity/Defs.lean
`adamsRat_zpow_X`	theorem	Reciprocity/Defs.lean
`adamsSer`	def	Reciprocity/Defs.lean		N1146
`adamsSer_clusterSer_sub_one_scongr`	theorem	Reciprocity/Defs.lean
`adamsSer_logSer`	theorem	Reciprocity/Quantum.lean
`adamsSer_one`	theorem	Reciprocity/Defs.lean
`adamsSer_sub`	theorem	Reciprocity/Defs.lean
`adic_complete_iff_of_pow_le`	theorem	Unramified/Extension.lean		N513
`adic_congruence_rules`	theorem	Measure/AdicTransport.lean		N116
`adic_cylinders_intersection`	theorem	Measure/AdicTransport.lean		N129
`adic_perturb_bijective`	theorem	Measure/AdicTransport.lean		N122
`adic_perturb_congruence_iff`	theorem	Measure/AdicTransport.lean		N121
`adic_perturb_measurable`	theorem	Measure/AdicTransport.lean		N134
`adic_perturb_measure_preserving`	theorem	Measure/AdicTransport.lean		N135
`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		N544
`affine_divisor_count`	theorem	Assembly/TypeEvents.lean		N737
`affine_resultant_eq`	theorem	Measure/MemberCharts.lean
`affine_type_event_primitive_density`	theorem	Assembly/MonicCells.lean		N753
`affine_type_event_unit_scaling`	theorem	Assembly/TypeEvents.lean		N746
`AffineDirection`	abbrev	Blowup/Directions.lean
`AffineDivisor`	def	Assembly/NullBridges.lean
`affinePolynomial`	def	Basic.lean	Projective model	N008
`affineTypeEvent`	def	Assembly/NullBridges.lean
`algebra_product_congruence`	theorem	Measure/AdicCylinders.lean		N164
`algebra_type_algEquiv`	theorem	Algebra/AlgebraType.lean		N538
`algebra_type_children_exists`	theorem	Measure/Haar.lean		N437
`algebra_type_of_generic_fibre_equiv`	theorem	Algebra/AlgebraType.lean		N1095
`algebra_type_pi`	theorem	Algebra/AlgebraType.lean		N539
`algebra_type_unique`	theorem	Algebra/FactorInvariant.lean		N537
`algebra_type_unramified_descent`	theorem	Unramified/DescentTypes.lean	(6.4)	N543
`algebraMap_chart_eq_chartBase`	theorem	Blowup/NilpotentGluing.lean
`algebraMap_injective_of_tower`	theorem	Algebra/AlgebraType.lean
`Allowed`	def	Basic.lean	Allowed residue ideals, cells, occupied points, (4.7)–(4.8)	N005
`allowed_pattern_of_divisor`	theorem	Recursion/Termination.lean		N994
`allowed_pattern_of_divisor_unique`	theorem	Recursion/Members.lean		N998
`allowedPatterns`	def	Basic.lean		N005
`AllPoints`	abbrev	Blowup/Charts.lean
`array_enumeration`	theorem	Assembly/TypeEvents.lean		N728
`arrayLaw`	def	Assembly/NullBridges.lean
`availablePoints`	def	Basic.lean	(6.3)	N006
`axis_ideal_pow_mem_iff`	theorem	Surfaces/Lengths.lean		N670
`axis_pow_mul_mem_span_cancel`	theorem	Surfaces/Lengths.lean		N679
`axis_quotient_length_top`	theorem	Surfaces/Lengths.lean		N678
`axis_span_isPrime`	theorem	Surfaces/Lengths.lean		N677
`axisQuotientLength`	def	Surfaces/TruncatedSeries.lean
`axisQuotientLength_eq`	theorem	Surfaces/TruncatedSeries.lean
`axisQuotientLength_eq_iff`	theorem	Surfaces/TruncatedSeries.lean
`axisQuotientLength_eq_top`	theorem	Surfaces/TruncatedSeries.lean
`axisT`	def	Surfaces/Lengths.lean
`axisX`	def	Surfaces/Lengths.lean
`bad_exit_null`	theorem	Recursion/Events.lean	Proof of Theorem 6.2	N568
`base_ideal_coordinates`	theorem	Unramified/Extension.lean		N582
`base_ideal_maximal_local`	theorem	Unramified/FrobeniusDescent.lean		N587
`base_ideal_pure`	theorem	Unramified/Extension.lean		N583
`baseChange_bijective_of_finite_cokernel`	theorem	Recursion/Members.lean		N436
`baseChangeUnit`	def	Surfaces/Lengths.lean
`BaseField`	abbrev	Basic.lean		N008
`baseIdeal`	def	Unramified/Extension.lean
`baseReduce`	abbrev	Unramified/Extension.lean
`beta_right_chartBase`	theorem	Blowup/NilpotentGluing.lean
`beta_right_chartBase_self`	theorem	Blowup/CurveSections.lean
`binary_type_event_decomposition`	theorem	Assembly/TypeEvents.lean		N745
`binaryTypeEvent`	def	Assembly/NullBridges.lean
`binomial_series_ode`	theorem	Reciprocity/Defs.lean		N1183
`block_conjugates_coprime`	theorem	Unramified/FrobeniusDescent.lean		N937
`block_descent_bijection`	theorem	Unramified/FrobeniusDescent.lean	Lemma 7.1	N622
`block_descent_congruence_iff`	theorem	Unramified/FrobeniusDescent.lean		N623
`block_translation`	theorem	Unramified/PolynomialTypes.lean		N624
`block_translation_type_iff`	theorem	Formula/TypeTransport.lean		N713
`blockCell`	def	Unramified/Extension.lean
`blowup_chart_exceptional_point_polynomial`	theorem	Blowup/ExceptionalLayers.lean		N823
`blowup_chart_relation`	theorem	Blowup/Charts.lean		N156
`blowup_chart_ringHom_ext`	theorem	Blowup/Charts.lean		N760
`blowup_chart_universal`	theorem	Blowup/Charts.lean		N157
`blowup_exceptional_parameter_regular`	theorem	Blowup/Charts.lean		N258
`blowup_overlap_isLocalization_right`	theorem	Blowup/PointTransport.lean		N762
`BlowupChart`	abbrev	Blowup/Charts.lean
`blowupChart_concrete_isNoetherianRing`	theorem	Surfaces/Regularity.lean		N850
`BlowupOverlap`	abbrev	Blowup/Charts.lean
`blowupRelation`	def	Blowup/Charts.lean
`BlowupRestriction`	structure	Blowup/Charts.lean
`boundary_chart_quotient_equiv`	theorem	Blowup/Charts.lean		N889
`boundary_contact_length_ne_zero_iff`	theorem	Recursion/Members.lean		N991
`boundary_contact_of_twisted_generator`	theorem	Blowup/DivisorPoints.lean		N890
`boundaryDirections`	def	Blowup/Directions.lean
`card_mul_eq_zero_eq_card_quotient`	theorem	Surfaces/TruncatedSeries.lean
`card_pow_eq_sum_irreducible_degrees`	theorem	Surfaces/Lengths.lean	(6.2)	N682
`card_truncIndex_axis_segment`	theorem	Surfaces/TruncatedSeries.lean
`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		N1078
`cell_child_bijOn`	theorem	Recursion/RootCellLaw.lean		N1093
`cell_child_data_exists`	theorem	Recursion/ChildMembers.lean		N1083
`cell_child_mem_stateSet`	theorem	Recursion/Members.lean		N428
`cell_child_Phi_eq_map`	theorem	Recursion/OrderDefect.lean		N1099
`cell_datum_point_equiv`	theorem	Recursion/Members.lean		N1104
`cell_member_index_map`	theorem	Recursion/RootCellLaw.lean	Proposition 4.4	N1101
`cell_strict_transforms_agree_at_datum_points`	theorem	Blowup/StrictNormalizer.lean		N969
`cell_transport_preimage`	theorem	Formula/TypeTransport.lean		N701
`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
`cellMeasure_cell_inter`	theorem	Formula/TypeTransport.lean
`chart_cell_law_generic`	theorem	Recursion/Members.lean		N1120
`chart_child_completion_equiv`	theorem	Surfaces/ChartCompletions.lean		N860
`chart_child_completion_map_exists`	theorem	Surfaces/Regularity.lean		N856
`chart_child_completion_map_local`	theorem	Surfaces/Regularity.lean		N857
`chart_image_measurable_chart_sigma`	theorem	Measure/AdicTransport.lean		N404
`chart_layer_polynomial_coordinates`	theorem	Blowup/ExceptionalLayers.lean	(4.1)	N260
`chart_measure_total_mass`	theorem	Measure/HenselProducts.lean		N411
`chart_nonrational_point_span_eq_comap`	theorem	Surfaces/ChartCompletions.lean		N854
`chart_point_eq_directionPoint`	theorem	Blowup/ExceptionalLayers.lean		N955
`chart_point_isMaximal_of_residue_surjective`	theorem	Surfaces/Lengths.lean		N855
`chartBase`	def	Blowup/Charts.lean
`chartBase_apply_eq_algebraMap`	theorem	Surfaces/ConcreteAtlas.lean
`chartBase_x_eq`	theorem	Blowup/H0Comparison.lean
`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		N844
`chartSubst_surfaceRelation_base_change_and_x_chart`	theorem	Surfaces/Lengths.lean		N847
`chartSubst_surfaceRelation_origin_and_unit_point`	theorem	Surfaces/Lengths.lean		N846
`child_coordinate_map_scaled`	theorem	Blowup/Charts.lean		N394
`child_coordinate_preimage_measure`	theorem	Assembly/NullBridges.lean		N395
`child_degree_le`	theorem	Formula/LawAlgebra.lean		N051
`child_ideal_generator_transverse_finite`	theorem	Blowup/PointTransport.lean		N971
`child_ideal_set_map_iff_stateSet`	theorem	Recursion/Termination.lean		N1094
`child_ideals_curve_datum`	theorem	Blowup/DivisorPoints.lean	Lemma 4.3	N972
`child_order_equiv_linear`	theorem	Blowup/TwoChartCurveData.lean		N903
`child_order_index_and_kernel`	theorem	Measure/MemberCharts.lean	Proposition 4.4	N904
`child_series_eval_comp_chart_subst`	theorem	Surfaces/Regularity.lean		N859
`child_volume_ratio`	theorem	Measure/AdicCylinders.lean	Proposition 6.1	N074
`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)	N005
`children_degree_identity`	theorem	Formula/LawAlgebra.lean	(6.5)	N048
`children_residue_degree_pos`	theorem	Formula/LawAlgebra.lean		N050
`children_valid`	theorem	Formula/LawAlgebra.lean		N049
`chooseTwo`	def	Basic.lean		N006
`chooseTwo_add`	theorem	Reciprocity/Defs.lean
`ClosedDirection`	abbrev	Blowup/Directions.lean
`closure_finite_ascent`	theorem	Algebra/AlgebraType.lean
`closure_finite_ascent_root`	theorem	Algebra/AlgebraType.lean
`closure_finite_descent`	theorem	Algebra/AlgebraType.lean
`closure_finite_of_separable`	theorem	Algebra/AlgebraType.lean
`cluster_reciprocity`	theorem	Reciprocity/Main.lean	Proof of monic/cluster reciprocity, Theorem 9.3	N1316
`cluster_reciprocity_one`	theorem	Reciprocity/Patterns.lean	Proof of monic/cluster reciprocity	N1315
`cluster_reciprocity_step` private	theorem	Reciprocity/Main.lean	Proof of monic/cluster reciprocity
`clusterSer`	def	Reciprocity/Defs.lean	(7.5)	N1146
`clusterSer_eq_pPow`	theorem	Reciprocity/Plethysm.lean	(9.4)
`codilate`	def	Reciprocity/Defs.lean		N1146
`codilate_dilate`	theorem	Reciprocity/Quantum.lean
`codilate_pPow`	theorem	Reciprocity/Quantum.lean
`Coef`	abbrev	Reciprocity/Defs.lean	Type variables Z_{e,f}	N1145
`coeff_adamsSer`	theorem	Reciprocity/Defs.lean
`coeff_clusterSer_eq_coeff_qact`	theorem	Reciprocity/Main.lean	(S) = (7.11), (8.9), (9.4)	N1285
`coeff_codilate`	theorem	Reciprocity/Quantum.lean
`coeff_dilate`	theorem	Reciprocity/Quantum.lean
`coeff_euler_families_eq_patternSum`	theorem	Reciprocity/Plethysm.lean
`coeff_eulerSer`	theorem	Reciprocity/Patterns.lean	lem-7.2, (G) = (7.9)	N1220
`coeff_expSer_sub_of_scongr`	theorem	Reciprocity/Defs.lean
`coeff_formalPow`	theorem	Reciprocity/Plethysm.lean
`coeff_lawCoef`	theorem	Reciprocity/Plethysm.lean
`coeff_lawCoef_globalLaw_false`	theorem	Reciprocity/Patterns.lean
`coeff_lawCoef_globalLaw_true`	theorem	Reciprocity/Patterns.lean
`coeff_logSer_sub_of_scongr`	theorem	Reciprocity/Defs.lean
`coeff_one_clusterSer`	theorem	Reciprocity/Plethysm.lean
`coeff_one_dilate_recipSer_clusterSer`	theorem	Reciprocity/Plethysm.lean
`coeff_one_eulerSer_zero`	theorem	Reciprocity/Patterns.lean
`coeff_pPow_sub_of_scongr`	theorem	Reciprocity/Plethysm.lean	Pow_v and the first-difference rule	N1193
`coeff_qact_crossingQ_gaussPhi_eulerSer`	theorem	Reciprocity/Patterns.lean	(S) = (7.11)
`coeff_qact_gaussPhi`	theorem	Reciprocity/Defs.lean
`coeff_qact_gaussPhi_of_lt`	theorem	Reciprocity/Defs.lean	(8.10)
`coeff_recipCoef_lawCoef`	theorem	Reciprocity/Patterns.lean
`coeff_recipSer`	theorem	Reciprocity/Quantum.lean
`coeff_subst_eq_sum`	theorem	Reciprocity/Defs.lean
`coeff_substAlgHom_kill`	theorem	Surfaces/Lengths.lean
`coeff_succ_clusterSer`	theorem	Reciprocity/Plethysm.lean
`coeff_zero_clusterSer`	theorem	Reciprocity/Plethysm.lean
`coeff_zero_dilate_recipSer_clusterSer`	theorem	Reciprocity/Plethysm.lean
`coeff_zero_eulerSer`	theorem	Reciprocity/Plethysm.lean
`coefficient_cylinder_mass`	theorem	Measure/HenselProducts.lean		N104
`coefficient_measure_pi_one`	theorem	Recursion/Members.lean		N1086
`coefficient_measure_probability`	theorem	Measure/HenselProducts.lean		N219
`coefficient_space_strict_instances`	theorem	Blowup/Charts.lean		N402
`coefficient_uniformizer_cylinder_mass`	theorem	Measure/HenselProducts.lean		N220
`coefficientMeasure`	def	Basic.lean	Monic model	N008
`coefficientMeasure_zero_null`	theorem	Measure/MemberCharts.lean
`coeffVec`	def	Unramified/Extension.lean
`colored_subset_count`	theorem	Measure/AdicCylinders.lean		N082
`common_vertical_exponent`	theorem	Measure/AdicCylinders.lean		N1036
`commonKernel`	def	Blowup/Charts.lean
`commonLevelIdeal`	def	Blowup/Charts.lean
`commonMultiplicity`	def	Blowup/Charts.lean
`compact_injective_image_measure`	theorem	Measure/StateVolumes.lean		N237
`complete_domain_finite_quotient_local`	theorem	Unramified/Extension.lean		N175
`completed_point_power_contraction`	theorem	Blowup/Charts.lean		N285
`completed_point_transport_left`	theorem	Blowup/PointTransport.lean		N770
`completed_point_transport_right`	theorem	Blowup/PointTransport.lean		N771
`CompletedLocalAt`	abbrev	Blowup/Charts.lean
`completedPointMap`	def	Blowup/Charts.lean
`concrete_chart_point_span_form`	theorem	Surfaces/ConcretePoints.lean		N905
`concrete_crossing_state_atlas_exists`	theorem	Surfaces/ConcreteAtlas.lean		N424
`concrete_crossing_state_eq_union_cells`	theorem	Surfaces/Lengths.lean		N423
`concrete_crossing_state_volume`	theorem	Surfaces/ConcreteStrictTransforms.lean	Proposition 3.3	N425
`concrete_curve_order_index`	theorem	Measure/MemberCharts.lean	Proposition 4.4	N914
`concrete_index_map_reindexed`	theorem	Recursion/Termination.lean		N1098
`concrete_infinity_boundary_contact`	theorem	Blowup/NilpotentGluing.lean	(4.6)	N965
`concrete_infinity_point_completion`	theorem	Surfaces/ConcretePoints.lean		N909
`concrete_infinity_strict_transform_multiplicity`	theorem	Blowup/PointTransport.lean		N957
`concrete_infinity_strict_transform_transverse_finite`	theorem	Surfaces/ConcretePoints.lean		N838
`concrete_left_point_completion_instances`	theorem	Surfaces/ConcretePoints.lean		N907
`concrete_left_point_completion_is_surface`	theorem	Surfaces/ConcretePoints.lean		N906
`concrete_left_point_exceptional_regular`	theorem	Surfaces/ConcretePoints.lean		N908
`concrete_member_cell_measurable`	theorem	Recursion/Members.lean		N985
`concrete_member_cells_cover`	theorem	Recursion/RootCellLaw.lean	Proposition 6.1	N995
`concrete_member_cells_disjoint`	theorem	Recursion/ChildMembers.lean		N999
`concrete_member_charts`	theorem	Recursion/Members.lean		N979
`concrete_member_curve_order_free`	theorem	Recursion/Members.lean	Lemma 2.1	N1081
`concrete_member_data_exists`	theorem	Recursion/Members.lean		N977
`concrete_member_division_chart_measure`	theorem	Recursion/Members.lean		N1053
`concrete_member_division_module_isAdicComplete`	theorem	Recursion/Members.lean
`concrete_member_divisor_count`	theorem	Recursion/OrderDefect.lean		N984
`concrete_member_measure_finite_support`	theorem	Recursion/Members.lean		N1049
`concrete_member_mul_t_injective`	theorem	Recursion/Members.lean
`concrete_member_one_le_degree`	theorem	Recursion/Members.lean
`concrete_member_state_generator_contact_length`	theorem	Recursion/Members.lean		N1048
`concrete_member_state_generator_division`	theorem	Recursion/Members.lean		N1046
`concrete_member_state_generator_regular`	theorem	Recursion/Members.lean		N1045
`concrete_member_state_generator_transverse`	theorem	Recursion/Members.lean		N1047
`concrete_member_stateSet_measurable`	theorem	Recursion/Members.lean		N980
`concrete_member_terminal_type`	theorem	Recursion/ChildMembers.lean	Lemma 2.2	N1074
`concrete_member_volume`	theorem	Recursion/Termination.lean		N982
`concrete_residue_ideal_chart_exists`	theorem	Surfaces/ChartCompletions.lean		N420
`concrete_single_state_atlas_exists`	theorem	Surfaces/ConcreteAtlas.lean		N421
`concrete_single_state_eq_union_cells`	theorem	Surfaces/Lengths.lean		N419
`concrete_single_state_volume`	theorem	Surfaces/ConcreteStrictTransforms.lean	Proposition 3.3	N422
`concrete_strict_transform_generators`	theorem	Blowup/PointTransport.lean		N964
`concrete_strict_transform_multiplicity`	theorem	Blowup/StrictNormalizer.lean	(4.6)	N839
`concrete_strict_transform_residue_series`	theorem	Blowup/NilpotentGluing.lean		N1115
`concrete_strict_transform_transverse_finite`	theorem	Blowup/StrictNormalizer.lean		N837
`concrete_strict_transforms_are_prescribed`	theorem	Surfaces/ConcreteStrictTransforms.lean		N913
`concrete_surface_base_injective`	theorem	Surfaces/PowerSeries.lean		N490
`concrete_surface_contact_eq_special_fiber_contact`	theorem	Surfaces/Lengths.lean		N418
`concrete_surface_curve_basis`	theorem	Surfaces/Regularity.lean		N499
`concrete_surface_curve_free_of_length`	theorem	Surfaces/Regularity.lean	Lemma 2.1	N505
`concrete_surface_curve_isAdicComplete`	theorem	Surfaces/Completeness.lean		N495
`concrete_surface_data_exists_unconditional`	theorem	Surfaces/Regularity.lean		N879
`concrete_surface_equiv_curve_length_and_regular`	theorem	Surfaces/PowerSeries.lean		N878
`concrete_surface_equiv_instances`	theorem	Surfaces/Regularity.lean		N871
`concrete_surface_equiv_regular_pair`	theorem	Surfaces/Regularity.lean		N872
`concrete_surface_isAdicComplete_maximalIdeal`	theorem	Surfaces/Completeness.lean		N478
`concrete_surface_isAdicComplete_parameterIdeal`	theorem	Surfaces/Completeness.lean		N477
`concrete_surface_isAdicComplete_span_pi`	theorem	Surfaces/Completeness.lean		N480
`concrete_surface_isAdicComplete_span_pi_base`	theorem	Surfaces/Completeness.lean		N481
`concrete_surface_isDomain`	theorem	Surfaces/Regularity.lean		N466
`concrete_surface_isLocalRing`	theorem	Surfaces/PowerSeries.lean		N456
`concrete_surface_isNoetherianRing`	theorem	Surfaces/Lengths.lean		N457
`concrete_surface_isRegularLocalRing`	theorem	Surfaces/Regularity.lean		N487
`concrete_surface_maximalIdeal_eq`	theorem	Surfaces/PowerSeries.lean		N461
`concrete_surface_parameterIdeal_isMaximal`	theorem	Surfaces/PowerSeries.lean		N460
`concrete_surface_pi_regular`	theorem	Surfaces/PowerSeries.lean		N489
`concrete_surface_quotient_parameters_equiv`	theorem	Surfaces/PowerSeries.lean		N459
`concrete_surface_quotient_T_equiv`	theorem	Surfaces/Completeness.lean		N874
`concrete_surface_regular_pair_tx`	theorem	Surfaces/Regularity.lean		N453
`concrete_surface_regular_pair_xt`	theorem	Surfaces/Regularity.lean		N454
`concrete_surface_residue_regular_of_special_fiber`	theorem	Surfaces/Lengths.lean		N501
`concrete_surface_residueField_equiv`	theorem	Surfaces/PowerSeries.lean		N462
`concrete_surface_ringHom_ext_of_isNilpotent`	theorem	Surfaces/Completeness.lean		N848
`concrete_surface_ringKrullDim_eq_two`	theorem	Surfaces/Regularity.lean		N488
`concrete_surface_single_curve_free`	theorem	Blowup/StrictNormalizer.lean		N509
`concrete_surface_span_T_isPrime`	theorem	Surfaces/Completeness.lean		N465
`concrete_surface_spanFinrank_le_two`	theorem	Surfaces/PowerSeries.lean		N485
`concrete_surface_special_fiber_equiv`	theorem	Surfaces/PowerSeries.lean	Lemma 2.1	N471
`concrete_surface_special_fiber_equiv_parameters`	theorem	Surfaces/Lengths.lean		N472
`concrete_surface_special_fiber_length_transport`	theorem	Blowup/Charts.lean		N508
`concrete_surface_sub_constantCoeff_mem_parameterIdeal`	theorem	Surfaces/PowerSeries.lean		N849
`concrete_surface_vertical`	theorem	Surfaces/Lengths.lean		N491
`concrete_two_chart_glued_generators_exist`	theorem	Blowup/FixedTangentCellBijection.lean	Lemma 4.3	N912
`concrete_type_add_of_index_map`	theorem	Recursion/Members.lean		N1096
`concrete_universe_exists`	theorem	Recursion/RootCellLaw.lean	Theorem 6.2	N1108
`concrete_zero_boundary_contact`	theorem	Blowup/NilpotentGluing.lean	(4.6)	N966
`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		N213
`congruence_bijection_measure_preserving`	theorem	Measure/StateVolumes.lean		N214
`conjugate_roots_distinct`	theorem	Unramified/PolynomialTypes.lean		N616
`conjugateFactor`	def	Unramified/Extension.lean
`conjugateProduct`	def	Unramified/Extension.lean
`constantCoeff_adamsSer`	theorem	Reciprocity/Defs.lean
`constantCoeff_clusterSer`	theorem	Reciprocity/Plethysm.lean
`constantCoeff_eulerSer`	theorem	Reciprocity/Plethysm.lean
`constantCoeff_expSer`	theorem	Reciprocity/Defs.lean
`constantCoeff_logSer`	theorem	Reciprocity/Defs.lean
`constantCoeff_moebiusSum`	theorem	Reciprocity/Quantum.lean
`constantCoeff_plethSum`	theorem	Reciprocity/Quantum.lean
`constantCoeff_pPow`	theorem	Reciprocity/Plethysm.lean
`contact`	def	Surfaces/Lengths.lean
`contact_fiberT_eq_axisQuotientLength`	theorem	Surfaces/TruncatedSeries.lean
`contact_fiberX_eq_axisQuotientLength`	theorem	Surfaces/TruncatedSeries.lean
`continuousOn_of_congruence_compatible`	theorem	Formula/PatternCounts.lean		N705
`contracted_ideal_map_localization_top`	theorem	Blowup/Charts.lean		N765
`contractedLocalCurveIdeal`	def	Blowup/Charts.lean
`coordinate_constraint_count`	theorem	Measure/AdicCylinders.lean		N061
`coordinate_coset_representatives_exist`	theorem	Blowup/Charts.lean		N401
`coordinate_cylinder_clopen`	theorem	Formula/LawAlgebra.lean		N703
`coordinate_hyperplane_null`	theorem	Formula/TypeTransport.lean	Discriminant locus is null	N704
`coordinate_ideal_cell_bijection`	theorem	Measure/Atlas.lean	Proposition 3.2	N208
`coordinate_ideal_in_residue_cell`	theorem	Measure/AdicCylinders.lean		N205
`coordinate_ideal_injective`	theorem	Measure/Normalizer.lean		N207
`coordinate_ideal_measurable_chart_sigma`	theorem	Surfaces/ConcreteStrictTransforms.lean		N417
`coordinate_ideal_measurableEmbedding`	theorem	Recursion/Members.lean		N1050
`coordinate_module_pi_quotient_length`	theorem	Measure/AdicCylinders.lean		N1042
`coordinate_remainder_raises_order`	theorem	Measure/AdicCylinders.lean		N165
`coordinate_scale_measure`	theorem	Blowup/StrictNormalizer.lean		N393
`coordinate_transition_congruence`	theorem	Measure/Normalizer.lean	Lemma 3.1	N210
`coordinateCoset`	def	Blowup/Charts.lean
`coordinateIdeal`	def	Measure/AdicCylinders.lean
`coordinateLift`	def	Measure/AdicCylinders.lean
`coordinateLift_smul_eq_mul`	theorem	Measure/AdicCylinders.lean
`coordinateLinear`	def	Blowup/Charts.lean
`coordinateRemainder`	def	Measure/AdicCylinders.lean
`coordinateScale`	def	Blowup/Charts.lean
`coprime_family_linear_injective`	theorem	Unramified/Extension.lean		N603
`coprime_family_type_iff`	theorem	Formula/TypeTransport.lean		N708
`coprime_of_coprime_residue_dvr`	theorem	Unramified/Extension.lean		N931
`coprime_of_monic_reduction_one`	theorem	Formula/LawAlgebra.lean		N711
`count_normalizedFactors_divisorAffinePolynomial`	theorem	Blowup/Directions.lean		N954
`countSum`	def	Reciprocity/Defs.lean		N1146
`crossing_residue_ideal_count`	theorem	Measure/Normalizer.lean	Proposition 3.3	N071
`crossing_special_fiber_length`	theorem	Unramified/LocalDescent.lean	Lemma 2.1	N064
`crossing_state_volume`	theorem	Measure/Normalizer.lean	Proposition 3.3	N415
`crossingQ`	def	Reciprocity/Defs.lean	(7.5), (8.2)	N1147
`crossingQ_eq_qmul_qplus_qdiag_qminus`	theorem	Reciprocity/Patterns.lean	(T) = (7.12), Lemma 8.2	N1281
`crossingQ_symm`	theorem	Reciprocity/Patterns.lean	(H) = (7.4)	N1276
`crossingQ_zero_zero`	theorem	Reciprocity/Patterns.lean
`crossingResidueIdeals`	def	Surfaces/Lengths.lean	Allowed residue ideals, cells, occupied points
`curve_datum_of_parent_function`	theorem	Surfaces/ConcreteAtlas.lean		N919
`curve_datum_surj_and_inf_clauses`	theorem	Blowup/NilpotentGluing.lean		N959
`curve_ideal_lattice_eq_kernels`	theorem	Blowup/CurveOrders.lean		N810
`curve_ideal_lattice_le_sections`	theorem	Blowup/CurveOrders.lean		N364
`curve_lattices_antitone`	theorem	Blowup/CurveOrders.lean		N801
`curve_limit_equiv_product_threads`	theorem	Blowup/TwoChartCurveData.lean		N812
`curve_limit_level_map_exists`	theorem	Blowup/CurveOrders.lean		N803
`curve_limit_level_map_surjective`	theorem	Blowup/CurveSections.lean	Lemma 4.1	N807
`curve_limit_range_of_stable_level`	theorem	Blowup/CechStability.lean		N808
`curve_quotient_complete_equiv_threads`	theorem	Blowup/CurveOrders.lean		N813
`curve_section_connecting_class_zero_iff`	theorem	Blowup/H0Comparison.lean		N368
`curve_sections_connecting_map_exists`	theorem	Recursion/Members.lean		N1119
`curve_sections_cover_overlap`	theorem	Blowup/CurveSections.lean		N365
`curve_sections_quot_equiv_product`	theorem	Blowup/TwoChartCurveData.lean		N811
`curve_sections_quot_reduction_exists`	theorem	Blowup/CurveOrders.lean		N802
`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		N553
`densityValue`	abbrev	Basic.lean		N010
`derivative_expSer`	theorem	Reciprocity/Defs.lean
`descend_block_mem_cell`	theorem	Unramified/FrobeniusDescent.lean		N621
`descendBlock`	def	Unramified/Extension.lean
`descendCoeff`	def	Unramified/Extension.lean
`descended_block_type_iff`	theorem	Assembly/TypeEvents.lean		N714
`descended_polynomial_type`	theorem	Unramified/DescentTypes.lean	Lemma 7.1	N936
`digitIter`	def	Measure/AdicCylinders.lean
`dilate`	def	Reciprocity/Defs.lean		N1146
`dilate_codilate`	theorem	Reciprocity/Quantum.lean
`dilate_mul`	theorem	Reciprocity/Quantum.lean
`dilate_pPow`	theorem	Reciprocity/Quantum.lean	(7.6)
`dilate_recipSer_eulerSer_eq_pPow`	theorem	Reciprocity/Plethysm.lean
`dilate_recipSer_eulerSer_mul_scongr_one`	theorem	Reciprocity/Plethysm.lean
`direction_child_member_exists`	theorem	Recursion/ChildMembers.lean		N1082
`direction_point_maximal`	theorem	Blowup/ExceptionalLayers.lean		N882
`direction_point_overlap_maximal`	theorem	Blowup/ExceptionalLayers.lean		N883
`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		N956
`discAffine`	def	Measure/MemberCharts.lean
`distinct_monic_irreducible_coprime`	theorem	Unramified/Extension.lean		N524
`division_chart_preimage_image_measurable`	theorem	Measure/Atlas.lean		N1112
`division_chart_rank_eq_of_residue_ideal_eq`	theorem	Measure/AdicCylinders.lean		N1110
`division_chart_same_cell_recenter`	theorem	Measure/AdicCylinders.lean		N1111
`division_coordinate_module_isAdicComplete`	theorem	Surfaces/Completeness.lean		N484
`division_data_same_cell_recenter`	theorem	Measure/AdicCylinders.lean		N1125
`division_data_vertical_perturbation`	theorem	Recursion/Termination.lean		N1051
`division_equiv_child_coordinates`	theorem	Blowup/CurveOrders.lean		N386
`division_linear_equivalence`	theorem	Measure/AdicCylinders.lean	Lemma 3.1	N163
`division_quotient_basis_equiv`	theorem	Recursion/Termination.lean		N1052
`divisionMap`	def	Measure/AdicCylinders.lean
`divisor_affine_polynomial_normalized_factors`	theorem	Recursion/Termination.lean		N996
`divisor_array_exists_unique`	theorem	Assembly/TypeEvents.lean		N735
`divisor_count_eval_of_point_count`	theorem	Assembly/TypeEvents.lean
`divisor_count_of_point_set`	theorem	Assembly/TypeEvents.lean		N736
`divisor_count_safe`	theorem	Formula/LawAlgebra.lean		N077
`divisor_form_cell_law`	theorem	Assembly/MonicCells.lean		N751
`divisor_probability_pos`	theorem	Formula/StateCombinatorics.lean		N722
`divisor_probability_safe`	theorem	Formula/LawAlgebra.lean		N076
`divisor_vector_properties`	theorem	Assembly/TypeEvents.lean		N742
`divisorAffinePolynomial`	def	Blowup/Directions.lean
`divisorBoundary`	def	Blowup/Charts.lean
`DivisorContactCondition`	abbrev	Recursion/Termination.lean
`divisorCount`	def	Basic.lean	(6.3)	N006
`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	N006
`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		N518
`dvr_extension_maximalIdeal_map_eq_pow`	theorem	Unramified/Extension.lean		N512
`dvr_isAdicComplete_span_uniformizer`	theorem	Surfaces/Lengths.lean		N483
`dvr_maximalIdeal_pow_injective`	theorem	Unramified/Extension.lean		N511
`eminusOne`	def	Basic.lean		N006
`eq_of_mul_derivative_eq_mul`	theorem	Reciprocity/Plethysm.lean
`eq_zero_of_scalar_mul_eq_zero`	theorem	Reciprocity/Quantum.lean
`equiv_of_fiber_card_eq`	theorem	Recursion/Termination.lean		N1077
`etale_invariant_children`	theorem	Recursion/OrderDefect.lean		N698
`etale_type_event_eq_term`	theorem	Recursion/Termination.lean		N430
`etale_type_event_measurable`	theorem	Recursion/Events.lean		N431
`eulerSer`	def	Reciprocity/Defs.lean	lem-7.2, (7.10)	N1146
`eval_at_pow_card`	theorem	Unramified/Extension.lean		N591
`eval₂_C_X_eq_algebraMap`	theorem	Reciprocity/Defs.lean
`exceptional_chart_is_affine_line`	theorem	Blowup/CurveOrders.lean		N248
`exceptional_line_equiv_chart_exceptional`	theorem	Blowup/CurveOrders.lean		N822
`exceptional_line_equiv_residue_field`	theorem	Blowup/CurveOrders.lean		N880
`exceptional_overlap_is_laurent_line`	theorem	Blowup/CurveOrders.lean		N249
`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
`exists_separable_monic`	theorem	Measure/MemberCharts.lean
`exists_unique_selfPattern_single`	theorem	Reciprocity/Plethysm.lean	(6.6)
`exists_unramified_lift`	theorem	Formula/TypeTransport.lean		N716
`exit_cell_coeff_nonneg`	theorem	Recursion/Events.lean
`exit_cell_type_mass`	theorem	Recursion/Events.lean		N563
`exit_event_succ_mass`	theorem	Recursion/Events.lean	Proof of Theorem 6.2	N566
`exit_event_zero_mass`	theorem	Recursion/Events.lean		N564
`exitLaw`	def	Formula/StateCombinatorics.lean	(6.6)
`Expr`	inductive	Basic.lean	Type variables Z_{e,f}	N003
`Expr.allSafe`	def	Basic.lean		N003
`Expr.eval`	def	Basic.lean		N003
`Expr.fraction`	def	Basic.lean		N003
`Expr.fraction_snd_ne_zero`	theorem	Reciprocity/Plethysm.lean
`Expr.neg`	def	Basic.lean		N003
`Expr.pow`	def	Basic.lean		N003
`Expr.prod`	def	Basic.lean		N003
`Expr.rational`	def	Basic.lean		N003
`Expr.rational_add`	theorem	Reciprocity/Plethysm.lean
`Expr.rational_const`	theorem	Reciprocity/Plethysm.lean
`Expr.rational_inv`	theorem	Reciprocity/Plethysm.lean
`Expr.rational_mul`	theorem	Reciprocity/Plethysm.lean
`Expr.rational_pow`	theorem	Reciprocity/Plethysm.lean
`Expr.rational_sub`	theorem	Reciprocity/Plethysm.lean
`Expr.rational_sum`	theorem	Reciprocity/Plethysm.lean
`Expr.rational_var`	theorem	Reciprocity/Plethysm.lean
`Expr.safe`	def	Basic.lean		N003
`Expr.sub`	def	Basic.lean		N003
`Expr.subst`	def	Basic.lean		N003
`Expr.sum`	def	Basic.lean		N003
`Expr.wf`	def	Reciprocity/Defs.lean		N1144
`Expr.wf_pow`	theorem	Reciprocity/Plethysm.lean
`expression_fraction`	theorem	Formula/LawAlgebra.lean		N030
`expression_pow_eval`	theorem	Formula/LawAlgebra.lean		N034
`expression_pow_safe`	theorem	Formula/LawAlgebra.lean		N035
`expression_prod_eval`	theorem	Formula/LawAlgebra.lean		N037
`expression_regular`	theorem	Formula/LawAlgebra.lean		N031
`expression_sum_eval`	theorem	Formula/LawAlgebra.lean		N036
`expression_sum_safe`	theorem	Formula/LawAlgebra.lean		N038
`expSer`	def	Reciprocity/Defs.lean		N1146
`expSer_add`	theorem	Reciprocity/Plethysm.lean		N1178
`expSer_logSer`	theorem	Reciprocity/Plethysm.lean	(7.6)	N1180
`expSer_zero`	theorem	Reciprocity/Defs.lean
`factor_cell_product_measure`	theorem	Unramified/PolynomialTypes.lean		N613
`factor_cells_measure_preserving`	theorem	Unramified/HomogeneousCells.lean	Lemma 7.1	N614
`factor_invariant_algEquiv`	theorem	Algebra/FactorInvariant.lean		N519
`factor_invariant_unramified_scale`	theorem	Unramified/DescentTypes.lean		N935
`factor_product_bijection`	theorem	Unramified/FactorCells.lean		N610
`factor_product_congruence_iff`	theorem	Unramified/PolynomialTypes.lean		N611
`factor_product_continuous`	theorem	Unramified/Extension.lean		N612
`factorInvariant`	def	Basic.lean	Monic model	N008
`factorProduct`	def	Unramified/Extension.lean
`FactorType`	abbrev	Basic.lean	Type of degree n	N001
`falling`	def	Basic.lean	(6.3)	N006
`fiberT`	def	Surfaces/Lengths.lean
`fiberX`	def	Surfaces/Lengths.lean
`field_invariant_algEquiv`	theorem	Algebra/FactorInvariant.lean		N534
`field_invariant_unramified_tower`	theorem	Unramified/DescentTypes.lean	(6.4)	N541
`fieldInvariant`	def	Algebra/AlgebraType.lean	Reduced-algebra type convention
`finite_colength_completion_ideal_descent`	theorem	Unramified/LocalDescent.lean		N277
`finite_completed_point_quotient_surjective`	theorem	Unramified/LocalDescent.lean		N282
`finite_coordinate_adic_congruence`	theorem	Measure/AdicCylinders.lean		N216
`finite_coordinate_borel_cylinders`	theorem	Measure/AdicCylinders.lean		N218
`finite_coordinate_cylinder_basis`	theorem	Measure/AdicCylinders.lean		N217
`finite_coordinate_linear_continuous`	theorem	Measure/AdicCylinders.lean		N238
`finite_curve_support_kernel_saturated`	theorem	Blowup/CurveOrders.lean		N294
`finite_field_card_primePower`	theorem	Formula/FiniteFieldCounts.lean		N1124
`finite_field_frobenius_fixed_points`	theorem	Unramified/Extension.lean		N590
`finite_field_irreducible_count`	theorem	Formula/FiniteFieldCounts.lean	(6.2)	N081
`finite_flat_local_ramification_degree`	theorem	Formula/LawAlgebra.lean		N251
`finite_free_adic_complete`	theorem	Unramified/Extension.lean		N169
`finite_free_residue_quotient`	theorem	Unramified/Extension.lean		N170
`finite_length_module_card`	theorem	Formula/FiniteFieldCounts.lean		N389
`finite_measures_from_cylinders`	theorem	Measure/AdicTransport.lean		N132
`finite_module_length_card`	theorem	Measure/Normalizer.lean		N1039
`finite_quotient_event_mass`	theorem	Measure/AdicTransport.lean		N131
`finite_quotient_fiber_mass`	theorem	Measure/AdicTransport.lean		N130
`finite_support_completion_recovers`	theorem	Blowup/CurveOrders.lean		N289
`finite_support_generators_compatible`	theorem	Blowup/CurveOrders.lean		N372
`finite_support_kernel_localize`	theorem	Blowup/PointTransport.lean		N766
`finite_support_level_generator_regular`	theorem	Blowup/NilpotentGluing.lean		N780
`finite_support_level_kernels_principal`	theorem	Blowup/NilpotentGluing.lean		N786
`finite_support_quotient_equiv`	theorem	Blowup/CurveOrders.lean	Lemma 4.3	N287
`finite_support_quotient_surjective`	theorem	Blowup/CurveOrders.lean		N286
`finite_support_quotient_surjective_of_isPrime`	theorem	Blowup/CurveOrders.lean
`finite_types_of_degree`	theorem	Formula/LawAlgebra.lean		N018
`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		N406
`fixed_tangent_cell_chart_partition`	theorem	Blowup/H0Comparison.lean		N400
`fixed_tangent_cell_curve_datum`	theorem	Blowup/DivisorPoints.lean		N961
`fixed_tangent_cell_generator_coefficients`	theorem	Blowup/PointTransport.lean		N952
`fixedTangentCell`	def	Blowup/Charts.lean
`form_cell_monic_identification`	theorem	Unramified/HomogeneousCells.lean		N947
`form_cell_product_measure`	theorem	Unramified/FactorCells.lean		N945
`form_cells_measure_preserving`	theorem	Unramified/HomogeneousCells.lean	Lemma 7.1	N946
`form_product_bijection`	theorem	Unramified/PolynomialTypes.lean		N943
`form_product_congruence_reflects`	theorem	Unramified/PolynomialTypes.lean		N941
`form_product_maps_to_and_preserves`	theorem	Unramified/Extension.lean		N940
`form_product_measurable`	theorem	Unramified/HomogeneousCells.lean		N944
`form_product_type_event_law`	theorem	Assembly/TypeEvents.lean		N750
`formalPow`	def	Reciprocity/Defs.lean		N1146
`formPoly`	def	Unramified/Extension.lean
`formPoly_add`	theorem	Unramified/Extension.lean
`formPoly_natDegree_le`	theorem	Assembly/TypeEvents.lean
`formProd`	def	Unramified/Extension.lean
`forms_linear_bijective`	theorem	Unramified/Extension.lean		N636
`forms_linear_injective`	theorem	Unramified/Extension.lean		N635
`FormsCoprime`	def	Unramified/Extension.lean
`FormulaRegular`	def	Basic.lean		N010
`frobenius_fixed_ring`	theorem	Unramified/FrobeniusDescent.lean	Standard facts	N599
`frobenius_fraction_extension`	theorem	Unramified/DescentTypes.lean		N930
`frobenius_pow_degree_eq_id`	theorem	Unramified/FrobeniusDescent.lean		N597
`frobeniusIter`	def	Unramified/Extension.lean
`frobeniusRoot`	def	Unramified/Extension.lean
`full_rank_free_submodule_finite_length`	theorem	Recursion/Termination.lean		N688
`fullCechDifferential`	def	Blowup/Charts.lean
`gaussPhi`	def	Reciprocity/Defs.lean	(7.10)	N1147
`gaussPhi_dilate`	theorem	Reciprocity/Quantum.lean
`gaussPhi_dilate_recipSer_clusterSer` private	theorem	Reciprocity/Main.lean	(9.4)
`gaussPhi_qactRecip_gaussPhiInv`	theorem	Reciprocity/Quantum.lean	Lemma 9.1	N1255
`gaussPhi_sub`	theorem	Reciprocity/Quantum.lean
`gaussPhiInv`	def	Reciprocity/Defs.lean		N1147
`generatorNormalForm`	def	Measure/AdicCylinders.lean
`generic_closure_free_of_type`	theorem	Recursion/Termination.lean		N689
`GenericClosure`	def	Algebra/AlgebraType.lean
`genericClosureVal`	def	Algebra/AlgebraType.lean
`geometric_exit_sum`	theorem	Formula/LawAlgebra.lean	Proof of Theorem 6.2	N028
`global_coefficients_safe`	theorem	Formula/StateCombinatorics.lean		N058
`global_formula_regular`	theorem	Formula/StateCombinatorics.lean	Theorem 1.1, Theorem 6.2	N060
`global_function_has_tangent_divisor`	theorem	Blowup/DivisorPoints.lean		N887
`global_function_mem_cell`	theorem	Blowup/DivisorPoints.lean		N973
`global_function_of_two_chart_curve_data`	theorem	Recursion/Termination.lean		N790
`global_function_strict_transform_at_right_point`	theorem	Blowup/TwoChartCurveData.lean		N893
`global_law_safe`	theorem	Formula/StateCombinatorics.lean		N057
`global_rational_eval`	theorem	Formula/RationalEval.lean		N1123
`globalLaw`	def	Basic.lean	(1.5), (7.3)	N007
`glued_function_exists_unique`	theorem	Blowup/H0Comparison.lean	Lemma 4.2	N351
`glued_function_initial_form`	theorem	Blowup/H0Comparison.lean		N355
`glued_function_left_chart`	theorem	Blowup/CurveOrders.lean		N352
`glued_function_order`	theorem	Blowup/H0Comparison.lean		N354
`glued_function_pair_closed`	theorem	Blowup/CurveOrders.lean		N349
`glued_function_pair_compatible`	theorem	Blowup/CurveOrders.lean		N350
`glued_function_right_chart`	theorem	Blowup/CurveOrders.lean		N353
`glued_generators_exist`	theorem	Blowup/CurveSections.lean	Lemma 4.3	N361
`glued_generators_level_one`	theorem	Blowup/CurveOrders.lean		N1113
`glued_generators_of_two_chart_curve_data`	theorem	Blowup/TwoChartCurveData.lean		N789
`glued_level_one_normalization`	theorem	Blowup/ExceptionalLayers.lean		N785
`gluedFunctionPair`	def	Blowup/Charts.lean
`GluedGenerators`	structure	Blowup/Charts.lean
`has_multiplicity_initial_form`	theorem	Recursion/Termination.lean		N987
`has_tangent_divisor_multiplicity`	theorem	Blowup/H0Comparison.lean		N898
`HasAlgebraType`	def	Algebra/AlgebraType.lean	Reduced-algebra type convention
`HasArray`	def	Assembly/NullBridges.lean
`HasBinaryType`	def	Basic.lean	Projective model	N008
`HasBinaryTypeF`	def	Basic.lean
`HasHomogeneousDivisor`	def	Blowup/Directions.lean
`HasMultiplicity`	def	Surfaces/Lengths.lean
`HasPattern`	def	Blowup/Directions.lean
`HasPolynomialType`	def	Basic.lean	Monic model	N008
`HasPolynomialTypeF`	def	Basic.lean	Remark 1.3, Reduced-algebra type convention, Remark 6.3
`HasPolynomialTypeF.to_original`	theorem	Algebra/AlgebraType.lean
`hasPolynomialTypeF_iff_of_separable`	theorem	Algebra/AlgebraType.lean
`HasTangentDivisor`	def	Blowup/Charts.lean	Allowed residue ideals, cells, occupied points, (4.6)
`hensel_factor_unique_of_dvd`	theorem	Unramified/Extension.lean		N618
`hensel_family_exists`	theorem	Measure/HenselProducts.lean		N102
`hensel_family_unique`	theorem	Unramified/Extension.lean		N602
`hensel_family_unique_mod_pow`	theorem	Unramified/PolynomialTypes.lean		N607
`hensel_pair_exists`	theorem	Measure/HenselProducts.lean		N100
`hensel_pair_unique`	theorem	Measure/HenselProducts.lean		N101
`homogeneous_divisor_boundary_multiplicities`	theorem	Recursion/Termination.lean	(4.6)	N989
`homogeneous_divisor_of_polynomial`	theorem	Recursion/Termination.lean		N988
`homogeneous_form_not_mem_pow_succ`	theorem	Blowup/CurveOrders.lean		N897
`ideal_chart_pushforward_independent`	theorem	Measure/Atlas.lean	Proposition 3.2	N222
`ideal_chart_transition_haar`	theorem	Measure/Atlas.lean	Proposition 3.2	N221
`ideal_closed_noetherian_local`	theorem	Surfaces/Lengths.lean		N373
`ideal_contact_generator`	theorem	Blowup/CurveOrders.lean		N190
`IdealAtlas`	structure	Measure/AdicCylinders.lean
`IdealChart`	structure	Measure/AdicCylinders.lean	Proposition 3.2
`IdealChart.isDivisionChart`	theorem	Measure/AdicCylinders.lean
`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		N474
`image_measurable_of_continuousOn_injOn_compact`	theorem	Formula/LawAlgebra.lean		N702
`inertiaDeg_unramified_tower`	theorem	Unramified/FrobeniusDescent.lean		N522
`infinity_block_event_law`	theorem	Assembly/MonicCells.lean		N747
`infinity_point_child_member`	theorem	Recursion/Termination.lean		N1088
`infinity_point_maximal`	theorem	Blowup/ExceptionalLayers.lean		N884
`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)	N990
`initial_form_lift_independent`	theorem	Blowup/H0Comparison.lean		N196
`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		N515
`integral_closure_finite_free`	theorem	Algebra/AlgebraType.lean	Standard facts	N176
`integral_closure_invariants_degree`	theorem	Algebra/AlgebraType.lean		N252
`integral_closure_is_dedekind`	theorem	Algebra/AlgebraType.lean		N180
`integral_closure_is_dvr`	theorem	Measure/PrimitiveLocus.lean	Standard facts	N182
`integral_closure_is_local`	theorem	Measure/PrimitiveLocus.lean		N179
`integral_closure_not_field`	theorem	Algebra/AlgebraType.lean		N181
`integral_closure_own_adic_complete`	theorem	Measure/PrimitiveLocus.lean		N514
`integral_local_extension_unique_prime`	theorem	Formula/LawAlgebra.lean		N250
`integralClosureTowerEquiv`	def	Algebra/AlgebraType.lean
`invariant_orbit_factors`	theorem	Unramified/Extension.lean		N933
`invSelf_pow_eq_selfZPow`	theorem	Blowup/NilpotentGluing.lean
`irreducible_count_moebius`	theorem	Surfaces/Lengths.lean	(6.2)	N683
`isAdicComplete_of_isAdicComplete_maximalIdeal`	theorem	Surfaces/Lengths.lean		N479
`isAdicComplete_pi`	theorem	Measure/HenselProducts.lean		N1034
`isAdicComplete_prod`	theorem	Surfaces/Lengths.lean		N482
`isAdicComplete_quotient_of_iInf_sup_pow`	theorem	Surfaces/Lengths.lean		N473
`isCoprime_of_isCoprime_map_residue`	theorem	Measure/HenselProducts.lean
`IsDivisionChart`	def	Measure/AdicCylinders.lean
`isDomain_of_regular_prime_element`	theorem	Surfaces/Lengths.lean		N463
`isUnit_mk_truncIdeal_iff`	theorem	Surfaces/TruncatedSeries.lean
`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		N783
`laurent_nonnegative_twist_kernel`	theorem	Blowup/ExceptionalLayers.lean		N342
`laurent_split_nonnegative_twist`	theorem	Blowup/ExceptionalLayers.lean		N299
`Law`	abbrev	Basic.lean	Type variables Z_{e,f}	N004
`law_coeff_descend`	theorem	Formula/LawAlgebra.lean		N548
`law_coeff_flatMap`	theorem	Formula/LawAlgebra.lean		N547
`law_coeff_mul`	theorem	Formula/LawAlgebra.lean		N549
`law_coeff_nonneg_closure`	theorem	Formula/LawAlgebra.lean		N724
`law_coeff_prod_descend`	theorem	Formula/LawAlgebra.lean		N550
`law_coeff_prod_formula`	theorem	Formula/LawAlgebra.lean		N729
`law_coeff_scale`	theorem	Formula/LawAlgebra.lean		N042
`law_safe_descend`	theorem	Formula/LawAlgebra.lean		N045
`law_safe_mul`	theorem	Formula/LawAlgebra.lean		N044
`law_safe_scale`	theorem	Formula/LawAlgebra.lean		N043
`lawAtom`	def	Basic.lean		N004
`lawCoef`	def	Reciprocity/Defs.lean	Type variables Z_{e,f}	N1145
`lawCoef_flatMap`	theorem	Reciprocity/Plethysm.lean
`lawCoef_globalLaw_false`	theorem	Reciprocity/Patterns.lean	(G) = (7.9)
`lawCoef_globalLaw_false_eq_recipCoef`	theorem	Reciprocity/Main.lean	Theorem 1.2, Lemma 9.2	N1317
`lawCoef_globalLaw_true`	theorem	Reciprocity/Patterns.lean	(G) = (7.9)
`lawCoef_lawProd`	theorem	Reciprocity/Plethysm.lean
`lawCoef_lawScale`	theorem	Reciprocity/Plethysm.lean
`lawCoef_nil`	theorem	Reciprocity/Plethysm.lean
`lawCoef_single_self_term`	theorem	Reciprocity/Patterns.lean	(S) = (7.11)
`lawCoef_single_term`	theorem	Reciprocity/Patterns.lean
`lawCoeff`	def	Basic.lean	Type variables Z_{e,f}	N004
`lawDescend`	def	Basic.lean	(6.4)	N004
`lawInterp`	def	Formula/LawAlgebra.lean
`lawInterp_append`	theorem	Formula/LawAlgebra.lean
`lawInterp_coeff`	theorem	Formula/LawAlgebra.lean
`lawInterp_flatMap`	theorem	Formula/LawAlgebra.lean
`lawInterp_lawMul`	theorem	Formula/LawAlgebra.lean
`lawInterp_lawProd`	theorem	Formula/LawAlgebra.lean
`lawInterp_lawScale`	theorem	Formula/LawAlgebra.lean
`lawInterp_nil`	theorem	Formula/LawAlgebra.lean
`lawMul`	def	Basic.lean	Type variables Z_{e,f}	N004
`lawOne`	def	Basic.lean		N004
`lawProd`	def	Basic.lean		N004
`LawSafe`	def	Basic.lean		N004
`LawSafe.lawWf`	theorem	Reciprocity/Plethysm.lean
`lawScale`	def	Basic.lean		N004
`LawWf`	def	Reciprocity/Defs.lean		N1145
`LawWf.wf_lawCoeff`	theorem	Reciprocity/Plethysm.lean
`lawWf_globalLaw`	theorem	Reciprocity/Patterns.lean
`lawWf_stateLaw`	theorem	Reciprocity/Patterns.lean
`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		N676
`length_quotient_sup_mul_eq_add`	theorem	Surfaces/Lengths.lean		N674
`length_quotient_sup_pow_eq_mul`	theorem	Surfaces/Lengths.lean		N675
`length_scaling_of_residue_card`	theorem	Measure/Normalizer.lean		N1040
`level_one_kernel_polynomial`	theorem	Blowup/DivisorPoints.lean
`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		N136
`linear_image_bound_from_cokernel_length`	theorem	Measure/HenselProducts.lean		N240
`linear_map_preserves_adic_congruence`	theorem	Measure/HenselProducts.lean		N199
`list_get_fiber_card`	theorem	Formula/LawAlgebra.lean		N726
`list_get_fiber_card_count`	theorem	Recursion/Termination.lean		N1075
`local_algEquiv_maximalIdeal`	theorem	Unramified/Extension.lean		N517
`local_completion_finite_quotient`	theorem	Unramified/LocalDescent.lean		N276
`local_law_safe`	theorem	Formula/StateCombinatorics.lean	Theorem 6.2	N056
`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		N262
`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		N1146
`logSer_expSer`	theorem	Reciprocity/Plethysm.lean	(7.6)
`main_dvr`	theorem	Main.lean	Theorem 1.1, Remark 1.3
`main_field_form`	theorem	Main.lean	Theorem 1.1	N660
`main_field_form_ramified`	theorem	Main.lean	Theorem 1.1
`map_maximalIdeal_localCompletion`	theorem	Blowup/CurveSections.lean
`map_maximalIdeal_localCompletion_comap_le`	theorem	Blowup/CurveSections.lean
`map_maximalIdeal_localCompletion_transport`	theorem	Blowup/CurveSections.lean
`matches_divisor_degree`	theorem	Blowup/DivisorPoints.lean	Lemma 4.3	N885
`matches_divisor_level_one_polynomial`	theorem	Blowup/DivisorPoints.lean		N886
`MatchesDivisor`	structure	Blowup/Charts.lean
`maximal_ideal_power_kills`	theorem	Measure/HenselProducts.lean		N065
`maximalIdeal_twoSeries`	theorem	Surfaces/TruncatedSeries.lean
`measurableEmbedding_pi`	theorem	Measure/HenselProducts.lean		N1054
`measurableSet_inter_of_bijOn`	theorem	Assembly/TypeEvents.lean
`measurableSet_smul_image`	theorem	Assembly/NullBridges.lean
`measure_eq_sum_prod_of_preimage`	theorem	Assembly/TypeEvents.lean
`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	N1065
`member_cell_box_measure`	theorem	Measure/MemberBoxes.lean	(1.7), Theorem 5.1, Proposition 6.1	N1066
`member_cell_chart_coset_decomposition`	theorem	Measure/MemberCharts.lean		N1060
`member_center_linear_part`	theorem	Measure/Haar.lean	Theorem 5.1	N1062
`member_chart_translate`	theorem	Measure/MemberCharts.lean		N1061
`member_children_degree_sum`	theorem	Measure/MemberCharts.lean		N1067
`member_coefficient_measure_map_product_coordinates`	theorem	Measure/MemberCharts.lean		N1058
`member_product_chart_pushforward`	theorem	Measure/MemberCharts.lean		N1059
`mk_mem_principalLayer`	theorem	Blowup/NilpotentGluing.lean
`module_length_quotient_ringEquiv`	theorem	Surfaces/Lengths.lean		N877
`moebiusSum`	def	Reciprocity/Defs.lean		N1146
`moebiusSum_plethSum`	theorem	Reciprocity/Quantum.lean	(7.6)
`monic_cell_law`	theorem	Assembly/MonicCells.lean	Lemma 7.1	N733
`monic_cells_partition`	theorem	Assembly/MonicCells.lean	Lemma 7.1	N739
`monic_coeff_sub_mem_iff`	theorem	Unramified/PolynomialTypes.lean
`monic_congruent_difference_factor`	theorem	Unramified/FactorCells.lean		N606
`monic_inseparable_null`	theorem	Measure/MemberCharts.lean	Remark 6.3, Discriminant locus is null
`monic_poly_reconstruct`	theorem	Unramified/FactorCells.lean		N601
`monic_polynomial_degree`	theorem	Formula/LawAlgebra.lean		N108
`monic_polynomial_divisor`	theorem	Assembly/TypeEvents.lean		N734
`monic_residue_polynomial_count`	theorem	Measure/HenselProducts.lean		N080
`monic_squarefree_factors_of_reduced`	theorem	Unramified/FactorCells.lean		N921
`monic_type_event_measurable_of_root_cell_law`	theorem	Recursion/RootCellLaw.lean		N740
`monicDensity`	def	Basic.lean	Monic model	N008
`monicDensityF`	def	Basic.lean
`monicDensityF_eq_densityValue`	theorem	Assembly/Formulas.lean	(7.3)
`monicExpr`	def	Basic.lean	Theorem 1.1, (1.5)	N007
`monicPolynomial`	def	Basic.lean	Monic model	N008
`monicPolyO`	def	Unramified/Extension.lean
`monicPolyO_map_fraction`	theorem	Unramified/Extension.lean
`monomial_span_pow`	theorem	Blowup/PointTransport.lean		N340
`monomialIdeal`	def	Surfaces/Lengths.lean
`monomialIdeal_mem_iff`	theorem	Surfaces/PowerSeries.lean		N671
`mul_derivative_logSer`	theorem	Reciprocity/Defs.lean
`mul_injective_quotient_transport`	theorem	Blowup/CurveSections.lean
`mvPolynomial_zero_null`	theorem	Measure/AdicCylinders.lean	Discriminant locus is null
`mvPowerSeries_fin_two_mem_variableIdeal_iff`	theorem	Surfaces/PowerSeries.lean		N446
`mvPowerSeries_fin_two_quotient_var_regular_mod_var`	theorem	Surfaces/PowerSeries.lean		N452
`mvPowerSeries_fin_two_span_C_var_isPrime`	theorem	Surfaces/Lengths.lean		N445
`mvPowerSeries_mem_span_C_var_iff`	theorem	Surfaces/Lengths.lean		N444
`mvPowerSeries_quotient_var_regular`	theorem	Surfaces/PowerSeries.lean		N451
`negative_laurent_twist_has_no_kernel`	theorem	Blowup/PointTransport.lean		N322
`never_return_null`	theorem	Recursion/Events.lean	Proof of Theorem 6.2	N567
`nilpotentEval`	def	Surfaces/Lengths.lean
`nilpotentEval_apply_generators`	theorem	Surfaces/PowerSeries.lean		N843
`nilpotentFamily`	def	Surfaces/Lengths.lean
`nilpotentFamily_hasSubst`	theorem	Surfaces/Lengths.lean
`nonboundary_direction_count`	theorem	Formula/PatternCounts.lean	(6.3)	N915
`nonrational_point_residue_surjective`	theorem	Surfaces/Regularity.lean		N868
`nonself_child_rank_lt`	theorem	Formula/StateCombinatorics.lean	Contact-size order, (6.6)	N053
`nonterminating_subset_return_or_bad`	theorem	Recursion/Termination.lean	Proof of Theorem 6.2	N561
`nonzerodivisor_survives_localization`	theorem	Blowup/PointTransport.lean		N261
`normalization_linear_part_cokernel_length_eq`	theorem	Blowup/PointTransport.lean		N388
`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		N939
`normalizedFormCell`	def	Unramified/Extension.lean
`normalizedGenerator`	def	Measure/AdicCylinders.lean
`normalizedIdeal`	def	Measure/AdicCylinders.lean
`normalizer_generator_equation`	theorem	Measure/Normalizer.lean		N201
`normalizer_preserves_adic_congruence` private	theorem	Measure/Normalizer.lean	Lemma 3.1
`normalizing_factor_is_unit`	theorem	Measure/HenselProducts.lean		N168
`one_sub_rational_returnWeight_ne_zero`	theorem	Reciprocity/Patterns.lean
`order_defect_child_le`	theorem	Recursion/OrderDefect.lean		N697
`order_defect_children_sum`	theorem	Recursion/OrderDefect.lean		N696
`order_defect_le_of_tower`	theorem	Recursion/Termination.lean		N693
`order_defect_pi`	theorem	Recursion/Termination.lean		N695
`orderDefect`	def	Algebra/AlgebraType.lean
`orderImage`	def	Algebra/AlgebraType.lean
`orig_monicDensity_eq`	theorem	Assembly/NullBridges.lean	Remark 1.3, Remark 6.3
`orig_projectiveDensity_eq`	theorem	Assembly/NullBridges.lean	Remark 1.3, Remark 6.3
`other_children_count`	theorem	Formula/LawAlgebra.lean		N727
`otherChildren`	def	Basic.lean	(4.7)–(4.8)	N005
`overlap_exceptional_point_comap_maximal`	theorem	Blowup/PointTransport.lean		N772
`overlap_exceptional_point_comap_maximal_right`	theorem	Blowup/PointTransport.lean		N773
`overlap_exceptional_quotient_domain`	theorem	Blowup/PointTransport.lean		N781
`overlap_layer_laurent_coordinates`	theorem	Blowup/NilpotentGluing.lean	(4.1)	N297
`overlap_level_generator_regular`	theorem	Blowup/NilpotentGluing.lean		N782
`overlap_point_residue_field_equiv`	theorem	Blowup/PointTransport.lean		N825
`overlapCurveIdeal`	def	Blowup/Charts.lean
`overlapException`	def	Blowup/Charts.lean
`overlapSlope`	def	Blowup/Charts.lean
`padicIntegers`	abbrev	Basic.lean		N640
`padicIntegers_isDVR`	theorem	Measure/PrimitiveLocus.lean		N642
`padicIntegers_maximal_adic_complete`	theorem	Measure/PrimitiveLocus.lean		N643
`padicIntegers_residueField_finite`	theorem	Measure/PrimitiveLocus.lean		N644
`PadicUnramified`	def	Basic.lean		N640
`pairwise_distinct_irreducible_pow_iInf`	theorem	Blowup/PointTransport.lean		N819
`pairwiseDisjoint_pi_events`	theorem	Assembly/TypeEvents.lean
`parent_ideal_unique_of_level_lattice`	theorem	Blowup/CurveSections.lean		N895
`Pattern`	abbrev	Basic.lean		N005
`pattern_divisor_count`	theorem	Formula/PatternCounts.lean	(6.3)	N917
`pattern_entry_eq_zero_of_lt`	theorem	Reciprocity/Defs.lean
`pattern_entry_le_patternWeight`	theorem	Reciprocity/Defs.lean
`patternDivisors`	abbrev	Blowup/Directions.lean
`patternDivisors_equiv_colorings`	theorem	Formula/PatternCounts.lean	(6.3)	N916
`patternSum`	def	Reciprocity/Defs.lean	lem-7.2	N1146
`patternSum_eq_of_le`	theorem	Reciprocity/Patterns.lean
`patternWeight`	def	Basic.lean		N005
`pExp`	def	Reciprocity/Defs.lean	(7.6)	N1146
`pi_algebraMap_mem_jacobson_bot`	theorem	Measure/HenselProducts.lean		N1033
`pi_field_maximal_ideals`	theorem	Algebra/AlgebraType.lean		N536
`pi_field_quotient_equiv`	theorem	Recursion/OrderDefect.lean		N434
`pi_fields_algEquiv_index_bijection`	theorem	Unramified/FactorCells.lean		N529
`pi_ideal_mem_iff_map_eval`	theorem	Measure/HenselProducts.lean		N1031
`pi_mul_cokernel_length`	theorem	Measure/Normalizer.lean		N1043
`pi_quotient_span_linearEquiv`	theorem	Measure/HenselProducts.lean		N1035
`pi_strict_transform_map_eval`	theorem	Measure/Atlas.lean		N1032
`plethSum`	def	Reciprocity/Defs.lean		N1146
`plethSum_add`	theorem	Reciprocity/Quantum.lean
`plethSum_moebiusSum`	theorem	Reciprocity/Quantum.lean		N1187
`pLog`	def	Reciprocity/Defs.lean	(7.6)	N1146
`point_cell_type_event`	theorem	Assembly/MonicCells.lean		N720
`pointChart`	def	Assembly/NullBridges.lean
`pointChildState`	def	Recursion/Members.lean
`pointCount`	def	Basic.lean	(6.2)	N006
`pointCount_eval`	theorem	Surfaces/PowerSeries.lean		N684
`polynomial_congruence_and_product`	theorem	Unramified/FactorCells.lean		N605
`polynomial_ideal_of_irreducible_pow_le`	theorem	Blowup/PointTransport.lean		N817
`polynomial_quotient_irreducible_pow_length`	theorem	Blowup/PointTransport.lean		N818
`polynomial_quotient_product_equiv`	theorem	Unramified/FactorCells.lean		N525
`polynomial_root_unique_of_derivative_isUnit`	theorem	Surfaces/PowerSeries.lean		N864
`polynomial_type_algEquiv_iff`	theorem	Unramified/PolynomialTypes.lean		N922
`polynomial_type_degree`	theorem	Measure/PrimitiveLocus.lean		N109
`polynomial_type_dvd`	theorem	Algebra/AlgebraType.lean
`polynomial_type_iff_algebra_type`	theorem	Algebra/FactorInvariant.lean		N546
`polynomial_type_map_unramified`	theorem	Unramified/DescentTypes.lean
`polynomial_type_mul_coprime`	theorem	Unramified/PolynomialTypes.lean		N526
`polynomial_type_unique`	theorem	Unramified/PolynomialTypes.lean		N527
`power_coordinates_transport`	theorem	Measure/HenselProducts.lean		N639
`powerCoordinates`	def	Measure/AdicCylinders.lean
`powerSeries_quotient_length_eq_order`	theorem	Surfaces/PowerSeries.lean		N876
`pPow`	def	Reciprocity/Defs.lean	Pow_v and the first-difference rule	N1146
`pPow_mul_pPow`	theorem	Reciprocity/Plethysm.lean
`pPow_pPow`	theorem	Reciprocity/Plethysm.lean	Pow_v and the first-difference rule	N1190
`preimage_inter_pi_eq_biUnion`	theorem	Assembly/TypeEvents.lean
`prime_power_ge_two`	theorem	Formula/LawAlgebra.lean		N059
`PrimePower`	def	Basic.lean		N008
`primitive`	def	Basic.lean	Projective model	N008
`primitive_iff_residue_ne_zero`	theorem	Unramified/PolynomialTypes.lean		N626
`primitive_locus_mass`	theorem	Measure/PrimitiveLocus.lean		N105
`principal_generator_orbit_count`	theorem	Measure/HenselProducts.lean		N069
`principal_ideal_image`	theorem	Blowup/PointTransport.lean		N194
`principal_ideal_unit_invariance`	theorem	Blowup/PointTransport.lean		N191
`principal_layer_quotient_equiv`	theorem	Blowup/ExceptionalLayers.lean		N257
`principal_power_unit_lift`	theorem	Blowup/NilpotentGluing.lean		N358
`principal_residue_ideal_count`	theorem	Surfaces/TruncatedSeries.lean
`PrincipalLayer`	abbrev	Blowup/Charts.lean
`principalLayerMap`	def	Blowup/Charts.lean
`principalLayerMap_apply_eq_mk`	theorem	Blowup/NilpotentGluing.lean
`PrincipalPowerQuotient`	abbrev	Blowup/Charts.lean
`principalPowerReduction`	def	Blowup/Charts.lean
`prod_formalPow_adamsSer_clusterSer_scongr`	theorem	Reciprocity/Plethysm.lean	lem-7.2
`product_chart_projection`	theorem	Measure/Atlas.lean		N1057
`product_coordinates_exist`	theorem	Measure/HenselProducts.lean		N1055
`product_division_equiv`	theorem	Measure/HenselProducts.lean		N1056
`product_law_of_factor_laws`	theorem	Assembly/MonicCells.lean		N732
`projective_cell_affine_type_event`	theorem	Assembly/MonicCells.lean		N752
`projective_cell_conditional_density`	theorem	Unramified/FrobeniusDescent.lean	Lemma 7.1	N632
`projective_cell_mass`	theorem	Unramified/FrobeniusDescent.lean		N629
`projective_cell_normalization_pushforward`	theorem	Unramified/HomogeneousCells.lean		N948
`projective_cells_partition`	theorem	Assembly/MonicCells.lean	Lemma 7.1	N744
`projective_normalizer_eval`	theorem	Unramified/PolynomialTypes.lean		N630
`projective_normalizer_positive`	theorem	Formula/LawAlgebra.lean		N079
`projectiveCell`	def	Unramified/Extension.lean
`projectiveDensity`	def	Basic.lean	Projective model	N008
`projectiveDensityF`	def	Basic.lean
`projectiveDensityF_eq_densityValue`	theorem	Assembly/Formulas.lean	(7.3)
`projectiveExpr`	def	Basic.lean	Theorem 1.1, (1.5)	N007
`projectiveNormalize`	def	Unramified/Extension.lean
`projectiveNormalizer`	def	Basic.lean	Lemma 7.1	N006
`projectiveNormalizer_rational_ne_zero`	theorem	Reciprocity/Quantum.lean
`pulledVariation`	def	Blowup/Charts.lean
`qact`	def	Reciprocity/Defs.lean	(8.9)	N1147
`qact_gaussPhi_dilate_recipSer_scongr` private	theorem	Reciprocity/Main.lean	(9.4)
`qact_qmul`	theorem	Reciprocity/Defs.lean
`qact_qone`	theorem	Reciprocity/Defs.lean
`qact_sub`	theorem	Reciprocity/Defs.lean
`qactRecip`	def	Reciprocity/Defs.lean	Lemma 9.1	N1147
`QCongr`	def	Reciprocity/Defs.lean		N1147
`QCongr.mono`	theorem	Reciprocity/Defs.lean
`QCongr.qact_scongr`	theorem	Reciprocity/Defs.lean
`QCongr.qmul`	theorem	Reciprocity/Defs.lean
`QCongr.trans`	theorem	Reciprocity/Defs.lean
`qcongr_crossingQ_mul_qdagger`	theorem	Reciprocity/Patterns.lean	Lemma 8.3, Theorem 9.3	N1308
`qcongr_qdiag_mul_qdagger`	theorem	Reciprocity/Quantum.lean	Lemma 8.3
`qcongr_qminus_qone`	theorem	Reciprocity/Defs.lean
`qcongr_qplus_qone`	theorem	Reciprocity/Defs.lean
`qdagger`	def	Reciprocity/Defs.lean	(8.2)	N1147
`qdagger_qminus`	theorem	Reciprocity/Quantum.lean	Lemma 8.1
`qdagger_qmul`	theorem	Reciprocity/Quantum.lean	Lemma 8.1	N1245
`qdagger_qplus`	theorem	Reciprocity/Quantum.lean	Lemma 8.1
`qdiag`	def	Reciprocity/Defs.lean		N1147
`qdiag_mul`	theorem	Reciprocity/Quantum.lean	Lemma 8.1	N1249
`qminus`	def	Reciprocity/Defs.lean	Lemma 8.1	N1147
`qminus_qmul`	theorem	Reciprocity/Defs.lean	Lemma 8.1	N1247
`qmul`	def	Reciprocity/Defs.lean	(8.1)	N1147
`qmul_assoc`	theorem	Reciprocity/Quantum.lean	Lemma 8.1	N1241
`qmul_qplus_qdiag_qminus_apply`	theorem	Reciprocity/Defs.lean
`qmul_zero_zero`	theorem	Reciprocity/Quantum.lean
`qone`	def	Reciprocity/Defs.lean	(8.1)	N1147
`qone_qmul`	theorem	Reciprocity/Defs.lean
`qplus`	def	Reciprocity/Defs.lean	Lemma 8.1	N1147
`qplus_qmul`	theorem	Reciprocity/Defs.lean	Lemma 8.1	N1246
`QPositive`	def	Reciprocity/Defs.lean		N1147
`QPositive.qdagger`	theorem	Reciprocity/Quantum.lean
`QPositive.qminus`	theorem	Reciprocity/Quantum.lean
`QPositive.qmul`	theorem	Reciprocity/Quantum.lean
`QPositive.qplus`	theorem	Reciprocity/Quantum.lean
`qPositive_qdiag`	theorem	Reciprocity/Quantum.lean
`qpow`	def	Reciprocity/Defs.lean		N1145
`qpow_add`	theorem	Reciprocity/Defs.lean
`qpow_natCast`	theorem	Reciprocity/Quantum.lean
`qpow_neg_mul_qpow`	theorem	Reciprocity/Quantum.lean
`qpow_one`	theorem	Reciprocity/Quantum.lean
`qpow_zero`	theorem	Reciprocity/Defs.lean
`qrecip`	def	Reciprocity/Defs.lean		N1147
`QSer`	abbrev	Reciprocity/Defs.lean	(8.1)	N1147
`quotient_mul_range_equiv`	theorem	Measure/HenselProducts.lean		N1037
`quotient_ring_length_intrinsic`	theorem	Measure/PrimitiveLocus.lean		N820
`RaisesAdicOrder`	def	Measure/AdicCylinders.lean
`ramificationIdx_unramified_tower`	theorem	Unramified/FrobeniusDescent.lean		N521
`rank_lt_of_degree_lt`	theorem	Formula/LawAlgebra.lean		N022
`rat_smul_eq_scalar_mul`	theorem	Reciprocity/Quantum.lean
`rational_divisorCount`	theorem	Reciprocity/Plethysm.lean
`rational_divisorProbability_single`	theorem	Reciprocity/Patterns.lean	Proposition 6.1
`rational_eminusOne`	theorem	Reciprocity/Plethysm.lean
`rational_returnWeight`	theorem	Reciprocity/Patterns.lean
`recip_main`	theorem	Reciprocity/Main.lean	Theorem 1.2, Remark 1.3, Corollary 10.3	N1319
`recipCoef`	def	Reciprocity/Defs.lean		N1145
`recipCoef_adamsCoef`	theorem	Reciprocity/Quantum.lean
`recipCoef_coeff`	theorem	Reciprocity/Quantum.lean
`recipCoef_lawCoef_globalLaw_true`	theorem	Reciprocity/Main.lean	Theorem 1.2, Lemma 9.2	N1318
`recipCoef_recipCoef`	theorem	Reciprocity/Quantum.lean
`recipCoef_scalar`	theorem	Reciprocity/Quantum.lean
`recipCoef_single`	theorem	Reciprocity/Quantum.lean
`recipPoly`	def	Reciprocity/Defs.lean		N1144
`recipRat`	def	Reciprocity/Defs.lean		N1144
`recipRat_algebraMap`	theorem	Reciprocity/Defs.lean
`recipRat_C`	theorem	Reciprocity/Defs.lean
`recipRat_projectiveNormalizer`	theorem	Reciprocity/Quantum.lean	Lemma 9.2
`recipRat_recipRat`	theorem	Reciprocity/Quantum.lean
`recipRat_X`	theorem	Reciprocity/Defs.lean
`recipSer`	def	Reciprocity/Defs.lean		N1146
`recipSer_dilate`	theorem	Reciprocity/Quantum.lean
`recipSer_gaussPhi`	theorem	Reciprocity/Quantum.lean
`recipSer_mul`	theorem	Reciprocity/Quantum.lean
`recipSer_pPow`	theorem	Reciprocity/Quantum.lean	(7.6)
`recipSer_qact`	theorem	Reciprocity/Quantum.lean
`recipSer_recipSer`	theorem	Reciprocity/Quantum.lean
`recursion_crossing_law`	theorem	Recursion/Events.lean	Proof of Theorem 6.2
`recursion_events_measurable`	theorem	Recursion/Events.lean		N562
`recursion_single_law`	theorem	Recursion/Events.lean	Proof of Theorem 6.2
`recursion_terminal_law`	theorem	Recursion/ChildMembers.lean
`reduced_form_eq_of_residue_coeff`	theorem	Blowup/NilpotentGluing.lean		N953
`reducedFormCell`	def	Unramified/Extension.lean
`reducedFormProduct`	def	Unramified/Extension.lean
`regular_principal_generators_associated`	theorem	Measure/HenselProducts.lean		N202
`RegularAt`	def	Basic.lean		N003
`RegularParameterPair`	def	Blowup/Charts.lean
`repeated_root_chart_type`	theorem	Recursion/OrderDefect.lean		N577
`repeated_root_one_chart_atlas`	theorem	Recursion/OrderDefect.lean	(7.1)	N1080
`residue_basis_family_basis`	theorem	Surfaces/PowerSeries.lean		N498
`residue_basis_family_lift_along_reduction`	theorem	Surfaces/PowerSeries.lean		N504
`residue_basis_family_of_length`	theorem	Surfaces/PowerSeries.lean		N503
`residue_cell_cylinder`	theorem	Unramified/PolynomialTypes.lean		N608
`residue_cell_mass`	theorem	Unramified/PolynomialTypes.lean	Lemma 7.1	N609
`residue_extension_equiv`	theorem	Unramified/PolynomialTypes.lean		N585
`residue_extension_field`	theorem	Unramified/PolynomialTypes.lean		N586
`residue_ideal_has_fixed_generator_lift`	theorem	Measure/PrimitiveLocus.lean		N204
`residue_quotient_card`	theorem	Measure/HenselProducts.lean		N103
`residue_vector_fiber_mass`	theorem	Unramified/PolynomialTypes.lean		N628
`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		N873
`residueKillT_xChartSubst`	theorem	Surfaces/ConcretePoints.lean
`residueKillX`	def	Surfaces/Lengths.lean
`residuePatterns`	def	Basic.lean	(7.3)	N007
`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
`return_event_mass`	theorem	Recursion/Events.lean	Proof of Theorem 6.2	N565
`return_weight_bounds`	theorem	Formula/StateCombinatorics.lean		N027
`returnWeight`	def	Basic.lean	(6.6)	N006
`reverse_normalized_irreducible`	theorem	Algebra/FactorInvariant.lean		N709
`reverse_polynomial_type_iff`	theorem	Algebra/FactorInvariant.lean		N710
`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		N1107
`root_cell_law`	theorem	Recursion/RootCellLaw.lean	(1.3), Theorem 1.1, Cluster model and cluster law B_n, (7.1)	N1109
`root_cell_law_at_universe_member`	theorem	Recursion/RootCellLaw.lean		N1091
`root_field_algEquiv_conjugate_orbit`	theorem	Unramified/FactorCells.lean		N934
`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	N007
`rootMultiplicity_map_eq_count_normalizedFactors`	theorem	Blowup/ExceptionalLayers.lean		N1117
`scalar`	def	Reciprocity/Defs.lean		N1145
`scalar_add`	theorem	Reciprocity/Quantum.lean
`scalar_class_card`	theorem	Unramified/PolynomialTypes.lean		N627
`scalar_eq_algebraMap`	theorem	Reciprocity/Quantum.lean
`scalar_mul`	theorem	Reciprocity/Quantum.lean
`scalar_mul_eq_smul`	theorem	Reciprocity/Quantum.lean
`scalar_mul_left_cancel`	theorem	Reciprocity/Quantum.lean
`scalar_one`	theorem	Reciprocity/Quantum.lean
`scalarClass`	def	Unramified/Extension.lean
`scale_type_valid_degree_iff`	theorem	Formula/StateCombinatorics.lean		N715
`scaled_inverse_from_image_containment`	theorem	Blowup/StrictNormalizer.lean		N233
`scaled_linear_image_index`	theorem	Blowup/StrictNormalizer.lean		N390
`scaled_normalization_identity`	theorem	Measure/PrimitiveLocus.lean	Lemma 3.1	N166
`scaled_strict_map_measurable`	theorem	Recursion/OrderDefect.lean		N1118
`scaledStrictMap`	def	Blowup/Charts.lean
`scaleType`	def	Basic.lean	(6.4)	N001
`scaleTypeHom`	def	Reciprocity/Defs.lean		N1145
`scaling_image_borel_mass`	theorem	Formula/TypeTransport.lean		N706
`SCongr`	def	Reciprocity/Defs.lean		N1146
`SCongr.C_mul`	theorem	Reciprocity/Quantum.lean
`SCongr.dilate`	theorem	Reciprocity/Quantum.lean
`SCongr.expSer`	theorem	Reciprocity/Quantum.lean
`SCongr.logSer`	theorem	Reciprocity/Quantum.lean
`SCongr.moebiusSum`	theorem	Reciprocity/Plethysm.lean
`SCongr.mono`	theorem	Reciprocity/Quantum.lean
`SCongr.mul`	theorem	Reciprocity/Quantum.lean
`SCongr.of_eq`	theorem	Reciprocity/Quantum.lean
`SCongr.of_mul_right`	theorem	Reciprocity/Quantum.lean
`SCongr.plethSum`	theorem	Reciprocity/Plethysm.lean
`SCongr.pow`	theorem	Reciprocity/Quantum.lean
`SCongr.qdiag`	theorem	Reciprocity/Defs.lean
`SCongr.refl`	theorem	Reciprocity/Quantum.lean
`SCongr.symm`	theorem	Reciprocity/Quantum.lean
`SCongr.trans`	theorem	Reciprocity/Quantum.lean
`sectionsToProduct`	def	Blowup/Charts.lean
`selectBlock`	def	Unramified/Extension.lean
`self_patterns_of_single_state`	theorem	Formula/StateCombinatorics.lean	(6.6)	N552
`SelfPattern`	def	Basic.lean		N005
`selfPattern_single_iff`	theorem	Reciprocity/Plethysm.lean
`separable_of_resultant`	theorem	Measure/MemberCharts.lean
`Ser`	abbrev	Reciprocity/Defs.lean	(7.5)	N1146
`series_quotient_equiv_adjoinRoot`	theorem	Recursion/OrderDefect.lean	(7.1)	N576
`shiftUnit`	def	Surfaces/Lengths.lean
`simple_root_derivative_unit`	theorem	Unramified/FrobeniusDescent.lean		N592
`single_residue_ideal_count`	theorem	Measure/StateVolumes.lean	Proposition 3.3	N070
`single_special_fiber_length`	theorem	Unramified/LocalDescent.lean	Lemma 2.1	N063
`single_state_return_chain`	theorem	Recursion/ChildMembers.lean		N560
`single_state_volume`	theorem	Measure/StateVolumes.lean	Proposition 3.3	N414
`singleResidueIdeals`	def	Surfaces/Lengths.lean	Allowed residue ideals, cells, occupied points
`span_pow_mul_colon_eq`	theorem	Surfaces/ConcreteAtlas.lean
`special_fiber_crossing_contact_regular`	theorem	Blowup/StrictNormalizer.lean	Lemma 2.1	N507
`special_fiber_single_contact_regular`	theorem	Blowup/StrictNormalizer.lean	Lemma 2.1	N506
`SpecialFiber`	abbrev	Surfaces/Lengths.lean
`squarefree_map_of_isSeparable`	theorem	Algebra/AlgebraType.lean
`squarefree_monic_has_polynomial_type`	theorem	Algebra/AlgebraType.lean
`squarefree_of_isReduced_adjoinRoot`	theorem	Algebra/AlgebraType.lean
`State`	inductive	Basic.lean	(2.1)	N002
`State.degree`	def	Basic.lean	(2.1)	N002
`State.firstContact`	def	Formula/LawAlgebra.lean
`State.rank`	def	Basic.lean	Contact-size order	N002
`State.tag`	def	Basic.lean		N002
`State.terminal`	def	Basic.lean		N002
`State.Valid`	def	Basic.lean	(2.1)	N002
`State.weight`	def	Basic.lean		N002
`state_fuel_stable`	theorem	Formula/StateCombinatorics.lean		N055
`state_law_coeff_nonneg`	theorem	Formula/PatternCounts.lean		N725
`state_law_unfold`	theorem	Formula/StateCombinatorics.lean	(6.7), Theorem 6.2	N551
`state_measure_atlas_independent`	theorem	Measure/Atlas.lean	Proposition 3.2	N413
`state_measure_total_mass`	theorem	Measure/PrimitiveLocus.lean		N412
`stateContactT`	def	Blowup/Charts.lean
`stateContactX`	def	Blowup/Charts.lean
`stateLaw`	def	Basic.lean	Theorem 6.2	N007
`stateLawFuel`	def	Basic.lean	(6.7)	N007
`stateMeasure`	def	Measure/AdicCylinders.lean
`StateShape`	def	Recursion/Members.lean
`StateShape.valid`	theorem	Recursion/Members.lean
`stateVolume`	def	Basic.lean	Proposition 3.3	N006
`strict_chart_coordinates_commute`	theorem	Blowup/StrictNormalizer.lean		N397
`strict_chart_one_ball_measure`	theorem	Assembly/NullBridges.lean	Theorem 5.1	N396
`strict_chart_preimage_set_identity`	theorem	Blowup/StrictNormalizer.lean		N398
`strict_correction_raises_order`	theorem	Blowup/StrictNormalizer.lean		N230
`strict_normalizer_factors_through_linear`	theorem	Blowup/StrictNormalizer.lean		N231
`strict_normalizer_lattice_image`	theorem	Blowup/StrictNormalizer.lean		N232
`strict_normalizer_preimage_measure`	theorem	Assembly/NullBridges.lean		N391
`strict_normalizer_pushforward_linear`	theorem	Measure/Haar.lean		N239
`strict_quotient_cokernel_length`	theorem	Blowup/StrictNormalizer.lean	Theorem 5.1	N385
`strict_quotient_inclusion_exists`	theorem	Blowup/StrictNormalizer.lean		N381
`strict_quotient_map_exists`	theorem	Blowup/StrictNormalizer.lean		N380
`strict_quotient_map_injective`	theorem	Blowup/StrictNormalizer.lean		N387
`strict_transform_bijOn_child_ideals`	theorem	Blowup/FixedTangentCellBijection.lean	Proposition 4.4	N974
`strict_transform_common_point_transport`	theorem	Blowup/StrictNormalizer.lean		N968
`strict_transform_equation_from_levels`	theorem	Blowup/StrictNormalizer.lean		N814
`strict_transform_equation_of_kernels`	theorem	Blowup/CurveSections.lean
`strict_transform_ideal_of_generator`	theorem	Measure/Haar.lean		N1038
`strict_transform_injOn_fixed_tangent_cell`	theorem	Blowup/FixedTangentCellBijection.lean	Proposition 4.4	N970
`strict_transform_left_point_equation`	theorem	Blowup/CurveSections.lean		N815
`strict_transform_mapsTo_child_ideals`	theorem	Blowup/StrictNormalizer.lean	(4.7)–(4.8)	N967
`strict_transform_translate_measure`	theorem	Assembly/NullBridges.lean		N399
`strict_transforms_give_level_lattice_membership`	theorem	Blowup/StrictNormalizer.lean		N894
`strictTransformAt`	def	Blowup/Charts.lean
`strictTransformIdeal`	def	Blowup/Charts.lean
`substUnit`	def	Surfaces/Lengths.lean
`sum_allowedPatterns_crossing`	theorem	Reciprocity/Defs.lean
`sum_allowedPatterns_reindex`	theorem	Reciprocity/Defs.lean
`sum_allowedPatterns_single`	theorem	Reciprocity/Plethysm.lean
`sum_C_mul_X_pow_pow`	theorem	Reciprocity/Defs.lean
`sum_divisors_moebius`	theorem	Reciprocity/Quantum.lean
`sum_divisors_sum_divisors_div`	theorem	Reciprocity/Quantum.lean
`sum_patterns_scalar_mul_eq_patternSum`	theorem	Reciprocity/Patterns.lean
`sum_prod_densityValue_eq_lawProd`	theorem	Assembly/TypeEvents.lean
`sum_triple_reindex`	theorem	Reciprocity/Plethysm.lean		N1298
`surface_state_generator_mem_maximal`	theorem	Blowup/H0Comparison.lean		N189
`surface_state_ideal_proper`	theorem	Blowup/H0Comparison.lean		N188
`surface_state_vertical_perturbation`	theorem	Blowup/H0Comparison.lean		N268
`surface_threads_injective`	theorem	Blowup/H0Comparison.lean	Lemma 4.2	N346
`surface_threads_range`	theorem	Blowup/H0Comparison.lean	Lemma 4.1, Lemma 4.2, Appendix A	N347
`surface_to_cech_kernel`	theorem	Blowup/H0Comparison.lean		N341
`surface_to_cech_range`	theorem	Blowup/H0Comparison.lean		N344
`surface_to_curve_limit_exists`	theorem	Blowup/H0Comparison.lean		N804
`surface_to_curve_limit_kernel`	theorem	Blowup/CurveSections.lean		N805
`surface_to_curve_quotient_kernel`	theorem	Blowup/CurveSections.lean		N367
`surface_vertical_parameter`	theorem	Blowup/H0Comparison.lean		N187
`SurfaceData`	structure	Surfaces/Lengths.lean	(2.1)
`surfaceIdeal`	def	Surfaces/Lengths.lean
`surfaceIdeal_ne_top`	theorem	Surfaces/PowerSeries.lean		N455
`surfaceMk`	def	Surfaces/Lengths.lean
`surfaceParameterIdeal`	def	Surfaces/Lengths.lean
`surfaceRelation`	def	Surfaces/Lengths.lean
`surfaceRelation_constantCoeff`	theorem	Surfaces/PowerSeries.lean		N448
`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		N1085
`t_chart_nonrational_point_completion_equiv`	theorem	Surfaces/ChartCompletions.lean		N869
`t_chart_origin_completion_equiv`	theorem	Surfaces/ChartCompletions.lean		N861
`t_chart_point_child_member`	theorem	Recursion/ChildMembers.lean		N1087
`t_chart_rational_point_child_data`	theorem	Recursion/OrderDefect.lean		N1084
`t_chart_unit_point_completion_equiv`	theorem	Surfaces/ChartCompletions.lean		N862
`tangent_count_nonneg`	theorem	Formula/PatternCounts.lean		N723
`tangent_divisor_unique`	theorem	Recursion/ChildMembers.lean	Proposition 6.1	N997
`tangentCount`	def	Basic.lean	(6.3)	N006
`tangentLift`	def	Blowup/Charts.lean
`TangentPattern`	structure	Basic.lean	Allowed residue ideals, cells, occupied points	N005
`tChartFamily`	def	Surfaces/Lengths.lean
`tChartFamily_hasSubst`	theorem	Surfaces/Lengths.lean
`term_type_event_cell_decomposition`	theorem	Recursion/ChildMembers.lean		N559
`terminal_curve_order_dvr`	theorem	Recursion/ChildMembers.lean	Lemma 2.2	N1071
`terminal_field_invariant`	theorem	Recursion/ChildMembers.lean	Lemma 2.2	N1073
`terminal_law`	theorem	Formula/StateCombinatorics.lean	Lemma 2.2	N054
`terminates_cell_decomposition`	theorem	Recursion/ChildMembers.lean		N558
`terminates_type_unique`	theorem	Recursion/ChildMembers.lean		N557
`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	N1287
`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
`Tests.main_dvr_galoisField`	theorem	Tests/NonVacuity.lean
`Tests.main_dvr_powerSeries`	theorem	Tests/NonVacuity.lean	Theorem 1.1
`Tests.main_dvr_zmod`	theorem	Tests/NonVacuity.lean
`Tests.monicDensity_four_ramified_quadratic_of_card_eq_two`	theorem	Tests/Regression.lean
`Tests.monicDensity_four_totally_ramified_of_card_eq_two`	theorem	Tests/Regression.lean	Example 10.4
`Tests.monicDensity_four_two_inert_quadratics_of_card_eq_two`	theorem	Tests/Regression.lean
`Tests.monicDensity_powerSeries_zmod_two_four_totally_ramified`	theorem	Tests/Regression.lean	Example 10.4
`Tests.monicDensity_three_totally_ramified_of_card_eq_three`	theorem	Tests/Regression.lean	(10.8)
`Tests.monicDensity_two_ramified`	theorem	Tests/Regression.lean	(1.3)
`Tests.monicExpr_four_eval_two`	theorem	Tests/Regression.lean		N1140
`Tests.monicExpr_four_ramified_quadratic_eval_two`	theorem	Tests/Regression.lean		N1128
`Tests.monicExpr_four_totally_ramified_eval_two`	theorem	Tests/Regression.lean	Example 10.4	N1126
`Tests.monicExpr_four_two_inert_quadratics_eval_two`	theorem	Tests/Regression.lean		N1129
`Tests.monicExpr_three_eval`	theorem	Tests/Regression.lean		N1136
`Tests.monicExpr_three_totally_ramified_eval_three`	theorem	Tests/Regression.lean	(10.8)	N1130
`Tests.monicExpr_two_eval`	theorem	Tests/Regression.lean	(1.3), Example 7.3, (10.8), (11.8), (11.9)–(11.10)	N094
`Tests.monicExpr_two_inert_eval_two`	theorem	Tests/Regression.lean		N096
`Tests.monicExpr_two_ramified_eval_two`	theorem	Tests/Regression.lean	Example 7.3	N096
`Tests.monicExpr_two_split_eval_two`	theorem	Tests/Regression.lean		N096
`Tests.projectiveDensity_four_totally_ramified_of_card_eq_two`	theorem	Tests/Regression.lean
`Tests.projectiveDensity_two_ramified`	theorem	Tests/Regression.lean	Example 7.3
`Tests.projectiveExpr_four_eval_two`	theorem	Tests/Regression.lean		N1141
`Tests.projectiveExpr_four_totally_ramified_eval_two`	theorem	Tests/Regression.lean	Example 10.4	N1127
`Tests.projectiveExpr_two_eval`	theorem	Tests/Regression.lean	Example 7.3, (11.8)	N095
`Tests.single_two_law` private	theorem	Tests/Regression.lean	(1.3), Example 6.4, Example 7.3
`Tests.stateLawFuelStep`	def	Tests/Regression.lean
`towerDelta`	def	Surfaces/Lengths.lean
`towerThreads`	def	Surfaces/Lengths.lean
`transition_unit_congruent_one`	theorem	Blowup/H0Comparison.lean		N360
`translateBlock`	def	Unramified/Extension.lean
`transverse_of_reduction_ne_zero`	theorem	Surfaces/Completeness.lean		N918
`tri`	def	Basic.lean		N006
`tri_chooseTwo`	theorem	Formula/StateCombinatorics.lean		N025
`truncCoeffs`	def	Surfaces/TruncatedSeries.lean
`truncCoeffs_apply`	theorem	Surfaces/TruncatedSeries.lean
`truncExponent`	def	Surfaces/TruncatedSeries.lean
`truncIndex`	def	Surfaces/TruncatedSeries.lean
`twisted_kernel_from_surface`	theorem	Blowup/H0Comparison.lean		N366
`two_chart_common_multiplicity_eq`	theorem	Blowup/DivisorPoints.lean		N826
`two_chart_datum_concrete_instances`	theorem	Surfaces/ConcreteStrictTransforms.lean		N910
`two_chart_datum_concrete_transverse`	theorem	Surfaces/ConcreteStrictTransforms.lean		N911
`two_chart_global_function_exists`	theorem	Blowup/FixedTangentCellBijection.lean	Lemma 4.3	N833
`two_chart_kernels_agree_on_overlap`	theorem	Blowup/TwoChartCurveData.lean		N787
`two_chart_layer_correction`	theorem	Blowup/CurveSections.lean		N300
`two_chart_left_data_transverse_finite`	theorem	Blowup/CurveSections.lean		N777
`two_chart_left_generators_regular_on_overlap`	theorem	Blowup/TwoChartCurveData.lean		N896
`two_chart_left_level_one_kernel_polynomial`	theorem	Blowup/DivisorPoints.lean		N827
`two_chart_left_points_maximal`	theorem	Blowup/CurveSections.lean		N775
`two_chart_level_generators_agree_on_overlap`	theorem	Blowup/TwoChartCurveData.lean		N788
`two_chart_level_generators_exist`	theorem	Blowup/TwoChartCurveData.lean		N832
`two_chart_right_data_transverse_finite`	theorem	Blowup/CurveSections.lean		N778
`two_chart_right_points_maximal`	theorem	Blowup/TwoChartCurveData.lean		N776
`two_mul_chooseTwo`	theorem	Reciprocity/Defs.lean
`two_mul_tri`	theorem	Reciprocity/Defs.lean
`two_term_coker_map_surjective`	theorem	Blowup/TwoChartCurveData.lean		N307
`TwoChartCurveData`	structure	Blowup/Charts.lean
`TwoSeries`	abbrev	Surfaces/Lengths.lean
`twoSeries_eval_exists_of_isAdicComplete`	theorem	Surfaces/Completeness.lean		N858
`twoSeries_ringHom_ext_of_isNilpotent`	theorem	Surfaces/Completeness.lean		N842
`twoSeriesResidueEquiv`	def	Surfaces/TruncatedSeries.lean
`twoTermCokerMap`	def	Surfaces/Lengths.lean
`type_event_null_difference`	theorem	Recursion/Events.lean		N575
`typeDegree`	def	Basic.lean	Type of degree n	N001
`typeEvent`	def	Assembly/NullBridges.lean
`unique_scaled_generator_normalization`	theorem	Measure/Normalizer.lean	Lemma 3.1	N167
`units_lift_from_local_quotient`	theorem	Measure/PrimitiveLocus.lean		N203
`universal_law_statement`	theorem	Recursion/Events.lean	Theorem 6.2	N572
`universe_basic_facts`	theorem	Recursion/ChildMembers.lean		N555
`unramified_coefficient_measure_haar`	theorem	Measure/PrimitiveLocus.lean		N924
`unramified_coefficient_measure_pi`	theorem	Measure/Haar.lean	Theorem 5.1	N927
`unramified_extension_measure_package`	theorem	Measure/Haar.lean		N926
`unramified_fraction_base_change`	theorem	Algebra/AlgebraType.lean		N540
`unramified_fraction_field_lift`	theorem	Unramified/FrobeniusDescent.lean		N929
`unramified_fraction_isSeparable`	theorem	Unramified/DescentTypes.lean
`unramified_free_module`	theorem	Unramified/FrobeniusDescent.lean		N581
`unramified_generic_fibre_ascent`	theorem	Recursion/Events.lean		N438
`unramified_generic_fibre_witness`	theorem	Algebra/AlgebraType.lean		N542
`unramified_is_dvr`	theorem	Unramified/FrobeniusDescent.lean	Standard facts	N589
`unramified_lift_map_parameter_quotient_irreducible`	theorem	Surfaces/Completeness.lean		N865
`unramified_root_isUnit_of_two_le_natDegree`	theorem	Surfaces/Completeness.lean		N870
`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	N001
`variableIdeal`	def	Surfaces/Lengths.lean
`wf_returnWeight`	theorem	Reciprocity/Plethysm.lean
`x_chart_infinity_completion_equiv`	theorem	Surfaces/ChartCompletions.lean		N863
`X_inv_sub_X_zpow_neg_tri_ne_zero`	theorem	Reciprocity/Patterns.lean	Proof of monic/cluster reciprocity
`X_sub_one_mul_crossingWeight`	theorem	Reciprocity/Defs.lean
`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