INSPECTION_SCOPE	coverage and raw logical graph inspection; no kernel replay; no exported axiom cache used
IMPORT_COUNT	4952
PROJECT_RECURSION_COMPANION	PL1.Bonami.cubeFintype._unsafe_rec	PL1.Bonami.cubeFintype	PL1.BonamiHaarBridge	PASS
RAW_IMPORTED_AXIOM	Classical.choice	module=Init.Prelude	standard=true	project=false
PROJECT_RECURSION_COMPANION	PL1.Bonami.cubeDiscreteTopology._unsafe_rec	PL1.Bonami.cubeDiscreteTopology	PL1.BonamiHaarBridge	PASS
RAW_IMPORTED_AXIOM	lcVoid	module=Init.Prelude	standard=false	project=false
RAW_IMPORTED_AXIOM	lcCast	module=Init.Prelude	standard=false	project=false
PROJECT_RECURSION_COMPANION	PL1.Bonami.cubeTopologicalSpace._unsafe_rec	PL1.Bonami.cubeTopologicalSpace	PL1.BonamiHaarBridge	PASS
RAW_IMPORTED_AXIOM	lcErased	module=Init.Prelude	standard=false	project=false
RAW_IMPORTED_AXIOM	Quot.lcInv	module=Init.Prelude	standard=false	project=false
PROJECT_RECURSION_COMPANION	PL1.EnfloBush.maxAbs._unsafe_rec	PL1.EnfloBush.maxAbs	PL1.EnfloBush	PASS
PROJECT_RECURSION_COMPANION	PL1.ALDyadicEmbedding.wordEquiv._unsafe_rec	PL1.ALDyadicEmbedding.wordEquiv	PL1.ALDyadicEmbedding	PASS
PROJECT_RECURSION_COMPANION	PL1.Bonami.Cube._unsafe_rec	PL1.Bonami.Cube	PL1.BonamiTensorization	PASS
RAW_IMPORTED_AXIOM	Lean.trustCompiler	module=Init.Core	standard=false	project=false
RAW_IMPORTED_AXIOM	isScalarObj	module=Init.Prelude	standard=false	project=false
RAW_IMPORTED_AXIOM	Lean.ofReduceBool	module=Init.Core	standard=false	project=false
PROJECT_RECURSION_COMPANION	PL1.EnfloBush.signAt._unsafe_rec	PL1.EnfloBush.signAt	PL1.EnfloBush	PASS
RAW_IMPORTED_AXIOM	lcProof	module=Init.Prelude	standard=false	project=false
PROJECT_RECURSION_COMPANION	LLexpr.reindexExpr._unsafe_rec	LLexpr.reindexExpr	BanLat.LLexpr	PASS
PROJECT_RECURSION_COMPANION	PL1.IntrinsicExposedPoint.resolventIterate._unsafe_rec	PL1.IntrinsicExposedPoint.resolventIterate	PL1.IntrinsicExposedPoint	PASS
RAW_IMPORTED_AXIOM	sorryAx	module=Init.Prelude	standard=false	project=false
PROJECT_RECURSION_COMPANION	PL1.Bonami.sample._unsafe_rec	PL1.Bonami.sample	PL1.BonamiHaarBridge	PASS
PROJECT_RECURSION_COMPANION	_private.PL1.LatticeAbsoluteContinuity.0.PL1.SchurLattice.partialSup._unsafe_rec	_private.PL1.LatticeAbsoluteContinuity.0.PL1.SchurLattice.partialSup	PL1.LatticeAbsoluteContinuity	PASS
PROJECT_RECURSION_COMPANION	PL1.BalancedFragmentTree.cell._unsafe_rec	PL1.BalancedFragmentTree.cell	PL1.BalancedFragmentTree	PASS
PROJECT_RECURSION_COMPANION	PL1.EnfloBush.signedSum._unsafe_rec	PL1.EnfloBush.signedSum	PL1.EnfloBush	PASS
PROJECT_RECURSION_COMPANION	PL1.Bonami.cubeCharacter._unsafe_rec	PL1.Bonami.cubeCharacter	PL1.BonamiHaarBridge	PASS
RAW_IMPORTED_AXIOM	Quot.sound	module=Init.Prelude	standard=true	project=false
RAW_IMPORTED_AXIOM	propext	module=Init.Core	standard=true	project=false
PROJECT_RECURSION_COMPANION	PL1.Bonami.noise._unsafe_rec	PL1.Bonami.noise	PL1.BonamiTensorization	PASS
RAW_IMPORTED_AXIOM	lcAny	module=Init.Prelude	standard=false	project=false
RAW_IMPORTED_AXIOM	Lean.ofReduceNat	module=Init.Core	standard=false	project=false
PROJECT_RECURSION_COMPANION	PL1.Bonami.average._unsafe_rec	PL1.Bonami.average	PL1.BonamiTensorization	PASS
PROJECT_RECURSION_COMPANION	PL1.FiniteRademacherClipping.rademacherSum._unsafe_rec	PL1.FiniteRademacherClipping.rademacherSum	PL1.FiniteRademacherClipping	PASS
RAW_IMPORTED_AXIOM	lcUnreachable	module=Init.Prelude	standard=false	project=false
PROJECT_RECURSION_COMPANION	LLexpr.eval._unsafe_rec	LLexpr.eval	BanLat.LLexpr	PASS
ALL_CONSTANTS	total=438918	eligible=435310	unsafe=653	partial=2955	axioms=15
PROJECT_CONSTANTS	total=5701	eligible=5683	unsafe=0	partial=18	axioms=0
PROJECT_MODULE_COVERAGE	PASS	expected=222	criterion=actual_module_origin
EXACT_FINAL_TYPE	PL1.theoremAReal	PL1.TheoremARealStatement	PASS
EXACT_FINAL_TYPE	PL1.theoremAComplexStrong	PL1.TheoremAComplexStrongStatement	PASS
EXACT_FINAL_TYPE	PL1.theoremBReal	PL1.TheoremBRealStatement	PASS
EXACT_FINAL_TYPE	PL1.theoremBComplexStrong	PL1.TheoremBComplexStrongStatement	PASS
RAW_REACHABILITY	PL1.hasEquivalentRealLatticeNorm_of_continuousLinearEquiv	roots=1	visited=14207	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.not_nonempty_continuousLinearEquiv_of_not_hasEquivalentRealLatticeNorm	roots=1	visited=14208	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.MainTheoremsStatement	roots=1	visited=33145	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.theoremA_except_nonlattice	roots=1	visited=52777	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.theoremB_partial	roots=1	visited=52268	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.schurRates_projection_range_underlyingReal_hasSchurProperty	roots=1	visited=49990	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.projection_range_underlyingReal_separableSpace	roots=1	visited=48779	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.RNPBridge.hasRadonNikodymProperty_of_finiteDimensional	roots=1	visited=33532	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.RNPTransport.hasRadonNikodymProperty_restrictScalars_iff	roots=1	visited=26748	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ContractiveRetract.norm_transport_le	roots=1	visited=14225	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ContractiveRetract.rangeEquiv_norm	roots=1	visited=12132	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.DyadicTrace.norm_trace_le	roots=1	visited=36276	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.DyadicTrace.trace_id	roots=1	visited=35151	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.DyadicTrace.one_le_norm_id_sub	roots=1	visited=36312	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.intrinsic_hasMetricApproximationProperty	roots=1	visited=48552	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.norm_intrinsicExpectation_eq_one	roots=1	visited=48814	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.finrank_intrinsicExpectation	roots=1	visited=48832	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.finrank_intrinsicBlock	roots=1	visited=48845	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.intrinsicBlock_comp	roots=1	visited=48508	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.intrinsicBlock_expansion_unique	roots=1	visited=48542	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.tendsto_intrinsicBlock_partialSum	roots=1	visited=48513	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.schur_intrinsic_not_boundedlyComplete	roots=1	visited=50599	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_intrinsic_not_boundedlyComplete	roots=1	visited=50577	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.schur_intrinsic_exists_nonCauchy_branch	roots=1	visited=50601	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_intrinsic_exists_nonCauchy_branch	roots=1	visited=50579	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.schur_intrinsic_no_uniform_sign_bound	roots=1	visited=51682	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.DecompositionRNP.hasRadonNikodymProperty_of_boundedlyCompleteDecomposition	roots=1	visited=35272	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ScalarDecompositionRNP.hasRNP_of_scalar_projections	roots=1	visited=35282	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.UnconditionalRNP.hasRadonNikodymProperty_of_schur_unconditional_projections	roots=1	visited=35322	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.noiseL1_add	roots=1	visited=39258	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.continuous_noiseL1_apply	roots=1	visited=39278	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.resolventL1_strong_zero	roots=1	visited=48180	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.resolventL1_eq_integral	roots=1	visited=48329	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.norm_resolventL1_sub_truncated_le	roots=1	visited=48979	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.truncatedResolventL1_tendsto	roots=1	visited=48980	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.SchurLattice.tendsto_zero_of_antitone_net_isGLB	roots=1	visited=16225	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.SchurLattice.conditionallyCompleteLattice	roots=1	visited=16360	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.SchurLattice.exists_countable_maximal_disjoint_positive_family	roots=1	visited=11531	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.OperatorDomination.exists_measurable_dominator	roots=1	visited=36462	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.OperatorDomination.cutoff_approximation	roots=1	visited=35145	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.OperatorDomination.maskedRestrictionLp	roots=1	visited=35085	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.LpInterpolation.norm_toLp_le_of_ae_norm_bound	roots=1	visited=23606	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.HilbertTraceBounds.sum_cell_dual_norm_sq_le	roots=1	visited=29613	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.HilbertTraceBounds.norm_sum_cell_apply_le	roots=1	visited=29683	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.SmoothingTrace.trace_tendsto_zero_of_smoothing	roots=1	visited=37790	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.SmoothingTrace.one_le_norm_id_sub_of_smoothing	roots=1	visited=37795	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.SmoothingTrace.trace_tendsto_zero_of_smoothing_approximation	roots=1	visited=37793	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.SmoothingTrace.one_le_norm_id_sub_of_smoothing_approximation	roots=1	visited=37798	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Ell1RNP.hasRadonNikodymProperty	roots=1	visited=35683	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.schur_intervalProjection_range_not_isomorphic_ell1	roots=1	visited=52337	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_intervalProjection_range_not_isomorphic_ell1	roots=1	visited=52315	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.schur_intrinsic_no_uniform_scalar_sign_bound	roots=1	visited=51709	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.InputCompression.norm_input_compression_error_tendsto_zero	roots=1	visited=37334	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.OutputCompression.tendsto_output_compression	roots=1	visited=19566	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.MatrixTrace.trace_tendsto_zero_of_smoothing_entries	roots=1	visited=38568	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.MatrixTrace.one_le_norm_id_sub_of_smoothing_entries	roots=1	visited=38573	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.hasEquivalentRealLatticeNorm_iff_hasBanachLatticeModel	roots=1	visited=14419	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.theoremA_of_separableSchurLatticeRNP	roots=1	visited=52917	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.separableSchurLatticeRNP	roots=1	visited=36447	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.theoremA	roots=1	visited=54072	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.theoremAReal	roots=1	visited=54074	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.theoremAComplexStrong	roots=1	visited=54074	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ComplementedLattice.theoremB_real_and_complex_of_real_structural_properties	roots=1	visited=52956	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ComplementedLattice.scalarIntervalRealCopy	roots=1	visited=39043	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.NoiseHypercontractivity.norm_positiveTimeNoiseL2_le_one	roots=1	visited=44096	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.NoiseHypercontractivity.positiveTimeNoiseL2_overlap	roots=1	visited=44092	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.NoiseHypercontractivity.exponent_lt_two	roots=1	visited=13150	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_resolvent_hasVanishingDyadicTrace	roots=1	visited=50658	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_projection_hasVanishingDyadicTrace	roots=1	visited=51041	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_intervalProjection_hasVanishingDyadicTrace	roots=1	visited=52192	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_intervalProjection_identity_distance	roots=1	visited=52198	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_intervalProjection_not_factors_identity	roots=1	visited=52272	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.schur_intrinsic_hasDaugavetProperty	roots=1	visited=50561	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_intrinsic_hasDaugavetProperty	roots=1	visited=50535	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.schur_intrinsic_underlyingReal_hasDaugavetProperty	roots=1	visited=50564	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_intrinsic_underlyingReal_hasDaugavetProperty	roots=1	visited=50538	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.IntrinsicTailNorm.schur_norm_id_sub_intrinsicExpectation_eq_two	roots=1	visited=50462	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.IntrinsicTailNorm.constant_norm_id_sub_intrinsicExpectation_eq_two	roots=1	visited=50436	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.IntrinsicExposedPoint.norm_integralFunctional	roots=1	visited=48588	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.IntrinsicExposedPoint.schur_integralFunctional_exposes_constant	roots=1	visited=48633	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.IntrinsicExposedPoint.constant_integralFunctional_exposes_constant	roots=1	visited=48633	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ExplicitMartingale.schur_explicit_martingale	roots=1	visited=50149	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ExplicitMartingale.constant_explicit_martingale	roots=1	visited=50127	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ExplicitMartingale.schur_beta_exists_dual_oscillation	roots=1	visited=50535	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ExplicitMartingale.schur_beta_not_weaklyCauchy_real	roots=1	visited=50535	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.isGeneratorPair_iff_mem_graph	roots=1	visited=49360	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.dense_generator_domain	roots=1	visited=49385	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.isClosed_generator_graph	roots=1	visited=49351	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.IsGeneratorPair.polynomial_core	roots=1	visited=49389	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.GeneratorGraphBanach.norm_eq	roots=1	visited=45758	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.GeneratorGraphBanach.kFunctional_eq	roots=1	visited=49452	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.KFunctional.half_norm_defect_le	roots=1	visited=48200	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.KFunctional.value_le_defect	roots=1	visited=48202	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.DiscreteInterpolation.mem_range_evalZero_iff	roots=1	visited=48455	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.DiscreteInterpolation.half_norm_le	roots=1	visited=48465	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.DiscreteInterpolation.normValue_le	roots=1	visited=48469	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.DiscreteInterpolation.extendedNorm_ne_top_iff	roots=1	visited=48472	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.KFunctional.continuousNorm_le_four_extendedNorm	roots=1	visited=45819	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.KFunctional.extendedNorm_le_five_continuousNorm	roots=1	visited=45814	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Interpolation.mem_intrinsic_iff	roots=1	visited=49817	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Interpolation.normValue_lower	roots=1	visited=49839	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Interpolation.normValue_upper	roots=1	visited=49840	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Interpolation.intrinsic_eq_realInterpolation	roots=1	visited=49856	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Interpolation.mem_intrinsic_iff_integrable	roots=1	visited=49834	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Interpolation.normValue_eq_integral	roots=1	visited=49839	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.KFunctional.continuousNorm_add_le	roots=1	visited=45715	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.KFunctional.continuousNorm_smul	roots=1	visited=45706	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.KFunctional.continuousNorm_eq_zero_iff	roots=1	visited=45759	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.InterpolationNorm.continuousLinearEquiv	roots=1	visited=49936	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.InterpolationNorm.norm_eq_integral	roots=1	visited=49937	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.InterpolationNorm.inclusion_injective	roots=1	visited=49941	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Daugavet.SliceCriterion.diam_realPartSlice	roots=1	visited=14827	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Daugavet.SliceCriterion.not_strongly_exposes	roots=1	visited=14579	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.schur_intrinsic_underlyingReal_diam_realPartSlice	roots=1	visited=50439	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_intrinsic_underlyingReal_diam_realPartSlice	roots=1	visited=50413	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.schur_intrinsic_integral_maximizing_sequence_far	roots=1	visited=50546	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_intrinsic_integral_maximizing_sequence_far	roots=1	visited=50521	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ComplementedLattice.OneSummingWith.precomp	roots=1	visited=14244	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ComplementedLattice.OneSummingWith.postcomp	roots=1	visited=14204	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ComplementedLattice.TwoSummingWith.precomp	roots=1	visited=14260	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ComplementedLattice.TwoSummingWith.postcomp	roots=1	visited=14233	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ComplementedLattice.uniform_finite_summing_estimates	roots=1	visited=19081	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ComplementedLattice.disjoint_sum_norm_le_of_complemented_ambient_estimates	roots=1	visited=20909	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.theoremAReal	roots=1	visited=54074	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.theoremAComplexStrong	roots=1	visited=54074	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.theoremB	roots=1	visited=53758	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.theoremBReal	roots=1	visited=53760	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.theoremBComplexStrong	roots=1	visited=53760	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.FiniteSumming.matrixGrothendieckWith_128	roots=1	visited=12137	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.FiniteSumming.oneSumming_128	roots=1	visited=19672	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.FiniteSumming.twoSumming_128	roots=1	visited=19388	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.DyadicL1Coordinates.analysis_synthesis	roots=1	visited=35286	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.DyadicL1Coordinates.norm_synthesis	roots=1	visited=35299	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.IntervalSumming.oneSumming_interval	roots=1	visited=36468	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.IntervalSumming.twoSumming_interval	roots=1	visited=36499	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.PositiveLowerOneBridge.positiveLowerOne_of_disjoint	roots=1	visited=17781	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.PositiveLowerOneBridge.positiveLowerOne_of_complemented_ambient	roots=1	visited=20864	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ALRenorming.seminorm_bounds	roots=1	visited=13048	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ALRenorming.isALNorm	roots=1	visited=13141	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ALAtomic.coordinateIsometry	roots=1	visited=26889	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ALAtomic.hasSchurProperty	roots=1	visited=29294	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ALDyadicEmbedding.containsIsomorphicCopy_of_not_atomic	roots=1	visited=37126	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.ALAlternative.schur_or_contains_interval_of_complemented	roots=1	visited=38709	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.EnfloBush.dyadic_max_integral_mul_norm	roots=1	visited=35218	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.EnfloBush.exists_dyadic_majorant	roots=1	visited=34940	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.EnfloBush.noise_comp_dyadicVanishing	roots=1	visited=45296	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.DyadicCoordinateDomination.exists_summable_majorant	roots=1	visited=10741	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.EnfloBush.maxMass_flatten	roots=1	visited=33843	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.EnfloBush.not_boundedBelow_sum_of_coordinates	roots=1	visited=36386	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.EnfloBush.dyadicVanishing_resolvent_of_noise	roots=1	visited=49314	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.EnfloBush.dyadicVanishing_intrinsic_evalZero	roots=1	visited=35236	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.EnfloBush.dyadicVanishing_intrinsic_flatten	roots=1	visited=36272	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.EnfloBush.not_boundedBelow_two_maps	roots=1	visited=36431	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.IntrinsicRealParts.norm_le_parts	roots=1	visited=48468	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.EnfloBush.scalarIntrinsic_no_real_L1_of_operators	roots=1	visited=48923	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_intervalProjection_range_no_real_L1	roots=1	visited=51875	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	PL1.Noise.constant_intervalProjection_range_no_underlying_real_L1	roots=1	visited=51890	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_REACHABILITY	ALL_ELIGIBLE_PROJECT	roots=5683	visited=60990	unsafe=0	partial=0	missing=0	axioms=#[propext, Classical.choice, Quot.sound]
RAW_AXIOM_ROOT_COVERAGE	PASS	requested=157
FRESH_INSPECT	PASS
