Login

promachina/iut-lean

maintenance drain
master public updated latest build queued
13430 checked 0 blocked 0 open 1 queued last run

Next action Worker drain enabled Verification is queued while maintenance drain is pausing new claims. Latest error: job_failed
Theorems · 13430 tracked
Indexed 13430 theorem-like declarations
Sorries left 0% 0 markers in 0 declarations
Blueprint 22 nodes to go
28 of 50 proved 3 ready 19 blocked

Showing 200 theorems.

Theorem Status Owner Module Last run
absLabelAverageCoefficient_gt_one Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absLabelFromProcession_core Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absLabelFromProcession_injective Checked unowned Iut/Stage1/IUTStage1Experiments.lean
absLabelFromProcession_injective Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absLabelFromProcession_surjective Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absLabelFromProcession_surjective Checked unowned Iut/Stage1/IUTStage1Experiments.lean
absLabelProcession_card_eq_half_plus_one Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absLabelProcessionCard_eq_halfPlusOne Checked unowned Iut/Stage1/IUTStage1Experiments.lean
absLabelProcession_core_maps_to_zero Checked unowned Iut/Stage1/IUTStage1Experiments.lean
absLabelProcessionEquivFullLabel_apply Checked unowned Iut/Stage1/IUTStage1Experiments.lean
absLabelProcessionEquivFullLabel_apply Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absLabelProcession_thetaExponent_eq_square Checked unowned Iut/Stage1/IUTStage1Experiments.lean
absLabelProcessionTop_eq_half_minus_one Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absLabelProcessionTop_eq_halfMinusOne Checked unowned Iut/Stage1/IUTStage1Experiments.lean
absLabelProcessionTop_ge_two Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absLabelProcessionTop_ge_two Checked unowned Iut/Stage1/IUTStage1Experiments.lean
absLabelProcessionTop_pos Checked unowned Iut/Stage1/IUTStage1Experiments.lean
absLabelProcessionTop_pos Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absLabelProcession_value_le_half Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absLabel_thetaExponent_matches_halfRange_j2 Checked unowned Iut/Stage1/IUTStage1Experiments.lean
absLabel_thetaPilot_degree_matches_halfRange_j2 Checked unowned Iut/Stage1/IUTStage1Experiments.lean
absLogQ_pos Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
absLogQ_pos Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
absLogQ_pos Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
absLogQ_pos Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
absNonzeroIndexNatCast_ne_neg Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absNonzeroIndexNatCast_ne_zero Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absNonzeroIndexNatCast_val Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absNonzeroLabelAverageCoefficient_gt_fullLabelAverageCoefficient Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
absoluteLogQ_eq Checked unowned Iut/Stage1/IUTStage1IUTIVAlgebra.lean
absoluteLogQ_pos Checked unowned Iut/Stage1/IUTStage1IUTIVAlgebra.lean
absThetaPilotDegree_distinguishes_one_two_of_q_ne_zero Checked unowned Iut/Stage1/IUTStage1Experiments.lean
absThetaPilotDegree_one_two_equal_iff_q_zero Checked unowned Iut/Stage1/IUTStage1Experiments.lean
acted_factor_eq Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
acted_factor_eq Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
acted_product_eq_sum Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
actedProductLogVolume_eq_original_plus_unitCopies Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
acted_tensor_packet_eq_sum Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
actedTensorPacketLogVolume_eq_original_plus_generators Checked unowned Iut/Stage1/IUTStage1Gaussian.lean
actionCount_eq_fiberCardinality Checked unowned Iut/Stage1/IUTStage1HodgeSHE.lean
actionCount_eq_fiberCardinality Checked unowned Iut/Stage1/IUTStage1HodgeSHE.lean
actionCountForKind_archimedean Checked unowned Iut/Stage1/IUTStage1HodgeSHE.lean
actionCountForKind_nonarchimedean Checked unowned Iut/Stage1/IUTStage1HodgeSHE.lean
action_entry_mem Checked unowned Iut/Stage1/IUTStage1Theorem311.lean
action_entry_mem Checked unowned Iut/Stage1/IUTStage1Theorem311.lean
actionStep_preserves_capsuleCount Checked unowned Iut/Stage1/IUTStage1Theorem311.lean
actionStep_preserves_capsuleNormalizedLogVolume Checked unowned Iut/Stage1/IUTStage1Theorem311.lean
actionStep_preserves_capsuleTotalLogVolume Checked unowned Iut/Stage1/IUTStage1Theorem311.lean
actionStep_preserves_directSummandCount Checked unowned Iut/Stage1/IUTStage1Theorem311.lean
action_translateElement_eq Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
add_gluingTranslate Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
additiveLogVolume Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
additiveLogVolume Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
additiveLogVolume Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
additiveLogVolume Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
additiveLogVolume Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
additive_normalizedRingOfIntegers_zero Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
additive_normalizedUniformizerShift Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
additive_rawUniformizerShift Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
additiveSource_compactOpenSubset_eq Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
additiveSource_ringOfIntegers_eq Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
add_vadd Checked unowned Iut/Foundations/InitialThetaData.lean
add_vadd Checked unowned Iut/Stage1/IUTStage1FiniteLabels.lean
adjacent_logLink_preserves_action Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjacent_logLink_preserves_realifiedLogVolume Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjacent_swap_not_automorphism Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjacent_swap_not_edge_preserving Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjustedExactThetaAudit Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
adjusted_familyHull_eq_normalizedDeterminant Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjustedFamilyHullLogVolume_eq_normalizedDeterminant Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
adjustedFamilyHullLogVolume_eq_normalizedDeterminant Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjustedFamilyHullLogVolume_eq_normalizedDeterminant Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
adjustedGaussianAudit Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
adjustedHullOperator_eq_coordinateScalarPrincipal Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjustedHullOperator_eq_directProductPrincipal Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjustedHullOperator_eq_nonzeroScalarProduct Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjustedHullOperator_eq_principal Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjustedHullOperator_eq_principal Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
adjustedHullOperator_eq_principal Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjustedHullOperator_eq_principal Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
adjustedHullOperator_eq_scalarImagePrincipal Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjustedHullOperator_eq_scalarParameterProduct Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjustedLogVolume_eq Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjustedLogVolume_eq Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjusted_raw_eq Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjusted_raw_eq Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjustedRawLogVolume_eq Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
adjustedSource_eq_valuationBall Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
adjustedSource_eq_valuationBall Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
adjustedStepXIAudit Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
adjustedStepXIAudit Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
adjustedSummand_eq_determinant Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
adjustedSummand_eq_determinant Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
adjustedSummand_eq_determinant Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
adjustedSummandLogVolume_eq_determinantLogVolume Checked unowned Iut/Stage1/IUTStage1StepXI.lean
adjustedSummandLogVolume_eq_determinantLogVolume Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
afterInd1_average_eq_before Checked unowned Iut/Stage1/IUTStage1StepX.lean
afterInd1_average_le_ind3UpperBound Checked unowned Iut/Stage1/IUTStage1StepX.lean
afterInd1Average_le_statementEndpoint_thetaRealLogVolume Checked unowned Iut/Stage1/IUTStage1StepX.lean
afterInd1Average_neg_of_qPilotPositive Checked unowned Iut/Stage1/IUTStage1StepX.lean
afterInd2_average_eq_before Checked unowned Iut/Stage1/IUTStage1StepX.lean
afterInd2_average_le_ind3UpperBound Checked unowned Iut/Stage1/IUTStage1StepX.lean
afterInd2Average_le_statementEndpoint_thetaRealLogVolume Checked unowned Iut/Stage1/IUTStage1StepX.lean
afterInd2Average_neg_of_qPilotPositive Checked unowned Iut/Stage1/IUTStage1StepX.lean
aggregateLevelIsNotPointwise Checked unowned Iut/Stage1/IUTStage1Experiments.lean
aggregate_ne_pointwise Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
algebraicClosure_isAlgClosure Checked unowned Iut/Foundations/InitialThetaData.lean
algorithm_certified Checked unowned Iut/Stage1/IUTStage1Theorem311.lean
algorithm_certified Checked unowned Iut/Stage1/IUTStage1StepXI.lean
algorithmCertified Checked unowned Iut/Stage1/IUTStage1Source.lean
algorithmCertified Checked unowned Iut/Stage1/IUTStage1StepXI.lean
algorithmCertified Checked unowned Iut/Stage1/IUTStage1StepXI.lean
algorithmCertified Checked unowned Iut/Stage1/IUTStage1StepXI.lean
algorithmCertified Checked unowned Iut/Stage1/SourceObligations.lean
algorithmicOutput_certified_eq Checked unowned Iut/Stage1/IUTStage1StepXI.lean
algorithmicOutput_eq_subclaims Checked unowned Iut/Stage1/IUTStage1StepXI.lean
algorithm_output_certified Checked unowned Iut/Stage1/IUTStage1StepXI.lean
algorithmOutputCertified Checked unowned Iut/Stage1/IUTStage1StepXI.lean
algorithmOutputCertified Checked unowned Iut/Stage1/IUTStage1Theorem311.lean
algorithmOutputCertified Checked unowned Iut/Stage1/IUTStage1StepXI.lean
algorithmOutputCertified Checked unowned Iut/Stage1/IUTStage1StepXI.lean
algorithmOutputCertified_eq_subclaims Checked unowned Iut/Stage1/IUTStage1StepXI.lean
alignment Checked unowned Iut/Stage1/IUTStage1Theorem311.lean
alignment_endpoint Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
alignmentExperimentReport_canBuild Checked unowned Iut/Stage1/IUTStage1FrobenioidShift.lean
allLocalExpressionValid Checked unowned Iut/Foundations/QualitativeData.lean
allLocalExpressionValid_expanded Checked unowned Iut/Foundations/QualitativeData.lean
allLocalValid Checked unowned Iut/Foundations/QualitativeData.lean
allLocalValid_expanded Checked unowned Iut/Foundations/QualitativeData.lean
allowed_chart_transport Checked unowned Iut/Stage1/IUTStage1StepXI.lean
allowed_chart_transport Checked unowned Iut/Stage1/IUTStage1StepXI.lean
allowedChartTransport Checked unowned Iut/Stage1/IUTStage1StepXI.lean
allowedChartTransport Checked unowned Iut/Stage1/IUTStage1StepXI.lean
allowedForgetfulTransport_holds Checked unowned Iut/Stage1/IUTStage1StepXI.lean
allowed_q_to_target_reading Checked unowned Iut/Stage1/IUTStage1StepXI.lean
allowedQToTargetReading Checked unowned Iut/Stage1/IUTStage1StepXI.lean
allowed_theta_to_target_reading Checked unowned Iut/Stage1/IUTStage1StepXI.lean
allowedThetaToTargetReading Checked unowned Iut/Stage1/IUTStage1StepXI.lean
all_parameters_nonzero Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
all_parameters_nonzero Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
all_parameters_nonzero Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
all_parameters_nonzero Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
all_parameters_nonzero_coordinate Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
all_targets_at_most Checked unowned Iut/Foundations/AlgorithmicBridge.lean
all_targets_at_most Checked unowned Iut/Foundations/AlgorithmicBridge.lean
all_targets_at_most Checked unowned Iut/Stage1/IUTStage1StepXI.lean
all_targets_at_most Checked unowned Iut/Foundations/AlgorithmicBridge.lean
all_targets_at_most Checked unowned Iut/Foundations/AlgorithmicBridge.lean
all_targets_at_most Checked unowned Iut/Foundations/AlgorithmicBridge.lean
all_targets_at_most Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/CommonTargetBound.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Stage1/IUTStage1StepXI.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/CommonTargetBound.lean
allTargetsAtMost Checked unowned Iut/Stage1/IUTStage1StepXI.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicOutput.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Stage1/IUTStage1Data.lean
allTargetsAtMost Checked unowned Iut/Stage1/IUTStage1StepXI.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicOutput.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost Checked unowned Iut/Foundations/AlgorithmicBridge.lean
allTargetsAtMost_of_commonBound Checked unowned Iut/Foundations/TransportedRegionFamily.lean
allTargetsAtMost_of_commonHullBound Checked unowned Iut/Foundations/TransportedRegionFamily.lean
all_targets_at_most_theta Checked unowned Iut/Stage1/IUTStage1StepXI.lean
allTargetsAtMost_theta Checked unowned Iut/Stage1/IUTStage1StepXI.lean
anchor_compactOpenSubset_eq_ringOfIntegers Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
anchorCompactOpenSubset_eq_ringOfIntegers Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
anchorLocalFactorRegion_eq_realizedRingOfIntegers Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
anchorRingOfIntegers_eq_valuationBall_one Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
apply_eq_bridge_apply Checked unowned Iut/Foundations/AlgorithmicBridge.lean
apply_eq_bridgeApply Checked unowned Iut/Foundations/AlgorithmicBridge.lean
apply_eq_hull_det Checked unowned Iut/Foundations/AlgorithmicBridge.lean
apply_eq_hull_det Checked unowned Iut/Foundations/AlgorithmicBridge.lean
apply_eq_hullDet Checked unowned Iut/Foundations/AlgorithmicBridge.lean
apply_eq_hullDet Checked unowned Iut/Foundations/AlgorithmicBridge.lean
apply_eq_hull_to_common Checked unowned Iut/Foundations/AlgorithmicBridge.lean
apply_eq_hullToCommon Checked unowned Iut/Foundations/AlgorithmicBridge.lean
approximant_closed Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
approximant_eq_determinantLogVolume Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
approximant_eq_normalized_determinant Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
approximant_eq_projected_normalized Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
approximant_eq_weighted_normalized Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
approximant_hull_eq_self Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
approximant_hull_eq_self Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
approximant_hull_le_canonical_hull Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
approximant_hullLogVolume_le_canonical_hull Checked unowned Iut/Stage1/IUTStage1SourceCore.lean
approximant_logVolume_between Checked unowned Iut/Stage1/IUTStage1SourceCore.lean

Showing the highest-priority 200 proofs for fast server render.

Keyboard shortcuts