Blueprint Summary
Overview
Total entries83completed: 66; deps incomplete: 12; sorries: 2; no proof: 2
Ready now2Entries whose next formalization step is currently unblocked.
Fully closed66Local code and prerequisite closure are both complete.
Actionable priorities4Entries ready now and already unlocking downstream work.
Current blockers2Missing external or incomplete Lean declarations.
Missing informal coverage13Entries with Lean code but missing an informal statement or proof block.
Ready next (4)
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 10proof: ready to formalize
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 10
-
Ready for proof work.stage: proofstatement: formalizeddirect uses: 1downstream unlocks: 6proof: Lean code incomplete
Associated lean decls (1)
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 4proof: ready to formalize
Current blockers (2)
-
«code:c1_c2_c3_norms»Declaration with sorry:NopertInline.c3_norm_bound[theorem/lemma; contains sorry; in proof; refs: 1] -
Declaration with sorry:
Noperthedron.exists_solution_table[theorem/lemma; contains sorry; in proof; refs: unknown]
Missing informal coverage (13)
-
«code:lem:XPgt0»Associated lean decls (1)
-
«code:lem:sqrt5»Associated lean decls (3)
-
«code:lem:RaRa»Associated lean decls (4)
-
«code:lem:sqrt2»Associated lean decls (4)
-
«code:lem:radius_noperthedron_one» -
«code:lem:RxRy»Associated lean decls (2)
-
«code:c1_c2_c3_norms» -
«def:noperthedron_main»Associated lean decls (6)
-
«code:lem:RxRy_wlog»Associated lean decls (1)
-
«thm:polyhedron_radius_def»Associated lean decls (1)
-
Polyhedron.radius_iff
-
-
«code:lem:MPgtr»Associated lean decls (1)
-
«code:lem:RaRalpha»Associated lean decls (5)
-
«code:lem:jensen»Associated lean decls (1)
Entry index (83)
Definitions9completed: 7; deps incomplete: 1; sorries: 0; no proof: 0
Lemmas49completed: 45; deps incomplete: 2; sorries: 1; no proof: 1
Theorems20completed: 10; deps incomplete: 8; sorries: 1; no proof: 1
Corollaries5completed: 4; deps incomplete: 1; sorries: 0; no proof: 0
Lean-only entries12
Informal-only entries3
Definition Index (9)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
Theorem / Lemma / Corollary Index (74)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
«code:lem:XPgt0»Associated lean decls (1)
-
Associated lean decls (1)
-
«code:lem:sqrt5»Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
«code:lem:RaRa»Associated lean decls (4)
-
Associated lean decls (1)
-
«code:lem:sqrt2»Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
«code:lem:radius_noperthedron_one» -
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
«code:lem:RxRy»Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (11)
-
RationalApprox.R_difference_norm_bounded -
RationalApprox.R'_difference_norm_bounded -
RationalApprox.M_difference_norm_bounded -
RationalApprox.Mθ_difference_norm_bounded -
RationalApprox.Mφ_difference_norm_bounded -
RationalApprox.X_difference_norm_bounded -
RationalApprox.Rℚ_norm_bounded -
RationalApprox.Mℚ_norm_bounded -
RationalApprox.R'ℚ_norm_bounded -
RationalApprox.Mθℚ_norm_bounded -
RationalApprox.Mφℚ_norm_bounded
-
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
«code:c1_c2_c3_norms» -
Associated lean decls (1)
-
Associated lean decls (1)
-
«def:noperthedron_main»Associated lean decls (6)
-
«code:lem:RxRy_wlog»Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
«thm:polyhedron_radius_def»Associated lean decls (1)
-
Polyhedron.radius_iff
-
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
«code:lem:MPgtr»Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
«code:lem:RaRalpha»Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
«code:lem:jensen»Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
By parent groups (17)
Rational trigonometric approximations. (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
Radius and norm control for noperthedron vertices. (3)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
Soundness of table rows and propagated non-Rupert certificates. (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Rotation and norm control inequalities. (2)
-
Associated lean decls (4)
Pointsymmetry properties of the construction. (2)
-
Associated lean decls (1)
Perturbation bounds for projected points. (4)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Reductions from general poses to certified subcases. (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Trigonometric inequality reductions. (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
Radius characterization and preservation tools. (2)
-
Associated lean decls (1)
Distance and local-maximality sector estimates. (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Linear-algebra lemmas for local geometry. (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Rupert-tightening reduction lemmas. (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
Matrix approximation error bounds. (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (11)
-
RationalApprox.R_difference_norm_bounded -
RationalApprox.R'_difference_norm_bounded -
RationalApprox.M_difference_norm_bounded -
RationalApprox.Mθ_difference_norm_bounded -
RationalApprox.Mφ_difference_norm_bounded -
RationalApprox.X_difference_norm_bounded -
RationalApprox.Rℚ_norm_bounded -
RationalApprox.Mℚ_norm_bounded -
RationalApprox.R'ℚ_norm_bounded -
RationalApprox.Mθℚ_norm_bounded -
RationalApprox.Mφℚ_norm_bounded
-
-
Associated lean decls (1)
Derivative bounds and approximation control for rotated projections. (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
Local theorem approximation bounds. (4)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Final non-Rupert conclusions for the noperthedron. (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
Spanning criteria for projected triples. (1)
-
Associated lean decls (1)
Dependency insights
Statement-used entries10Entries reused in statement dependencies.
Proof-used entries61Entries reused in proof-only dependencies.
Tracked parent groups18Grouped health rollups for parents with more than one child entry.
Most used in statements (10)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 9
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
Most used in proofs (61)
-
Reverse dependencies recorded in proof dependencies.proof uses: 6statement uses: 0direct uses: 6downstream unlocks: 18
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 16
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 15
Associated lean decls (11)
-
RationalApprox.R_difference_norm_bounded -
RationalApprox.R'_difference_norm_bounded -
RationalApprox.M_difference_norm_bounded -
RationalApprox.Mθ_difference_norm_bounded -
RationalApprox.Mφ_difference_norm_bounded -
RationalApprox.X_difference_norm_bounded -
RationalApprox.Rℚ_norm_bounded -
RationalApprox.Mℚ_norm_bounded -
RationalApprox.R'ℚ_norm_bounded -
RationalApprox.Mθℚ_norm_bounded -
RationalApprox.Mφℚ_norm_bounded
-
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 19
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 16
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 11
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 21
Associated lean decls (4)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 21
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 20
Associated lean decls (1)
-
Show all 51 more proof-used entries
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 18
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 17
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 17
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 16
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
-
«thm:polyhedron_radius_def»Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10Associated lean decls (1)
-
Polyhedron.radius_iff
-
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 8
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 8
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 7
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 6
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 6
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 6
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 5
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 5
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Group health (18)
-
Noperthedron construction and core definitions.Grouped view over entries sharing the same parent.total: 4closed: 2local-only: 1ready: 1blocked: 0incomplete Lean: 0unlock score: 33
-
Radius characterization and preservation tools.Grouped view over entries sharing the same parent.total: 2closed: 1local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 22
-
Pointsymmetry properties of the construction.Grouped view over entries sharing the same parent.total: 2closed: 0local-only: 1ready: 1blocked: 0incomplete Lean: 0unlock score: 7
-
Matrix approximation error bounds.Grouped view over entries sharing the same parent.total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 74Next: no ready child currently unlocks downstream work.
-
Linear-algebra lemmas for local geometry.Grouped view over entries sharing the same parent.total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 73Next: no ready child currently unlocks downstream work.
-
Trigonometric inequality reductions.Grouped view over entries sharing the same parent.total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 60Next: no ready child currently unlocks downstream work.
-
Rational trigonometric approximations.Grouped view over entries sharing the same parent.total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 54Next: no ready child currently unlocks downstream work.
-
Local theorem approximation bounds.Grouped view over entries sharing the same parent.total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 52Next: no ready child currently unlocks downstream work.
-
Perturbation bounds for projected points.Grouped view over entries sharing the same parent.total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 52Next: no ready child currently unlocks downstream work.
-
Distance and local-maximality sector estimates.Grouped view over entries sharing the same parent.total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 45Next: no ready child currently unlocks downstream work.
-
Show all 8 more groups
-
Rotation and norm control inequalities.Grouped view over entries sharing the same parent.total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 37Next: no ready child currently unlocks downstream work.
-
Derivative bounds and approximation control for rotated projections.Grouped view over entries sharing the same parent.total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 33Next: no ready child currently unlocks downstream work.
-
Soundness of table rows and propagated non-Rupert certificates.Grouped view over entries sharing the same parent.total: 4closed: 1local-only: 3ready: 0blocked: 0incomplete Lean: 0unlock score: 29Next: no ready child currently unlocks downstream work.
-
Radius and norm control for noperthedron vertices.Grouped view over entries sharing the same parent.total: 3closed: 2local-only: 1ready: 0blocked: 0incomplete Lean: 0unlock score: 29Next: no ready child currently unlocks downstream work.
-
Spanning criteria for projected triples.Grouped view over entries sharing the same parent.total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 25Next: no ready child currently unlocks downstream work.
-
Rupert-tightening reduction lemmas.Grouped view over entries sharing the same parent.total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 11Next: no ready child currently unlocks downstream work.
-
Reductions from general poses to certified subcases.Grouped view over entries sharing the same parent.total: 3closed: 0local-only: 3ready: 0blocked: 0incomplete Lean: 0unlock score: 9Next: no ready child currently unlocks downstream work.
-
Final non-Rupert conclusions for the noperthedron.Grouped view over entries sharing the same parent.total: 2closed: 0local-only: 2ready: 0blocked: 0incomplete Lean: 0unlock score: 1Next: no ready child currently unlocks downstream work.
-
Metadata
Owners in use2Distinct owners referenced by the current blueprint entries.
Tags in use6Distinct tags currently attached to blueprint entries.
Owner rollups (2)
-
David Renshawentries: 2actionable: 0quick wins: 0linked PRs: 0
-
Jason Reedentries: 2actionable: 0quick wins: 0linked PRs: 0
Tag rollups (6)
-
tag: localentries: 4actionable: 0quick wins: 0linked PRs: 0
-
tag: spanningentries: 2actionable: 0quick wins: 0linked PRs: 0
-
tag: congruenceentries: 1actionable: 0quick wins: 0linked PRs: 0
-
tag: main-theorementries: 1actionable: 0quick wins: 0linked PRs: 0
-
tag: proofentries: 1actionable: 0quick wins: 0linked PRs: 0
-
tag: setupentries: 1actionable: 0quick wins: 0linked PRs: 0
Metadata audit
Missing owner79
Missing effort79
Untagged79
Missing owner (79)
-
Missing owner metadata.
Associated lean decls (3)
-
«code:c1_c2_c3_norms»Missing owner metadata. -
«code:lem:MPgtr»Missing owner metadata.Associated lean decls (1)
-
«code:lem:RaRalpha»Missing owner metadata.Associated lean decls (5)
-
«code:lem:RaRa»Missing owner metadata.Associated lean decls (4)
-
«code:lem:RxRy_wlog»Missing owner metadata.Associated lean decls (1)
-
«code:lem:RxRy»Missing owner metadata.Associated lean decls (2)
-
«code:lem:XPgt0»Missing owner metadata.Associated lean decls (1)
-
«code:lem:jensen»Missing owner metadata.Associated lean decls (1)
-
«code:lem:radius_noperthedron_one»Missing owner metadata. -
Show all 69 more entries missing owner
-
«code:lem:sqrt2»Missing owner metadata.Associated lean decls (4)
-
«code:lem:sqrt5»Missing owner metadata.Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (11)
-
RationalApprox.R_difference_norm_bounded -
RationalApprox.R'_difference_norm_bounded -
RationalApprox.M_difference_norm_bounded -
RationalApprox.Mθ_difference_norm_bounded -
RationalApprox.Mφ_difference_norm_bounded -
RationalApprox.X_difference_norm_bounded -
RationalApprox.Rℚ_norm_bounded -
RationalApprox.Mℚ_norm_bounded -
RationalApprox.R'ℚ_norm_bounded -
RationalApprox.Mθℚ_norm_bounded -
RationalApprox.Mφℚ_norm_bounded
-
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
«def:noperthedron_main»Missing owner metadata.Associated lean decls (6)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
«thm:polyhedron_radius_def»Missing owner metadata.Associated lean decls (1)
-
Polyhedron.radius_iff
-
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing effort (79)
-
Missing effort metadata.
Associated lean decls (3)
-
«code:c1_c2_c3_norms»Missing effort metadata. -
«code:lem:MPgtr»Missing effort metadata.Associated lean decls (1)
-
«code:lem:RaRalpha»Missing effort metadata.Associated lean decls (5)
-
«code:lem:RaRa»Missing effort metadata.Associated lean decls (4)
-
«code:lem:RxRy_wlog»Missing effort metadata.Associated lean decls (1)
-
«code:lem:RxRy»Missing effort metadata.Associated lean decls (2)
-
«code:lem:XPgt0»Missing effort metadata.Associated lean decls (1)
-
«code:lem:jensen»Missing effort metadata.Associated lean decls (1)
-
«code:lem:radius_noperthedron_one»Missing effort metadata. -
Show all 69 more entries missing effort
-
«code:lem:sqrt2»Missing effort metadata.Associated lean decls (4)
-
«code:lem:sqrt5»Missing effort metadata.Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (11)
-
RationalApprox.R_difference_norm_bounded -
RationalApprox.R'_difference_norm_bounded -
RationalApprox.M_difference_norm_bounded -
RationalApprox.Mθ_difference_norm_bounded -
RationalApprox.Mφ_difference_norm_bounded -
RationalApprox.X_difference_norm_bounded -
RationalApprox.Rℚ_norm_bounded -
RationalApprox.Mℚ_norm_bounded -
RationalApprox.R'ℚ_norm_bounded -
RationalApprox.Mθℚ_norm_bounded -
RationalApprox.Mφℚ_norm_bounded
-
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
«def:noperthedron_main»Missing effort metadata.Associated lean decls (6)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
«thm:polyhedron_radius_def»Missing effort metadata.Associated lean decls (1)
-
Polyhedron.radius_iff
-
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Untagged (79)
-
Missing tag metadata.
Associated lean decls (3)
-
«code:c1_c2_c3_norms»Missing tag metadata. -
«code:lem:MPgtr»Missing tag metadata.Associated lean decls (1)
-
«code:lem:RaRalpha»Missing tag metadata.Associated lean decls (5)
-
«code:lem:RaRa»Missing tag metadata.Associated lean decls (4)
-
«code:lem:RxRy_wlog»Missing tag metadata.Associated lean decls (1)
-
«code:lem:RxRy»Missing tag metadata.Associated lean decls (2)
-
«code:lem:XPgt0»Missing tag metadata.Associated lean decls (1)
-
«code:lem:jensen»Missing tag metadata.Associated lean decls (1)
-
«code:lem:radius_noperthedron_one»Missing tag metadata. -
Show all 69 more untagged entries
-
«code:lem:sqrt2»Missing tag metadata.Associated lean decls (4)
-
«code:lem:sqrt5»Missing tag metadata.Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (11)
-
RationalApprox.R_difference_norm_bounded -
RationalApprox.R'_difference_norm_bounded -
RationalApprox.M_difference_norm_bounded -
RationalApprox.Mθ_difference_norm_bounded -
RationalApprox.Mφ_difference_norm_bounded -
RationalApprox.X_difference_norm_bounded -
RationalApprox.Rℚ_norm_bounded -
RationalApprox.Mℚ_norm_bounded -
RationalApprox.R'ℚ_norm_bounded -
RationalApprox.Mθℚ_norm_bounded -
RationalApprox.Mφℚ_norm_bounded
-
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
«def:noperthedron_main»Missing tag metadata.Associated lean decls (6)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
«thm:polyhedron_radius_def»Missing tag metadata.Associated lean decls (1)
-
Polyhedron.radius_iff
-
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Structure and coverage
Informal-only3Statements with no associated Lean code yet.
Ready to formalize2Entries whose next step is currently unblocked.
Formalized, ancestors open12Local Lean work is done, but prerequisite closure is still open.
Fully closed66Local code and ancestor closure are both complete.
Heaviest prerequisites (39)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 0proof deps: 8direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 1proof deps: 5direct uses: 1downstream unlocks: 9
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 2proof deps: 3direct uses: 2downstream unlocks: 12
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 0proof deps: 4direct uses: 1downstream unlocks: 9
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 0proof deps: 4direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 1proof deps: 3direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 0proof deps: 3direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 0proof deps: 3direct uses: 1downstream unlocks: 8
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 5
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 7
-
Show all 29 more heaviest-prerequisite entries
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 2proof deps: 1direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 3downstream unlocks: 15
Associated lean decls (11)
-
RationalApprox.R_difference_norm_bounded -
RationalApprox.R'_difference_norm_bounded -
RationalApprox.M_difference_norm_bounded -
RationalApprox.Mθ_difference_norm_bounded -
RationalApprox.Mφ_difference_norm_bounded -
RationalApprox.X_difference_norm_bounded -
RationalApprox.Rℚ_norm_bounded -
RationalApprox.Mℚ_norm_bounded -
RationalApprox.R'ℚ_norm_bounded -
RationalApprox.Mθℚ_norm_bounded -
RationalApprox.Mφℚ_norm_bounded
-
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 20
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 10
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 16
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 12
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 9
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 4
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 6
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 9
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 5
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 2downstream unlocks: 19
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 2downstream unlocks: 11
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 17
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 6downstream unlocks: 18
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 10
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 8
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 18
Associated lean decls (2)
-
«thm:polyhedron_radius_def»Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 10Associated lean decls (1)
-
Polyhedron.radius_iff
-
-
No prerequisites (44)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
«code:lem:XPgt0»Associated lean decls (1)
-
Associated lean decls (1)
-
«code:lem:sqrt2»Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Show all 34 more entries without prerequisites
-
Associated lean decls (1)
-
Associated lean decls (1)
-
«code:c1_c2_c3_norms» -
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
«code:lem:jensen»Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
«code:lem:RaRalpha»Associated lean decls (5)
-
«code:lem:MPgtr»Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
«code:lem:RxRy_wlog»Associated lean decls (1)
-
«def:noperthedron_main»Associated lean decls (6)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
«code:lem:RxRy»Associated lean decls (2)
-
«code:lem:radius_noperthedron_one» -
Associated lean decls (1)
-
«code:lem:RaRa»Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
«code:lem:sqrt5»Associated lean decls (3)
-
No dependents (13)
-
«code:lem:XPgt0»Associated lean decls (1)
-
«code:lem:sqrt2»Associated lean decls (4)
-
«code:lem:radius_noperthedron_one» -
«code:lem:RxRy»Associated lean decls (2)
-
«code:c1_c2_c3_norms» -
«code:lem:RaRalpha»Associated lean decls (5)
-
«code:lem:jensen»Associated lean decls (1)
-
Associated lean decls (1)
-
«code:lem:MPgtr»Associated lean decls (1)
-
«code:lem:RxRy_wlog»Associated lean decls (1)
-
Show all 3 more entries without dependents
-
«def:noperthedron_main»Associated lean decls (6)
-
«code:lem:RaRa»Associated lean decls (4)
-
«code:lem:sqrt5»Associated lean decls (3)
-
Proof debt hotspots (1)
-
Construction of the certified interval solution table.Grouped proof/code debt derived from the current incomplete-declaration snapshots.affected entries: 1incomplete decls: 1missing decls: 0total debt: 1